Please use this identifier to cite or link to this item:
Title: A verification system for interval-based specification languages
Authors: Chen, C. 
Dong, J.S. 
Sun, J. 
Martin, A.
Keywords: Formal specification languages
Real-time systems
Theorem proving
Issue Date: 2010
Citation: Chen, C., Dong, J.S., Sun, J., Martin, A. (2010). A verification system for interval-based specification languages. ACM Transactions on Software Engineering and Methodology 19 (4). ScholarBank@NUS Repository.
Abstract: Interval-based specification languages have been used to formally model and rigorously reason about real-time computing systems. This usually involves logical reasoning and mathematical computation with respect to continuous or discrete time. When these systems are complex, analyzing their models by hand becomes error-prone and difficult. In this article, we develop a verification system to facilitate the formal analysis of interval-based specification languages with machine-assisted proof support. The verification system is developed using a generic theorem prover, Prototype Verification System (PVS). Our system elaborately encodes a highly expressive set-based notation, Timed Interval Calculus (TIC), and can rigorously carry out the verification of TIC models at an interval level. We validated all TIC reasoning rules and discovered subtle flaws in the original rules. We also apply TIC to model Duration Calculus (DC), which is a popular interval-based specification language, and thus expand the capacity of the verification system. We can check the correctness of DC axioms, and execute DC proofs in a manner similar to the corresponding pencil-and-paper DC arguments. © 2010 ACM.
Source Title: ACM Transactions on Software Engineering and Methodology
ISSN: 1049331X
DOI: 10.1145/1734229.1734232
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

Google ScholarTM



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