Computing quantitative characteristics of finite-state real-time systems
- 1 January 1994
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 266-270
- https://doi.org/10.1109/real.1994.342709
Abstract
Presents a general method for computing quantitative information about finite-state real-time systems. We have developed algorithms that compute exact bounds on the delay between two specified events and on the number of occurrences of an event in a given interval. This technique allows us to determine performance measures such as schedulability, response time, and system load. Our algorithms produce more detailed information than traditional methods. This information leads to a better understanding of system behavior, in addition to determining its correctness. The algorithms presented in this paper are efficiently implemented using binary decision diagrams and have been incorporated into the SMV symbolic model verifier. Using this method, we have verified a model of an aircraft control system with 10/sup 15/ states. The results obtained demonstrate that our method can be successfully applied in the verification of real-time system designs.Keywords
This publication has 5 references indexed in Scilit:
- Building a predictable avionics platform in Ada: a case studyPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Computing quantitative characteristics of finite-state real-time systemsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1994
- A proof system for communicating shared resourcesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1990
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986
- Scheduling Algorithms for Multiprogramming in a Hard-Real-Time EnvironmentJournal of the ACM, 1973