The Methodology of Modal Constraints
Kim G. Larsen, Bernhard Steffen, Carsten Weise · 1996
. We present a complete solution of the RPC-Memory Specification Problem, by applying a constraint-oriented state-based proof methodology for concurrent software systems. Our methodolgy 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 extends elegantly to real-time systems. 1 Introduction We present a constraint-oriented state-based proof methodology for concurrent software systems which exploits compositionality and abstraction for the reduction of the investigated verification problem. Formal basis for this methodology are Modal Transition Systems (MTS) [LT88] allowin...