The Design And Implementation Of An Automated Model Checking Oriented Model Extractor

With the increasing complexity of computer softwares, it is necessary and urgent to ensure the correctness and reliability of these systems. Model Checking is a formal method for verifying the temporal logic properties of finite state systems, and has gotten huge success in areas such as hardware circuits, device drivers and security protocols.The difficulty of applying model checking technique to the systems implemented in high-level programming language is extracting an abstract model which is usually done by hand. But this approach has some weaknesses, for instance, the cost of modeling is fairly high and the artificial models are error-prone, therefore there are strong practical requirements for extracting verification model from the source code directly. SPIN is one of the most excellent model checkers whose modeling language is PROMELA, while the C programming language is one of the most popular languages, so the main content of the thesis focuses on the technique of model extraction for C programs in order to achieve the goal of model checking C programs with SPIN automatically.In this thesis, we design a set of methods for extracting verification models from the ANSI-C programs which handle most language features in C properly, especially a few tough structures, such as recursive function, enumeration type and pointer. And then we develop a model extractor named C2Spin. C2Spin is divided into two parts in terms of functionality, the front-end and the back-end. The front-end is an analyzer that executes lexical and syntactic analysis over the C source code.The back-end is a translator that performs systematic translation from C programs into PROMELA descriptions. Moreover, a couple of abstraction and optimization techniques were deployed in C2Spin so as to reduce the size of the model, speed up the process of model extraction or improve the efficiency of the execution.C2Spin reduces the expense of modeling significantly. SPIN can detect various errors in applications implemented in C mechanically combining with C2Spin, such as deadlock. We ran a quantity of testing using C2Spin. In the experiments, depending upon the models generated by C2Spin, we found a semantic bug in SPIN4.3.0 and similar livelocks in the implementation of two classic mutual exclusion algorithms written by Holzmann. Thus we conclude that C2Spin is useful in testing ANSI-C programs.