Compositional verification of real-time systems
- 17 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 458-465
- https://doi.org/10.1109/lics.1994.316045
Abstract
Presents a compositional proof system for the verification of real-time systems. Real-time systems are modeled as timed transition modules, which explicitly model interaction with the environment and may be combined using composition operators. Composition rules are devised such that the correctness of a system may be determined from the correctness of its components. These proof rules are demonstrated on Fischer's mutual exclusion algorithm, for which mutual exclusion and bounded response are proven.<>Keywords
This publication has 6 references indexed in Scilit:
- Real-time logics: complexity and expressivenessPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Temporal Proof Methodologies for Timed Transition-SystemsInformation and Computation, 1994
- Specification and Proof in Real Time CSPPublished by Cambridge University Press (CUP) ,1993
- Specification and Compositional Verification of Real-Time SystemsLecture Notes in Computer Science, 1991
- Specifying real-time properties with metric temporal logicReal-Time Systems, 1990
- A temporal-logic based compositional proof system for real-time message passingLecture Notes in Computer Science, 1989