# TC-Verifier: Trans-Compiler-Based Code Translator Verifier with Model-Checking
## 3 Methodology
### Verification Success Rate  
Given that the translation process is modeled as a state machine, where translation correctness is verified based on whether the state machine reaches a valid final state without deadlocks, we can define an objective metric for evaluating the verifier. The formal notation of the state machine for the translation process is as follows:  
* \(S\) be the set of all possible states in the state machine. * \(s_{0}\in S\) be the initial state. * \(s_{f}\in S\) be the valid final state (i.e., successful verification). * \(\Sigma\) be the input alphabet representing syntactic structures of the source language. * \(T:S\times\Sigma\to S\) be the state transition function defined by the trans-compiler rules. * \(P\) be the set of translation paths executed for different syntactic structures. We define the verification process as a deterministic finite state machine (FSM), where reaching \(s_{f}\) signifies successful translation verification. We can define a verification success rate metric (\(\mathcal{V}\)). The verification success rate measures the proportion of input constructs that successfully reach the final state \(s_{f}\). A higher \(\mathcal{V}\) indicates better verification performance:  
\[\mathcal{V}=\frac{|P_{\text{success}}|}{|P|} \tag{1}\]  
where:  
* \(P_{\text{success}}\subseteq P\) is the subset of translation paths that lead to \(s_{f}\) (i.e., verified translations). * \(|P|\) is the total number of translation paths attempted by the symbolic queries. After forming the Uppaal model, we can define queries to check certain properties and paths' validity to later compute the verification success rate (\(\mathcal{V}\)). There are two main query types that we will use in our queries: possibly and invariantly. The possibly query; \(E<>p\) evaluates to true for a state transition system if and only if there is a sequence of action transitions \(s0\to s1\rightarrow\ldots\to sn\), where \(s0\) is the initial state and \(sn\) satisfies \(p\). \(p\) is a property that we define. For example, \(p\) can be \(Process\_end\) which means that the process reaches the end state. It can also be _not deadlock_, which means that the state machine will not halt in a certain state. Many other properties can be defined according to the needed check. \(E<>\)\(Process\_end\) means there exists a path to reach the end state. The invariantly query; \(A[\;]p\) evaluates to true if (and only if) every reachable state satisfies the property p. The query \(A[\;]Process.end\) means that for each reachable state in the state machine, the end state is reachable from that state. Uppaal verifier symbolically checks these properties defined by symbolic queries and gives a result satisfied or not satisfied. For invariant queries, if the query is not satisfied, it gives a counter-example with a trace that proves the violation. In the case of a possibly query, it provides a trace only for the satisfied case. Since Uppaal does not give all the counter-examples or all the violation traces, we had to write queries for all expected symbols to have a possibly query for each different symbol. This process will consume time if written manually. However, it can be easily automated since it is very systematic. We used ChatGPT 4 by open AI in this process using one-shot learning. We give one example to ChatGPT for the encoded variables, the XML model exported from Uppaal, where the format of the query needed in the prompt with the comment explains the query. We also write in the prompt the properties that we need to check in simple English language. The comment example is essential as it will be used in the interpretation of the results. Then, ChatGPT gives us all the queries needed to be placed in a.q file with the comment of each query. Since each translation process involves only a few dozen queries, we used human validation to assess the quality of the queries generated by GPT-4. For each code statement translation state machine model, we have two main queries in addition to the path-specific queries.