Paper Info
Title
Seven at one stroke: LTL model checking for High-level Specifications in B, Z, CSP, and more
Abstract
The size of formal models is steadily increasing and there is a demand from industrial users to be able to use expressive temporal query languages for validating and exploring high-level formal specifications. We present an exten- sion of LTL, which is well adapted for validating B, Z and CSP specifications. We present a generic, flexible LTL model checker, implemented inside the PROB tool, that can be applied to a multitude of formalisms such as B, Z, CSP, BkCSP, as well as Object Petri nets, compensating CSP, and dSL. Our algorithm can deal with deadlocking states, partially explored state spaces, past operators, and can be combined with existing symmetry reduction techniques of PROB. We estab- lish correctness of our algorithm in general, as well as combined with symmetry reduction. Finally, we present various applications and empirical results of our tool, showing that it can be applied successfully in practice. Keywords: Validation and Verification, Notations and Languages, LTL, model checking, B-method, CSP, Z, Integrated Methods, symmetry reduction.
Year
Venue
Keywords
2007
ISoLA
model checking,b method,state space,validation and verification,formal specification
Field
DocType
Citations 
Formal equivalence checking,Abstraction model checking,Model checking,Programming language,Computer science,Formal specification,Formal verification
Conference
7
PageRank 
References 
Authors
0.55
31
2
Name
Order
Citations
PageRank
Michael Leuschel12156135.89
Daniel Plagge21337.78