# TC-Verifier: Trans-Compiler-Based Code Translator Verifier with Model-Checking
## 3 Methodology
### Selected Verification Tool  
Before using a specific tool to verify the trans-compiler, we performed an initial pilot test to check the user-friendliness of three model-checking tools. This initial test aims to choose a tool to implement the model-checking idea and prove the concept. We evaluated the tested tools according to the following points:  
* User-friendly modeling: This is essential for providing a user-friendly model-checking methodology that can be applied to various types of trans-compilers regardless of the experience of the TC-Verifier users with model-checking tools. * Flexible user-defined specifications: The specifications and properties to be checked can be written easily and do not require deep knowledge of model checking. Given that many model checkers are primarily designed to verify parallel code and address security-sensitive aspects, the chosen model checker must be adaptable enough to effectively model sequential software with user-defined specifications. * Providing counterexamples: The results from the verification process should not only differentiate between the formally verified rules and those that remain unverified but also provide counterexamples where verification fails. These counterexamples are vital for pinpointing specific scenarios or input cases where the trans-compiler does not meet the expected criteria. * Quality of tool documentation and tutorial availability: This documentation is essential for software developers like trans-compiler developers who are non-experts in formal verification to model their software and formalize its specifications. * Modeling automation: capability to automate the transformation of the trans-compiler into its model form. Such automation would significantly streamline the verification process, enhancing efficiency and reducing the potential for error. We investigated three tools for our problem context, and we evaluated them using the defined aspects. The three experimented tools are Alloy [19], Spin [20], and Uppaal [21; 22]. Table 1 shows an evaluation and comparison resulting from the experiment of modeling the variable declaration translation process using the three tools. Alloy, a tool that uses relational and first-order logic, requires a deep understanding of its specification language, significantly different from conventional programming lan \begin{table}
\begin{tabular}{l c c c} \hline \hline
**Evaluation Aspect** & **Alloy** & **Spin** & **Uppaal** \\ \hline User-friendly modeling & Poor & Excellent & Moderate \\ Flexible user-defined specifications & Poor & Poor & Excellent \\ Providing counterexamples & Moderate & Excellent & Excellent \\ Documentation and Tutorials & Excellent & Moderate & Excellent \\ Automated modeling support & No & No & No \\ \hline \hline \end{tabular}
\end{table} 
Table 1: Comparison and evaluation of model checking tools. guages. This complexity is further compounded by the need for users to understand how to formulate and check assertions within the system, making it less ideal for those unfamiliar with its unique structure. The analysis performed by Alloy is limited by the user-provided bounds, which may not be sufficient for the applications requiring comprehensive verification [23]. Meanwhile, Spin, which is tailored for verifying the distributed systems using Promela [24], proved cumbersome for our needs. The translation of Java code into Promela was not only time-consuming, requiring over 100 lines of code for a simple task, but also limited by Promela's poor support for complex data types [25] and potential for state space explosions in more complex scenarios, making it unsuitable for comprehensive modeling of our trans-compiler. Although Promela allowed us to model the sequential behavior of the translator, it suffered from the scarcity of detailed tutorials and documentation and the difficulty of specifying the specifications to be checked.