file.pdf (1.02 MB)
Download file

Compositional model checking

Download (1.02 MB)
journal contribution
posted on 01.10.1997, 00:00 authored by E. M. Clarke, D. E. Long, K. L. McMillan
Abstract: "We describe a method for reducing the complexity of temporal logic model checking in systems composed of many parallel processes. Thegoal is to check properties of the components of a system and then deduce globalproperties from these local properties. The main difficulty with this type of approach is that local properties are often not preserved at the global level. We present a general framework for using additional interface processes to model the environment for a component. These interface processes are typically much simpler than the full environment of the component. By composing a component with its interface processes and then checking properties of this composition, we can guarantee that these properties will be preserved at the global level. We give two example compositional systems based on the logic CTL."


Publisher Statement

Copyright 1997 Society of Photo-Optical Instrumentation Engineers. One print or electronic copy may be made for personal use only. Systematic reproduction and distribution, duplication of any material in this paper for a fee or for commercial purposes, or modification of the content of the paper are prohibited



Usage metrics