Hassen Saïdi

Modular and Incremental Analysis of Concurrent Software Systems

To appear in the Proceedings of the 14th IEEE International Conference on Automated Software Engineering (ASE'99), Cocoa Beach, Florida.


Modularization and abstraction are the keys to practical verification and analysis of large and complex systems. In this paper, we present an incremental methodology for the automatic analysis and verification of temporal properties of concurrent software systems. Our methodology is based on the theory of abstract interpretation. We first propose a compositional data flow analysis algorithm that computes invariants of concurrent systems by composing invariants generated separately for each component. The generated invariants are associated to each control location in each component. We present a novel compositional rule allowing us to obtain strong invariants of the whole system as conjunctions of local invariants of each component. Our work is a generalization of previous work on this topic, and allows us to generate stronger invariants. We also show how the generated invariants are used to construct, almost for free, finite state abstractions of the original system that preserve safety properties. This reduces dramatically the cost of computing such abstractions as reported in previous work. We finally give a novel refinement algorithm which refines the constructed abstraction until the property of interest is proved or a counterexample is exhibited. Our methodology is implemented in a framework that combines deductive methods supported by theorem proving techniques and algorithmic methods supported by model checking and abstract interpretation techniques.

Click here to get the compressed postscript file of the paper.