Please use this identifier to cite or link to this item: https://doi.org/10.1145/1368088.1368126
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
Source: 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. https://doi.org/10.1145/1368088.1368126
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
URI: http://scholarbank.nus.edu.sg/handle/10635/40042
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.

SCOPUSTM   
Citations

5
checked on Dec 14, 2017

WEB OF SCIENCETM
Citations

5
checked on Nov 19, 2017

Page view(s)

53
checked on Dec 10, 2017

Google ScholarTM

Check

Altmetric


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