Open AccessA Constraint Oriented Proof Methodology based on Modal Transition Systems
Author(s) -
Kim G. Larsen
Publication year - 1994
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v1i47.21595
Subject(s) - computer science , constraint (computer aided design) , programming language , modal , abstraction , transition system , model checking , reduction (mathematics) , algorithm , principle of compositionality , theoretical computer science , key (lock) , state (computer science) , mathematics , artificial intelligence , operating system , philosophy , chemistry , geometry , epistemology , polymer chemistry
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