Compositional verification of sequential programs with procedures
2008 (English)In: Information and Computation, ISSN 0890-5401, E-ISSN 1090-2651, Vol. 206, no 7, 840-868 p.Article in journal (Refereed) Published
We present a method for algorithmic, compositional verification of control-flow-based safety properties of sequential programs with procedures. The application of the method involves three steps: (1) decomposing the desired global property into local properties of the components, (2) proving the correctness of the property decomposition by using a maximal model construction, and (3) verifying that the component implementations obey their local specifications. We consider safety properties of both the structure and the behaviour of program control flow. Our compositional verification method builds on a technique proposed by Grumberg and Long that uses maximal models to reduce compositional verification of finite-state parallel processes to standard model checking. We present a novel maximal model construction for the fragment of the modal P-calculus with boxes and greatest fixed points only, and adapt it to control-flow graphs modelling components described in a sequential procedural language. We extend our verification method to programs with private procedures by defining an abstraction, presented as an inlining transformation. All algorithms have been implemented in a tool set automating all required verification steps. We validate our approach on an electronic purse case study.
Place, publisher, year, edition, pages
2008. Vol. 206, no 7, 840-868 p.
program verification, control-flow behaviour, compositional reasoning, modal mu-calculus, safety properties, maximal model, private procedures, modular model checking, reachability analysis, applet interactions, software, automata, machines
IdentifiersURN: urn:nbn:se:kth:diva-17733DOI: 10.1016/j.ic.2008.03.003ISI: 000258015900004ScopusID: 2-s2.0-46149087012OAI: oai:DiVA.org:kth-17733DiVA: diva2:335778
QC 201005252010-08-052010-08-05Bibliographically approved