A verification system for timed interval calculus

• Main Authors: CHEN, Chunqing, DONG, Jin Song, SUN, Jun
• Format: text
• Language: English
• Published: Institutional Knowledge at Singapore Management University 2008
• Subjects: Real-Time Systems; Specification Language; Theorem Proving; PVS; Software Engineering
• Online Access: https://ink.library.smu.edu.sg/sis_research/4963; https://ink.library.smu.edu.sg/context/sis_research/article/5966/viewcontent/1368088.1368126.pdf
• Institution: Singapore Management University

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.