|
A Constraint Oriented Proof Methodology Based on Modal Transition
Systems
Kim G. Larsen December 1994 |
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. Available as PostScript, PDF, DVI. |