A Constraint Oriented Proof Methodology Based on Modal Transition Systems

Kim G. Larsen
Bernhard Steffen
Carsten Weise

In TACAS, pages 13--28

Abstract:

We present a constraint-oriented state-based proof methodology for concurrent software systems which exploits compositionality and abstraction for the reduction of the verification problem under investigation. Formal basis for this methodology are Modal Transition Systems allowing loose state-based specifications, which can be refined by successively adding constraints. Key concepts of our method are projective views, separation of proof obligations, Skolemization and abstraction. Central to the method is the use of Parametrized Modal Transition Systems. The method easily transfers to real-time systems, where the main problem are parameters in timing constraints.

Comments
Aalborg, Denmark and Passau/Aachen, Germany. Email: carsten@informatik.rwth-aachen.de.

Available as PostScript.

BRICS WWW home page