Models for reactivity

A hierarchy of models that capture realistic aspects of reactive, real-time, 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,...

Full description

Bibliographic Details
Published in:Acta informatica, Vol. 30, No. 7 (1993), p. 609-678
Main Author: Manna, Zohar
Other Involved Persons: Pnueli, Amir
Format: electronic Article
Language:English
ISSN:1432-0525
Item Description:This research was supported in part by the National Science Foundation under grant CCR-92-23226, by the Defense Advanced Research Projects Agency under contract NAG2-703, by the United States Air Force Office of Scientific Research under contract F49620-93-1-0139, by the European Community ESPRIT Basic Research Action Project 6021 (REACT), and by the France-Israel project for cooperation in Computer Science. An extended abstract of this paper appeared in [MP92], while a preliminary version of Section 4 appeared in [MP93].
Physical Description:Online-Ressource
DOI:10.1007/BF01191722
Subjects:
QR Code: Show QR Code
Description:
  • A hierarchy of models that capture realistic aspects of reactive, real-time, 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.