Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Compositional Verification of Programs with Procedures
[go: Go Back, main page]

Compositional Verification of Control-Flow 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]
  2. For structural properties:
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:
  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 Soot)
  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
6. Publications