QRDChecker: A model checking tool for QRDC

Yu Pei, Qi Wen Xu, Xuan Dong Li, Guo Liang Zheng

Research output: Journal article publicationJournal articleAcademic researchpeer-review

Abstract

A reactive system does not terminate and its behaviors are typically defined as a set of infinite sequences of states. In formal verification, a requirement is usually expressed in a logic, and when the models of the logic are also defined as infinite sequences, such as the case for LTL (linear temporal logic), the satisfaction relation is simply defined by the set containment. However, this satisfaction relation does not work for interval temporal logics, where the models are finite sequences. In fact, for different interval based properties, different satisfaction relations are sensible. Two classes of finitary properties are identified, and then two satisfaction relations are defined for them, which are unified by a general relation. A model checking algorithm is proposed and implemented in a verification tool for QRDC (quantified RDC (restricted duration calculus)), which is an interval temporal logic. The tool QRDChecker can check the validity of QRDC formulae under both continuous and discrete interpretations. Moreover, for discrete QRDC, it can also translate the formulae into an automaton in the form accepted by the Spin model checking system, which can be subsequently used to verify a reactive system against properties expressed in the logic.
Original languageEnglish
Pages (from-to)355-364
Number of pages10
JournalRuan Jian Xue Bao/Journal of Software
Volume16
Issue number3
DOIs
Publication statusPublished - 1 Mar 2005
Externally publishedYes

Keywords

  • Finitary property
  • Interval temporal logic
  • Model checking
  • Reactive system

ASJC Scopus subject areas

  • Software

Cite this