Back to Search
Start Over
Translating Xd-C programs to MSVL programs.
- Source :
-
Theoretical Computer Science . Feb2020, Vol. 809, p430-465. 36p. - Publication Year :
- 2020
-
Abstract
- C language is one of the most popular languages for software systems. In order to verify safety, reliability and security properties of such systems written in C, a tool UMC4M for runtime verification at code level based on Modeling, Simulation and Verification Language (MSVL) and its compiler MC is employed. To do so, a C program P has to be translated to an MSVL program M and the negation of a desired property Q is also translated to an MSVL program M', then "M and M'" is compiled and executed armed with MC. Whether P violates Q is checked by evaluating whether there exists an acceptable execution of new MSVL program "M and M'". Therefore, how to translate a C program to an MSVL program is a critical issue. However, in general, C is of complicated structures with goto statement. In this paper, we confine the syntax of C in a suitable subset called Xd-C without loss of expressiveness. Further, we present a translation algorithm from an Xd-C program to an MSVL program based on translation algorithms for expressions and statements. Moreover, the equivalences between expressions and statements involved in Xd-C and MSVL programs are inductively proved. Subsequently, the equivalence between the original Xd-C program and the translated MSVL program is also proved. In addition, the proposed approach has been implemented by a tool called C 2 M. A benchmark of experiments including 13 real-world Xd-C programs is conducted. The results show that C 2 M works effectively. [ABSTRACT FROM AUTHOR]
Details
- Language :
- English
- ISSN :
- 03043975
- Volume :
- 809
- Database :
- Academic Search Index
- Journal :
- Theoretical Computer Science
- Publication Type :
- Academic Journal
- Accession number :
- 141379581
- Full Text :
- https://doi.org/10.1016/j.tcs.2019.12.038