Please use this identifier to cite or link to this item:
Title: A verification system for timed interval calculus
Authors: Chen, C. 
Dong, J.S. 
Sun, J. 
Keywords: PVS
Real-Time Systems
Specification Language
Theorem Proving
Issue Date: 2008
Citation: Chen, C., Dong, J.S., Sun, J. (2008). A verification system for timed interval calculus. Proceedings - International Conference on Software Engineering : 271-280. ScholarBank@NUS Repository.
Abstract: Timed Interval Calculus (TIC) is a highly expressive set-based notation for specifying and reasoning about embedded real-time systems. However, it lacks mechanical proving support, as its verification usually involves infinite time intervals and continuous dynamics. In this paper, we develop a system based on a generic theorem prover, Prototype Verification System (PVS), to assist formal verification of TIC at a high grade of automation. TIC semantics has been constructed by the PVS typed higher-order logic. Based on the encoding, we have checked all TIC reasoning rules and discovered subtle flaws. A translator has been implemented in Java to automatically transform TIC models into PVS specifications. A collection of supplementary rules and PVS strategies has been defined to facilitate the rigorous reasoning of TIC models with functional and non-functional (for example, real-time) requirements at the interval level. Our approach is generic and can be applied further to support other real-time notations. Copyright 2008 ACM.
Source Title: Proceedings - International Conference on Software Engineering
ISBN: 9781605580791
ISSN: 02705257
DOI: 10.1145/1368088.1368126
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.