Models for Reactivity
Abstract
A hierarchy of models that capture realistic aspects of reactive, realtime, and hybrid systems is introduced. On the most abstract level, the qualitative (non-quantitative) model of reactive systems captures the temporal precedence aspect of time. A more refined model is that of real-time systems, which represents the metric aspect of time. The third and most detailed model is that of hybrid systems, which allows the incorporation of continuous components into a reactive system. For each of the three levels, we present a computational model, a requirement specification language based on extensions of temporal logic, system description languages based on Statecharts and a textual programming language, proof rules for proving validity of properties, and examples of such proofs. Temporal logic, Reactive systems, Real-time, Specification, Verification, Hybrid systems, Proof rules, Statecharts
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 07, 1993
- Accession Number
- ADA266419
Entities
People
- Amir Pnueli
- Zohar Manna
Organizations
- Stanford University