bild
School of
Electrical Engineering
and Computer Science

Compositional Verification of Control-Flow Based Temporal Safety Properties of Programs with Procedures




1. Introduction

CVPP is an informal collaborative project aiming at the development of techniques for the algorithmic verification of control flow based properties of programs with procedures, with focus on compositionality.

2. Participants

At present, the people involved in the collaboration are:

3. Summary of the Approach

We develop methods for the algorithmic verification of open systems, that is, systems where some components (termed concrete) are available through their implementation as Java bytecode, while other components (termed abstract) are given through their specifications, that is, a formal description of their essential properties.  Such systems arise naturally when the implementation of certain components is not yet available, such as in the context of mobile code. Open systems also arise in the context of modular design, where for verification purposes the specification of components is used rather than their implementation, since the implementation is allowed to change over time (say, be optimised for performance) but not the specification. The main problem that arises when verifying open systems is how to relativise the verification on specifications of components. The technique we explore is based on the notion of maximal model for a given specification,  that is a model that represents all models satisfying the specification, in the sense that it possesses exactly those properties shared by all these models. In effect, this allows abstract components to be replaced by concrete ones, in this way reducing the verification problem to standard model checking.

Our program model abstracts from the data, thus focusing on (and over-approximating) program control flow. The structure of programs is given by means of flow graphs, while program behaviour is given by means of pushdown automata (PDAs), induced canonically from the flow graphs, and capturing the passing of control during method calls and returns.

We consider properties of the structure as well as the behaviour of programs. Both types of properties are specified in a fragment of the modal mu-calculus with box modalities and greatest fixed points only, interpreted over flow graphs and flow graph behaviours, respectively.

4. Verification Method

Our algorithmic verification method for open systems deals (a) with components, namely how a component implementation relates to its specification, as well as (b) with systems, namely how system properties relate to component properties.

A. Model checking of a concrete component against a property (specification) consists of the following steps:
  1. Extract flow graph of component from Java bytecode [Program Analyser]
    • If needed, inline private methods [Inliner]
  2. For structural properties:
    • cast flow graph as finite automaton, e.g. as CCS term [Model Generator], then
    • apply standard, finite–state model checking [CWB]
  • For behavioural properties:
    • cast flow graph as pushdown automaton [Model Generator], then
    • apply PDA model checking [NikMC]
B. Model checking of an open system against a property consists of the following steps:
  1. For every concrete component, proceed as explained in A.1
  2. For every abstract component, from specification:
    • if structural, compute maximal flow graph [Maximal Model Constructor]
    • if behavioural, first translate to equivalent set of structural properties [Property Translator], then construct the corresponding set of maximal flow graphs
  3. Compose extracted with constructed flow graphs to obtain the flow graph of the open system
  4. Model check resulting flow graph against global property, as explained in A.2

5. Tool Support

We provide tool support for our verification method in the form of a tool set consisting of the following individual tools:
  1. Program Analyser: Extracts flow graphs (with the help of Sawja)
  2. Inliner: Abstracts flow graph from private methods
  3. Property Translator: Translates behavioural to structural properties
  4. Maximal Model Constructor: Produces maximal flow graphs
  5. Model Generator: Casts flow graphs as FAs or PDAs for model checking
  6. Model Checkers: For verifying structural and behavioural properties
We also provide ProMoVer which is a tool based on our tool set to automate the proceudre-modular verification.

6. Publications


7. Tasks

Show Tasks

Published by: Siavash Soleimanifard <siavashs@csc.kth.se>
Updated 2015-02-05