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 | 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.