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.
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.