Verification of reactive systems using temporal logic with clocks

Chuchang Liu*, Mehmet A. Orgun

*Corresponding author for this work

Research output: Contribution to journalArticle

14 Citations (Scopus)

Abstract

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.

Original languageEnglish
Pages (from-to)377-408
Number of pages32
JournalTheoretical Computer Science
Volume220
Issue number2
Publication statusPublished - 17 Jun 1999

Fingerprint Dive into the research topics of 'Verification of reactive systems using temporal logic with clocks'. Together they form a unique fingerprint.

  • Cite this