Translating Xd-C programs to MSVL programs.

*(English)*Zbl 1436.68077Summary: 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 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 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 C2M. A benchmark of experiments including 13 real-world Xd-C programs is conducted. The results show that C2M works effectively.

##### MSC:

68N15 | Theory of programming languages |

68N20 | Theory of compilers and interpreters |

68Q60 | Specification and verification (program logics, model checking, etc.) |

PDF
BibTeX
XML
Cite

\textit{M. Wang} et al., Theor. Comput. Sci. 809, 430--465 (2020; Zbl 1436.68077)

Full Text:
DOI

##### References:

[1] | Clarke, E. M.; Grumberg, O.; Long, D. E., Model checking and abstraction, ACM Trans. Program. Lang. Syst., 16, 5, 1512-1542 (1994) |

[2] | Clarke, E. M.; Grumberg, O.; Peled, D., Model Checking (1999), MIT Press |

[3] | Cimatti, A.; Clarke, E.; Giunchiglia, E.; Giunchiglia, F.; Pistore, M.; Roveri, M.; Sebastiani, R.; Tacchella, A., NuSMV 2: an opensource tool for symbolic model checking, (Proceedings of the 14th International Conference on Computer Aided Verification. Proceedings of the 14th International Conference on Computer Aided Verification, CAV. Proceedings of the 14th International Conference on Computer Aided Verification. Proceedings of the 14th International Conference on Computer Aided Verification, CAV, Lecture Notes in Computer Science, vol. 2404 (2002), Springer), 359-364 · Zbl 1010.68766 |

[4] | Holzmann, G. J., The model checker SPIN, IEEE Trans. Softw. Eng., 23, 5, 279-295 (1997) |

[5] | Pnueli, A., The temporal logic of programs, (Proceedings of the 18th Annual Symposium on Foundations of Computer Science. Proceedings of the 18th Annual Symposium on Foundations of Computer Science, FOCS (1977), IEEE Computer Society), 46-57 |

[6] | Clarke, E. M.; Emerson, E. A.; Sistla, A. P., Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Trans. Program. Lang. Syst., 8, 2, 244-263 (1986) · Zbl 0591.68027 |

[7] | Gheorghe, M.; Ceterchi, R.; Ipate, F.; Konur, S.; Lefticaru, R., Kernel p systems: from modelling to verification and testing, Theor. Comput. Sci., 724, 45-60 (2018) · Zbl 1390.68309 |

[8] | Natarajan, A.; Chauhan, H.; Mittal, N.; Garg, V. K., Efficient abstraction algorithms for predicate detection, Theor. Comput. Sci., 688, 24-48 (2017) · Zbl 1371.68180 |

[9] | Ivancic, F.; Shlyakhter, I.; Gupta, A.; Ganai, M. K.; Kahlon, V.; Wang, C.; Yang, Z., Model checking C programs using F-SOFT, (Proceedings of 23rd International Conference on Computer Design. Proceedings of 23rd International Conference on Computer Design, ICCD (2005), IEEE Computer Society), 297-308 |

[10] | Henzinger, T. A.; Jhala, R.; Majumdar, R.; Sutre, G., Lazy abstraction, (Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL (2002), ACM), 58-70 · Zbl 1323.68374 |

[11] | Beyer, D.; Cimatti, A.; Griggio, A.; Keremoglu, M. E.; Sebastiani, R., Software model checking via large-block encoding, (Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design. Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD (2009), IEEE), 25-32 |

[12] | Dietsch, D.; Heizmann, M.; Langenfeld, V.; Podelski, A., Fairness modulo theory: a new approach to LTL software model checking, (Proceedings of the 27th International Conference on Computer Aided Verification. Proceedings of the 27th International Conference on Computer Aided Verification, CAV. Proceedings of the 27th International Conference on Computer Aided Verification. Proceedings of the 27th International Conference on Computer Aided Verification, CAV, Lecture Notes in Computer Science, vol. 9206 (2015), Springer), 49-66 · Zbl 1381.68157 |

[13] | Ball, T.; Rajamani, S. K., Automatically validating temporal safety properties of interfaces, (Proceedings of the 8th International SPIN Workshop on Model Checking of Software. Proceedings of the 8th International SPIN Workshop on Model Checking of Software, Lecture Notes in Computer Science, vol. 2057 (2001), Springer), 103-122 · Zbl 0985.68641 |

[14] | Beyer, D.; Henzinger, T. A.; Jhala, R.; Majumdar, R., The software model checker BLAST: applications to software engineering, Int. J. Softw. Tools Technol. Transf., 9, 5, 505-525 (2007) |

[15] | Beyer, D.; Keremoglu, M. E., CPAchecker: a tool for configurable software verification, (Proceedings of 23rd International Conference on Computer Aided Verification. Proceedings of 23rd International Conference on Computer Aided Verification, CAV. Proceedings of 23rd International Conference on Computer Aided Verification. Proceedings of 23rd International Conference on Computer Aided Verification, CAV, Lecture Notes in Computer Science, vol. 6806 (2011), Springer), 184-190 |

