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

fYear

1994

fDate

7-9 Dec 1994

Firstpage

266

Lastpage

270

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¹⁵ 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;

fLanguage

English

Publisher

ieee

Conference_Titel

Real-Time Systems Symposium, 1994., Proceedings.

Conference_Location

San Juan

Print_ISBN

0-8186-6600-5

Type

conf

DOI

10.1109/REAL.1994.342709

Filename

342709