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.


checked on Nov 18, 2019


checked on Nov 18, 2019

Page view(s)

checked on Oct 28, 2019

Google ScholarTM



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