Formal techniques for the specification of real time systems must be capable of describing system behavior as a set of relationships expressing the temporal constraints among events and actions, including properties of invariance, precedence, periodicity, liveness, and safety conditions. The paper describes a Temporal-Interval Logic with Compositional Operators (TILCO) designed expressly for the specification of real time systems. TILCO is a generalization of classical temporal logics based on the operators, eventually and henceforth; it allows both qualitative and quantitative specification of time relationships. TILCO is based on time intervals and can concisely express temporal constraints with time bounds, such as those needed to specify real time systems. This approach can be used to verify the completeness and consistency of specifications, as well as to validate system behavior against its requirements and general properties. TILCO has been formalized by using the theorem prover Isabelle/HOL. TILCO specifications satisfying certain properties are executable by using a modified version of the Tableaux algorithm. The paper defines TILCO and its axiomatization, highlights the tools available for proving properties of specifications and for their execution, and provides an example of system specification and validation.

The Temporal Interval Logic with Compositional Operators (TILCO) has been especially designed for the specification and validation of real-time systems. TILCO extends the classical temporal logics based on the operators eventually, and henceforth by using time intervals in order to allow the specification of both qualitative and quantitative temporal relationships. The use of time intervals also supports an abstract and synthetic style for specifying real-time systems. The validation of TILCO specifications is supported by means of property proving; direct execution of specifications and model-checking of system histories are also possible. Therefore, the TILCO model can be considered as a dual approach. This paper describes TILCO and shows with an example its application for the specification and validation of real-time systems. Highlights about the TILCO axiomatization are given and the tools available for proving properties of specifications and for specifications execution are discussed.

High level operational languages support the specification and validation of complex reactive systems through the automatic generation of rapid prototypes since the early stages of the development lifecycle. However, when it comes to the implementation stage, these prototypes must be translated into target code to accomplish performance requirements without losing validation results. A transformation method supporting the incremental and automatic transition from rapid prototypes to target code is presented, which relies on a Petri net based specification language. Experimental results are presented to evaluate the performance improvement achieved by this automatic transformation.>

A framework for the development of distributed object-oriented systems in heterogeneous environments is presented. This model attempts to incorporate concepts of distributed computing technology together with software engineering methods. A tool has been developed to enforce the model by means of a high-level specification language and an automatic code generator. However, it is emphasized that the model may be exploited as a methodologic foundation even outside an automatic generation approach.>