I.2 Features of ITL
Features of ITL [Slide 12]
- 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 behaviour.
- Supports sequential operators found in programs, etc.
Features of ITL [Slide 13]
- 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.