Abstraction-based generation of finite state models from C programs.

摘要

Model checking is a major advancement in the quest for practical automatic verification methods for computer systems, and has been effectively used to discover flaws in real-world hardware systems. Unfortunately, applying model-checking techniques to software systems has proved to be more difficult, due to the large number of states and irregular transitions of such systems. One promising method for generating reasonably-sized models from programs is the use of system (LTS), which is much smaller than the concrete LTS (the LTS which would sound in the sense that if a program is well-behaved in its use of pointers, then any linear temporal logic formula which holds true for the can be checked against the design for bisimilarity. Bisimilarity ensures that the program is a faithful implementation of the design. A suite of software tools has been implemented based upon the theory. These tools interface with the Concurrency Workbench, a model checking system. A case study is presented which shows the practicality of this technique for verifying real-world C programs.