UM  > 科技學院  > 電腦及資訊科學系
Checking interval based properties for reactive systems
Yu, Pei1,3; Qiwen, Xu2
2004
Conference Name5th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2004
Source PublicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2937
Pages122-134
Conference Date1 11, 2004 - 1 13, 2004
Conference PlaceVenice, Italy
Author of SourceSpringer Verlag
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, the satisfaction relation is simply defined by the containment between the set of system behaviors and that of logic models. However, this satisfaction relation does not work for interval temporal logics, where the models can be considered as a set of finite sequences. In this paper, we observe that for different interval based properties, different satisfaction relations are sensible. Two classes of properties are discussed, and accordingly two satisfaction relations are defined, and they are subsequently unified by a more general definition. A tool is developed based on the Spin model checking system to verify the proposed general satisfaction relation for a decidable subset of Discrete Time Duration Calculus. © Springer-Verlag Berlin Heidelberg 2004.

Indexed BySCI
Language英语
WOS Research AreaComputer Science
WOS SubjectComputer Science, Software Engineering ; Computer Science, Theory & Methods
WOS IDWOS:000189213100011
Fulltext Access
Citation statistics
Document TypeConference paper
CollectionDEPARTMENT OF COMPUTER AND INFORMATION SCIENCE
Affiliation1.International Institute for Software Technology, United Nations University, China;
2.University of Macau, China;
3.Department of Computer Science and Technology, Nanjing University, China
Recommended Citation
GB/T 7714
Yu, Pei,Qiwen, Xu. Checking interval based properties for reactive systems[C]//Springer Verlag,2004:122-134.
Related Services
Recommend this item
Bookmark
Usage statistics
Export to Endnote
Google Scholar
Similar articles in Google Scholar
[Yu, Pei]'s Articles
[Qiwen, Xu]'s Articles
Baidu academic
Similar articles in Baidu academic
[Yu, Pei]'s Articles
[Qiwen, Xu]'s Articles
Bing Scholar
Similar articles in Bing Scholar
[Yu, Pei]'s Articles
[Qiwen, Xu]'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.