[16] | Kroening, D.; Tautschnig, M., CBMC - C bounded model checker, (Proceedings of 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Proceedings of 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS. Proceedings of 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Proceedings of 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS, Lecture Notes in Computer Science, vol. 8413 (2014), Springer), 389-391 |

[17] | Brockschmidt, M.; Cook, B.; Ishtiaq, S.; Khlaaf, H.; Piterman, N., T2: temporal property verification, (Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS. Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS, Lecture Notes in Computer Science, vol. 9636 (2016), Springer), 387-393 |

[18] | Wang, M.; Tian, C.; Duan, Z., Full regular temporal property verification as dynamic program execution, (Proceedings of the 39th International Conference on Software Engineering (ICSE) - Companion Volume (2017), IEEE Computer Society), 226-228 |

[19] | Wang, M.; Tian, C.; Zhang, N.; Duan, Z., Verifying full regular temporal properties of programs via dynamic program execution, IEEE Trans. Reliab., 1-16 (2018) |

[20] | Duan, Z., An extended interval temporal logic and a framing technique for temporal logic programming (1996), Department of Computer Science, Newcastle University, Newcastle upon Tyne: Department of Computer Science, Newcastle University, Newcastle upon Tyne UK, Ph.D. thesis |

[21] | Duan, Z., Temporal Logic and Temporal Logic Programming (2005), Science Press: Science Press Alexandria, NSW, Australia |

[22] | Zhang, N.; Duan, Z.; Tian, C., A mechanism of function calls in MSVL, Theor. Comput. Sci., 654, 11-25 (2016) · Zbl 1353.68184 |

[23] | Yang, K.; Duan, Z.; Tian, C.; Zhang, N., A compiler for MSVL and its applications, Theor. Comput. Sci., 749, 2-16 (2018) · Zbl 1407.68096 |

[24] | Duan, Z.; Tian, C., A practical decision procedure for propositional projection temporal logic with infinite models, Theor. Comput. Sci., 554, 169-190 (2014) · Zbl 1358.68188 |

[25] | Duan, Z.; Tian, C.; Zhang, L., A decision procedure for propositional projection temporal logic with infinite models, Acta Inform., 45, 1, 43-78 (2008) · Zbl 1141.68039 |

[26] | Howar, F.; Isberner, M.; Merten, M.; Steffen, B.; Beyer, D., The RERS grey-box challenge 2012: analysis of event-condition-action systems, (Proceedings of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation. Proceedings of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA. Proceedings of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation. Proceedings of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA, Lecture Notes in Computer Science, vol. 7609 (2012), Springer), 608-614 |

[27] | Navabpour, S.; Joshi, Y.; Wu, W.; Berkovich, S.; Medhat, R.; Bonakdarpour, B.; Fischmeister, S., RiTHM: a tool for enabling time-triggered runtime verification for c programs, (Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering (2013), ACM: ACM New York), 603-606 |

[28] | Wang, M.; Tian, C.; Zhang, N.; Duan, Z., Verifying full regular temporal properties of programs via dynamic program execution, IEEE Trans. Reliab., 68, 3, 1101-1116 (2019) |

[29] | Blazy, S.; Leroy, X., Mechanized semantics for the Clight subset of the C language, J. Autom. Reason., 43, 3, 263-288 (2009) · Zbl 1185.68136 |

[30] | Yang, X.; Duan, Z., Operational semantics of framed tempura, J. Log. Algebraic Program., 78, 1, 22-51 (2008) · Zbl 1170.68006 |

[31] | Wang, X.; Tian, C.; Duan, Z.; Zhao, L., MSVL: a typed language for temporal logic programming, Front. Comput. Sci., 11, 5, 762-785 (2017) |

[32] | Standard Performance Evaluation Corporation, SPEC CINT2000, October 2008 |

[33] | Duan, Z.; Yang, X.; Koutny, M., Framed temporal logic programming, Sci. Comput. Program., 70, 1, 31-61 (2008) · Zbl 1131.68036 |

[34] | Duan, Z.; Koutny, M., A framed temporal logic programming language, J. Comput. Sci. Technol., 19, 3, 341-351 (2004) |

[35] | Blazy, S.; Dargaye, Z.; Leroy, X., Formal verification of a C compiler front-end, (Proceedings of the 14th International Symposium on Formal Methods (FM). Proceedings of the 14th International Symposium on Formal Methods (FM), Lecture Notes in Computer Science, vol. 4085 (2006), Springer), 460-475 |

[36] | (2018) |

[37] | (2018) |

[38] | (2014) |

[39] | Zhang, N.; Duan, Z.; Tian, C., Model checking concurrent systems with MSVL, Sci. China Inf. Sci., 59, 11, Article 118101 pp. (2016) |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.