An Approach to Compositional Model Checking

A natural trend in most of the engineering disciplines is the construction of systems from components. This has the potential to reduce costs and increase reliability, provided that the components can be specified and verified in such a way that it is possible to reason about the composed system. In this paper, we explore an approach to compositional reasoning that uses model checking to verify component specifications and deduction to verify the constraints that a component imposes on the system in which it is embedded. We use CTL as the specification language along with the SMV model checker.

• Type: Conference
• Year: 2002
• Where: IPPS
• Authors: Hector A. Andrade, Beverly Sanders
• Keywords: Distributed And Parallel Computing, Engineering Disciplines, IPPS 2002, Natural Trend, SMV Model Checker