I.3 ITL’s Influence
ITL’s Influence [Slide 14]
- 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
University).
- 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 Temporal Logic.
ITL’s Influence [Slide 15]
- 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).