Induction in the Timed Interval Calculus |
| |
Authors: | Axel Wabenhorst |
| |
Affiliation: | Software Verification Research Centre, The University of Queensland, QLD 4072, Australia |
| |
Abstract: | The Timed Interval Calculus, a timed-trace formalism based on set theory, is introduced. It is extended with an induction law and a unit for concatenation, which facilitates the proof of properties over trace histories. The effectiveness of the extended Timed Interval Calculus is demonstrated via a benchmark case study, the mine pump. Specifically, a safety property relating to the operation of a mine shaft is proved, based on an implementation of the mine pump and assumptions about the environment of the mine. |
| |
Keywords: | Real-time specification and reasoning Interval logic Temporal logic Induction Timed traces |
本文献已被 ScienceDirect 等数据库收录! |
|