| || |
This course will give a not so short introduction to Interval Temporal Logic (ITL)
ITL is a
- discrete, linear temporal logic
- for both finite and infinite intervals (sequences of states) which includes
- a basic construct for sequential composition and
- an analog of Kleene star (regular expressions)
- Combines temporal logic, automata and regular expressions
- Modular reasoning about time (e.g., hardware, software, multimedia)
- Flexible notation for discrete linear order
- Analytical framework for going from infinite-time behaviour to finite-time
- Supports sequential operators found in programs, etc.
- Compositionality with assumptions and commitments
- Refinement to derive concrete programs from abstract specifications.
- ITL with memory and framing can embed various kinds of imperative programs,
including parallel ones.
- Executable specifications and imperative subsets.
- Temporal projection between different time granularities; enables imperative
constructs for interleaved processes.
- ITL helped influence Prof Mike Gordon, FRS to switch from LCF to HOL in his
theorem proving tools. (E.g., see his article From LCF to HOL: A short history).
- Hybrid systems: Duration Calculus (real and discrete time).
- ITL is used to give semantics to Verilog (EPSRC project with Oxford
- ITL is used in hardware/software codesign (EPSRC projects with University of
Newcastle upon Tyne and Oxford University).
- ITL is used for security and trust policies (DTC-DIF projects).
- ITL used in the projects Safemos (UK) and ProCoS (EU).
- Mexitl (Kent, Winnipeg) is based on ITL, Multimedia in Executable Interval
- AnaTempura runtime verification tool uses executable subset of ITL.
- Influenced Verisity Ltd.’s language temporal e (part of IEEE Standard 1647).
Verisity acquired by Cadence Design Systems, Inc., a major supplier of
electronic design tools and services.
- Used in the KIV theorem prover (University of Augsburg, Germany) - e.g., for
Statecharts, UML and medical protocols.
- ITL with framing and temporal projection extensively studied by Duan and group
(Xidian University, Xi’an, China).