Please use this identifier to cite or link to this item:
|Title:||A verification system for timed interval calculus||Authors:||Chen, C.
|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. 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.
checked on Oct 17, 2019
WEB OF SCIENCETM
checked on Oct 10, 2019
checked on Oct 14, 2019
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.