Compositional model checking
Top Cited Papers
- 7 January 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 353-362
- https://doi.org/10.1109/lics.1989.39190
Abstract
A method is described for reducing the complexity of temporal logic model checking in systems composed of many parallel processes. The goal is to check properties of the components of a system and then deduce global properties from these local properties. The main difficulty with this type of approach is that local properties are often not preserved at the global level. The authors 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, the authors can guarantee that these properties will be preserved at the global level. They give two example compositional systems based on the logic CTL.<>Keywords
This publication has 11 references indexed in Scilit:
- A language for compositional specification and verification of finite state hardware controllersProceedings of the IEEE, 1991
- Characterizing Kripke structures in temporal logicLecture Notes in Computer Science, 1987
- Automatic Verification of Sequential Circuits Using Temporal LogicIEEE Transactions on Computers, 1986
- Automatic verification of finite-state concurrent systems using temporal logic specificationsACM Transactions on Programming Languages and Systems, 1986
- “Sometimes” and “not never” revisitedJournal of the ACM, 1986
- Automatic verification of asynchronous circuits using temporal logicIEE Proceedings E Computers and Digital Techniques, 1986
- Checking that finite state concurrent programs satisfy their linear specificationPublished by Association for Computing Machinery (ACM) ,1985
- A Calculus of Communicating SystemsLecture Notes in Computer Science, 1980
- Communicating sequential processesCommunications of the ACM, 1978
- AN n log n ALGORITHM FOR MINIMIZING STATES IN A FINITE AUTOMATONPublished by Elsevier ,1971