Sciweavers

Share
ICSE
2008
IEEE-ACM

A verification system for timed interval calculus

10 years 8 months ago
A verification system for timed interval calculus
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 r...
Chunqing Chen, Jin Song Dong, Jun Sun 0001
Added 17 Nov 2009
Updated 09 Dec 2009
Type Conference
Year 2008
Where ICSE
Authors Chunqing Chen, Jin Song Dong, Jun Sun 0001
Comments (0)
books