Compositional Verification of Sequential Programs with Procedures

Abstrakt:

I 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. I shall consider safety properties of the control flow behaviour of programs, as well as of the control flow structure.

The compositional verification method builds on a technique proposed by Grumberg and Long who use maximal models to reduce compositional verification of finite-state parallel processes to standard model checking. The generalisation of the maximal model technique to programs with recursion requires a refinement, since maximal applets are only guaranteed to exist for structural but not for behavioural properties. I therefore present a mixed, two-level approach where local assumptions are structural, while the global guarantee is behavioural.

The proposed verification method is applicable to arbitrary sequential programs with procedures. It is evaluated on an industrial case study taken from the smart card area. By separating the tasks of verifying global and local properties the method supports secure post-issuance loading of applets onto a smart card.