A dense-time temporal logic with nice compositionality properties
Date
1997-02
Authors
Advisors
Journal Title
Journal ISSN
ISSN
0302-9743
Volume Title
Publisher
Type
Article
Peer reviewed
Abstract
A dense temporal logic specification method for the development of reactive systems is introduced. The two development constructs of this method are refinement and composition. A reactive system is specified by a pair consisting of a machine and a condition on the computations of this machine. In order to compose such systems compositionally, each machine step contains additional information such as, “this is a system step”, or “this is an environment step” or “this is a communication step”. Compositionality enables us to break refinement between complex systems into refinement between small and simple systems. The latter can then be verified by existing proof rules for refinement which are reformulated in our formalism.
Description
Keywords
Citation
Cau, Antonio and Roever, W.-P. de, A dense-time temporal logic with nice compositionality properties. In: Computer aided systems theory, EUROCAST '97: a selection of papers from the 6th International Workshop on Computer Aided Systems Theory, Las Palmas de Gran Canaria, Spain, February 1997. Editors: Franz Pichler and Roberto Moreno Diaz, Berlin: New York: Springer, 1997, Lecture notes in computer science, vol 1333. pp. 123-145.