Compositional verification of sequential programs with procedures
METADATA ONLY
Loading...
Author / Producer
Date
2008-07
Publication Type
Journal Article
ETH Bibliography
yes
Citations
Altmetric
METADATA ONLY
Data
Rights / License
Abstract
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 μ-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.
Permanent link
Publication status
published
External links
Editor
Book title
Journal / series
Volume
206 (7)
Pages / Article No.
840 - 868
Publisher
Elsevier
Event
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
Program verification; Control-flow behaviour; Compositional reasoning; Modal μ-calculus; Safety properties; Maximal model; Private procedures
Organisational unit
03634 - Basin, David / Basin, David