Verification of reactive systems using temporal logic with clocks

This paper presents a framework for the specification and verification of timing properties of reactive systems using Temporal Logic with Clocks (TLC). Reactive systems usually contain a number of parallel processes, therefore, it is essential to study and analyse each process based on its own local...

Full description

Saved in:
Bibliographic Details
Published in:Theoretical computer science 1999-06, Vol.220 (2), p.377-408
Main Authors: Liu, Chuchang, Orgun, Mehmet A.
Format: Article
Language:English
Subjects:
Algorithmics. Computability. Computer arithmetics
Applied sciences
Computer science
control theory
systems
Exact sciences and technology
Theoretical computing
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This paper presents a framework for the specification and verification of timing properties of reactive systems using Temporal Logic with Clocks (TLC). Reactive systems usually contain a number of parallel processes, therefore, it is essential to study and analyse each process based on its own local time. TLC is a temporal logic extended with multiple clocks, and it is in particular suitable for the specification of reactive systems. In our framework, the behavior of a reactive system is described through a formal specification; its timing properties, including safety and liveness properties, are expressed by TLC formulas. We also propose several demonstration techniques, such as an application of local reasoning and deriving fixed-time rules from the proof system of TLC, for proving that a reactive system meets its temporal specification. Under the proposed framework, the timing properties of a reactive system can therefore be directly reasoned about from the formal specification of the system.
ISSN:0304-3975
1879-2294
DOI:10.1016/S0304-3975(99)00008-0