Execution of TILCO Specifications Technical Report

Formal techniques for the specication 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 specication 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 specication 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 specications by using a lower number of quantications and of nesting levels between temporal operators This paper denes 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 decompositioncomposition mechanisms TILCO has been expressly designed for the specication 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 specications as well as to validate system behavior against its requirements and general properties CTILCO has been formalized by using the theorem prover IsabelleHOL CTILCO specications satisfying certain properties are executable CTILCO is dened in terms of theorems and allows the system specication and the formal proof of properties including compositiondecomposition with communications An example of system specication and validation has been also included.