Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

5-2008

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.

Keywords

Real-Time Systems, Specification Language, Theorem Proving, PVS

Discipline

Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the 30th International Conference on Software Engineering (ICSE 2008), Leipzig, Germany, 2008 May 10-18

First Page

271

Last Page

280

ISBN

9781605580791

Identifier

10.1145/1368088.1368126

Publisher

IEEE

City or Country

Germany

Additional URL

https://doi.org/10.1145/1368088.1368126

Download

Share

COinS