Analyzing real-time systems
- 1 January 2000
- conference paper
- Published by Association for Computing Machinery (ACM)
- p. 243-249
- https://doi.org/10.1145/343647.343775
Abstract
Temporal logic model checking is a technique for the auto- matic verification of systems against specifications. Besides the correctness of safety and liveness properties it is often important to determine critical answer and delay times of systems, especially if they are embedded in a real-time envi- ronment. In this paper we present an approach which allows the verification as well as the timing analysis of real- time systems. The systems are described as networks of communicating time-extended finite state machines (I/O- interval structures). We use a compact symbolic representa- tion to obtain efficient analysis algorithms. 1Keywords
This publication has 2 references indexed in Scilit:
- Spectral transforms for large boolean functions with applications to technology mappingPublished by Association for Computing Machinery (ACM) ,1993
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986