QRDChecker: A model checking tool for QRDC
Pei Y.1; Xu Q.-W.2; Li X.-D.1; Zheng G.-L.1
Source PublicationRuan Jian Xue Bao/Journal of Software
AbstractA 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.
KeywordFinitary property Interval temporal logic Model checking Reactive system
URLView the original
Fulltext Access
Citation statistics
Document TypeJournal article
CollectionUniversity of Macau
Affiliation1.Nanjing University
2.Universidade de Macau
Recommended Citation
GB/T 7714
Pei Y.,Xu Q.-W.,Li X.-D.,et al. QRDChecker: A model checking tool for QRDC[J]. Ruan Jian Xue Bao/Journal of Software,2005,16(3):355-364.
APA Pei Y.,Xu Q.-W.,Li X.-D.,&Zheng G.-L..(2005).QRDChecker: A model checking tool for QRDC.Ruan Jian Xue Bao/Journal of Software,16(3),355-364.
MLA Pei Y.,et al."QRDChecker: A model checking tool for QRDC".Ruan Jian Xue Bao/Journal of Software 16.3(2005):355-364.
Related Services
Recommend this item
Usage statistics
Export to Endnote
Google Scholar
Similar articles in Google Scholar
[Pei Y.]'s Articles
[Xu Q.-W.]'s Articles
[Li X.-D.]'s Articles
Baidu academic
Similar articles in Baidu academic
[Pei Y.]'s Articles
[Xu Q.-W.]'s Articles
[Li X.-D.]'s Articles
Bing Scholar
Similar articles in Bing Scholar
[Pei Y.]'s Articles
[Xu Q.-W.]'s Articles
[Li X.-D.]'s Articles
Terms of Use
No data!
Social Bookmark/Share
All comments (0)
No comment.

Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.