Inerval Temporal Logic for real-Time Systems: Specification, Execution and Verification Processes

Formal techniques for the specification of realtime systems must be capable of describing temporal constraints among events and actions properties of invariance precedence periodicity repeated occurrences liveness and safety conditions etc This paper describes an evolution of the Temporal Interval Logic called TILCO TILCO is a generalisation of classical temporal logics based on the operators eventually and henceforth and allows both qualitative and quantitative specification of time relationships TILCO is based on time intervals and can concisely express temporal constraints with time bounds TILCO is strongly concise and ecient for the specification of realtime systems In this paper an extension of TILCO called TILCOX is presented TILCOX proposes two new operators that increase conciseness and readability of specications allowing to describe (i) ordering of events without distinction between past and future and (ii) predicates depending on the number of occurrences of events in intervals TILCOX is capable of describing specifications by using a lower number of quantications and of nesting levels between temporal operators This paper defines the semantics of TILCOX and related examples that show the power of the model proposed. CTILCO an extension of TILCO Temporal Interval Logic with Compositional Operators CTILCO introduces the communication among components specied in TILCO and allows the adoption of decomposition / composition mechanisms TILCO has been expressly designed for the specification of realtime systems CTILCO is based on time intervals and can concisely express temporal constraints with time bounds such as those needed to specify realtime systems It can be used to verify the completeness and consistency of specifications as well as to validate system behavior against its requirements and general properties CTILCO has been formalized by using the theorem prover Isabelle/HOL CTILCO specifications satisfying certain properties are executable CTILCO is dened in terms of theorems and allows the system specification and the formal proof of properties including composition / decomposition with communications An example of system specification and validation has been also included.