Title :
Computing quantitative characteristics of finite-state real-time systems
Author :
Campos, S. ; Clarke, E. ; Marrero, W. ; Minea, M. ; Hiraishi, H.
Author_Institution :
Sch. of Comput. Sci., Carnegie Mellon Univ., Pittsburgh, PA, USA
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 1015 states. The results obtained demonstrate that our method can be successfully applied in the verification of real-time system designs
Keywords :
aircraft control; delays; diagrams; finite state machines; formal verification; performance evaluation; processor scheduling; real-time systems; symbol manipulation; SMV; aircraft control system; binary decision diagrams; delay; event occurrences; exact bounds; finite-state real-time systems; performance measures; quantitative characteristics; real-time system design verification; response time; schedulability; symbolic model checking; symbolic model verifier; system behavior; system correctness; system load; Aircraft control; Algorithms; Delay effects; Finite state machines; Real time systems;
Conference_Titel :
Real-Time Systems Symposium, 1994., Proceedings.
Conference_Location :
San Juan
Print_ISBN :
0-8186-6600-5
DOI :
10.1109/REAL.1994.342709
