A Constraint Oriented Proof Methodology Based on Modal Transition Systems

A Constraint Oriented Proof Methodology Based on Modal Transition Systems

Kim G. Larsen
Bernhard Steffen
Carsten Weise

In 6th NWPT, pages 238-250

Abstract:

In this paper, 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. The method is even applicable to real time systems.

Comments
Weise: Lehrstuhl für Informatik I, Aachen University of Technology, Germany. Email: carsten@informatik.rwth-aachen.de.

Available as PostScript, DVI.

[BRICS symbol] BRICS WWW home page