A verification system for interval-based specification languages

Interval-based specification languages have been used to formally model and rigorously reason about real-time computing systems. This usually involves logical reasoning and mathematical computation with respect to continuous or discrete time. When these systems are complex, analyzing their models by...

Full description

Saved in:
Bibliographic Details
Main Authors: CHEN, Chunqing, DONG, Jin Song, SUN, Jun, MARTIN, Andrew P.
Format: text
Language:English
Published: Institutional Knowledge at Singapore Management University 2010
Subjects:
Online Access:https://ink.library.smu.edu.sg/sis_research/5905
https://ink.library.smu.edu.sg/context/sis_research/article/6905/viewcontent/1734229.1734232.pdf
Tags: Add Tag
No Tags, Be the first to tag this record!
Institution: Singapore Management University
Language: English
Description
Summary:Interval-based specification languages have been used to formally model and rigorously reason about real-time computing systems. This usually involves logical reasoning and mathematical computation with respect to continuous or discrete time. When these systems are complex, analyzing their models by hand becomes error-prone and difficult. In this article, we develop a verification system to facilitate the formal analysis of interval-based specification languages with machine-assisted proof support. The verification system is developed using a generic theorem prover, Prototype Verification System (PVS). Our system elaborately encodes a highly expressive set-based notation, Timed Interval Calculus (TIC), and can rigorously carry out the verification of TIC models at an interval level. We validated all TIC reasoning rules and discovered subtle flaws in the original rules. We also apply TIC to model Duration Calculus (DC), which is a popular interval-based specification language, and thus expand the capacity of the verification system. We can check the correctness of DC axioms, and execute DC proofs in a manner similar to the corresponding pencil-and-paper DC arguments.