TILCOX an Extension of TILCO Temporal Logic

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 efficient 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 specifications 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 specications by using a lower number of quantifications 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 is an extension of TILCO Temporal Interval Logic with Compositional Operators. CTILCO introduces the communication among components specified 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 defined 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.