A Constraint Oriented Proof Methodology Based on Modal Transition
Kim G. Larsen
In TACAS, pages
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.
Aalborg, Denmark and Passau/Aachen, Germany. Email:
Available as PostScript.
BRICS WWW home page