Executable Interval Temporal Logic Specifications
This work addresses the problem of system verification and simulation for researchers and engineers in formal methods, but it appears incremental as it builds on existing ITL concepts.
The paper formalizes the executability of Interval Temporal Logic (ITL) specifications, enabling testing and simulation of system behaviors, and investigates how the reflection operator can reverse these executable behaviors.
In this paper the reversibility of executable Interval Temporal Logic (ITL) specifications is investigated. ITL allows for the reasoning about systems in terms of behaviours which are represented as non-empty sequences of states. It allows for the specification of systems at different levels of abstraction. At a high level this specification is in terms of properties, for instance safety and liveness properties. At concrete level one can specify a system in terms of programming constructs. One can execute these concrete specification, i.e., test and simulate the behaviour of the system. In this paper we will formalise this notion of executability of ITL specifications. ITL also has a reflection operator which allows for the reasoning about reversed behaviours. We will investigate the reversibility of executable ITL specifications, i.e., how one can use this reflection operator to reverse the concrete behaviour of a particular system.