Computing quantitative characteristics of finite-state real-time systems
Published 1 January 1994
Campos, Clarke, Marrero, Marius Minea, Hiraishi
Citations80
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
Using this method, a model of an aircraft control system with 10/sup 15/ states is verified and it is demonstrated that the method can be successfully applied in the verification of real-time system designs.
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
Computer Science
IEEE Transactions on ComputersGraph-Based Algorithms for Boolean Function Manipulation
8,829 Citations1986Bryant
Experimental results from applying a new data structure for representing Boolean functions and an associated set of manipulation algorithms to problems in logic design verification demonstrate the practicality of this approach.
Journal of the ACMScheduling Algorithms for Multiprogramming in a Hard-Real-Time Environment
8,334 Citations1973C. L. Liu, J. W. Layland
ACM Transactions on Programming Languages and SystemsAutomatic verification of finite-state concurrent systems using temporal logic specifications
3,555 Citations1986E. M. Clarke, E. Allen Emerson +1 more
It is argued that this technique can provide a practical alternative to manual proof construction or use of a mechanical theorem prover for verifying many finite-state concurrent systems.
Elsevier eBooksScheduling Algorithms for Multiprogramming in a Hard-Real-Time Environment
3,241 Citations2002C. L. Liu, J. W. Layland
Information and ComputationSymbolic model checking: 1020 States and beyond
2,674 Citations1992Jerry R. Burch, E. M. Clarke +3 more
It is shown how the novel mu-calculus model checking algorithm can be used to derive efficient decision procedures for CTL model checking, satisfiability of linear-time temporal logic formulas, strong and weak observational equivalence of finite transition systems, and language containment of finite omega -automata.
Munich Personal RePEc Archive (Ludwig Maximilian University of Munich)Symbolic model checking: an approach to the state explosion problem
980 Citations1992Kenneth L. McMillan
Model-checking for real-time systems
890 Citations2002Rajeev Alur, Costas Courcoubetis +1 more
An algorithm is developed for model checking, that is, for determining the truth of a TCTL formula with respect to a timed graph, and it is argued that choosing a dense domain, instead of a discrete domain, to model time does not blow up the complexity of the model-checking problem.
Lecture notes in computer scienceLogics and models of real time: A survey
553 Citations1992Rajeev Alur, Thomas A. Henzinger
This work surveys logic-based and automata-based languages and techniques for the specification and verification of real-time systems and discusses three syntactic extensions of temporal logic: time-bounded operators, freeze quantification, and time variables.
Lecture notes in computer scienceReal-Time: Theory in Practice
353 Citations1992J. W. de Bakker, Huizing, C. +2 more
Lecture notes in computer scienceQuantitative temporal reasoning
173 Citations2005E. Allen Emerson, Aloysius K. Mok +2 more
Building a predictable avionics platform in Ada: a case study
154 Citations2002C. Douglass Locke, David R. Vogel +1 more
The authors describe this avionics case study and its goals, examine the resulting design issues and trade-offs, and investigate the ability of the rate monotonic analysis model to predict its performance under a heavy load.
Foundations of Real-Time Computing: Scheduling and Resource Management
107 Citations1991André M. Van Tilborg, Gary M. Koob
This paper presents real-Time, Priority-Ordered, Deadlock Avoidance Algorithms, which describe the design and analysis of processor Scheduling Policies for Real-Time Systems and some of the strategies adopted in Spring.
Rate Monotonic Analysis for Real-Time Systems
93 Citations1991Lui Sha, Mark Klein +1 more
As a mathematical discipline travels far from its empirical source, or still more, if it is a second and third generation only indirectly inspired by the ideas coming from ‘reality,’ it is beset with very grave dangers.
Computing quantitative characteristics of finite-state real-time systems
80 Citations1994Campos, Clarke +3 more
Using this method, a model of an aircraft control system with 10/sup 15/ states is verified and it is demonstrated that the method can be successfully applied in the verification of real-time system designs.
Fixed Priority Scheduling Theory for Hard Real-Time Systems
65 Citations1991John P. Lehoczky, Lui Sha +2 more
The Liu and Layland theory of rate monotonic scheduling is presented along with many generalizations including an exact characterization of task set schedulability, average case behavior and allowance for arbitrary task deadlines.
Real-Time Symbolic Model Checking for Discrete Time Models
61 Citations1994Sérgio Campos, Edmund M. Clarke
The BDD-based symbolic model checking algorithm given in (4.10) is extended to handle real-time properties using the bounded until operator (9) and it is believed that this algorithm which is based on discrete time is able to handle many real- time properties that arise in practical problems.
RTSL: a language for real-time schedulability analysis
42 Citations2002Andre N. Fredette, Rance Cleaveland
The paper develops a generalized approach to schedulability analysis that is mathematically founded in a process algebra called RTSL that allows the reachable state space of finite state systems to be automatically generated and searched for timing exceptions.
A proof system for communicating shared resources
17 Citations1990R. Gerber, I. Lee
The authors introduce a proof system for CCSR, a process algebra based on the CSR model, which allows the algebraic specifications of timeouts, interrupts, periodic behaviors and exceptions and a rigorous treatment of preemption.