Homepage

TILCO web page (Temporal Interval Logic with Compositional Operators)

Formal methods should be adopted since the early phases of the system development to reduce failures in the final software product.
In the specification phase, many languages/formalisms could be used to specify the system under development. For real-time systems, where the specification is focussed on modelling system behavior in response of external stimuli, one of the possible approaches consists in using logical statements to describe what the system has to do.This is a different modality of specification with respect to operational approaches which are based on producing descriptions focussed on how the system does certain operations.
For the specification of real-time systems formal frameworks are typically used. A formal framework is based on a formal model that allow representing the system under specification and a set of tools aids the model verification. Two kinds of specification verification can be present: verification by using property proof and verification by simulation.
Verification by using property-proof permits to prove properties for the system. For example, given the specification of a system it permits to demostrate if a deadlock will never happen. Property-proof is particularly important for safety-crytical systems where some critical situations have to be absolutelly avoided.
In a framework based on a logical language, properties and the specification are expressed using the same logic language.
 
To prove a property means to demonstrate the property by using the logical specification. To this extent, theorem provers could be adopted to mechanically derive these proofs or at least to aid the user in such a work.
Temporal logics are extensions of propositional/first order logics to deal with time constraints, such as ordering of events (i.e., one event has to occur before another) or quantitative constraints (i.e., something has to occur within 10ms). In the past, many temporal logics were presented: in particular TILCO (Temporal Interval Logic with Compositional Operators) (R. Mattolini, P. Nesi, ``An Interval Logic for Real Time System Specification) is specifically suitable for real-time systems specification.
 
Click here to get the TILCO Theory in Isabelle.
 
Temporal logics are well suited to describe temporal constraints while they are not particularly appropriate to describe system structure. For this reason, CTILCO (Communicating TILCO) has been introduced as an extension of TILCO. CTILCO describes the system as a set of communicating processes where each process can be furtherly decomposed or specified by using TILCO to express its behavior. This approach defines a composition/decomposition specification methodology supported by verification. CTILCO permits specification reuse (in the same project or in other projects). Moreover, a synchronous communication model has been defined in TILCO and communication theorems have been proved to permit to demonstrate properties concerning communicating processes.
Click here to get the CTILCO Theory in Isabelle.
Even if TILCO is well suited for real-time systems specification it has been furtherly enhanced with new operators to simplify the expression of temporal constraints(TILCOX). That paper includes the deductive system of TILCOX. To this end, a new proof system has been developed within the Isabelle/HOL theorem prover.

Click here to get the TILCOX Theory in Isabelle.


As already mentioned property-proof is not the only validation support used during the specification, even simulation could be adopted. With system simulation the behavior of the system (or part of it) is tested to see its response to certain stimuli.
In this case, only a small part of the system behavior is tested. Simulation is naturally used with operational specification languages (state machines, Petri nets, etc.), while simulation or execution is not natural for denotational formalisms such as logical specification languages. In these languages, given the history of inputs, execution means to find the history of outputs which satisfy the specification. Some problems may arise, (i) the history of outputs could not be univocally determined; (ii) the specification could be partial, that is the value of an output may not be specified in some instants; (iii) the value of an output may depend on the value of a future input (non-causal specification).
The execution of specifications formalized in temporal logics may not be limited to system simulation; in some cases, it may be used even for system implementation when some temporal constraints are satisfied and the specification is complete and causal.
In traditional approaches, the system hardware executes a program written in a programming language as C, C++, Ada. This source-code is generated from an executable specification (i.e., Petri nets) and generally it uses services of the operating system for time scheduling of the actions to be done.
In our approach the system hardware executes a general inferential engine that given the specification and inputs, produces the outputs. The problem in this case is to produce the outputs at the correct time.
An executor for propositional TILCO and TILCOX has been developed. Specifications written in TILCO and TILCOX are translated in a simple temporal logic (BTL) with only and, or, not and delay operators and transformed in a temporal inference network.
For such a network, inference rules have been defined to infer from the input values the output values.
As regard real-time execution, it has been found that for a causal specification the time needed to produce the outputs at a time $t$ knowing the inputs at time t, t-1, t-2,... is proportional to the number of arcs of the inferential network. Thus the real-time execution can be feasible depending on the network size and the system hardware. This is a strongly innovative result in the field of formal methods since there exist only few temptatives of defining execution engines for non trivial temporal logic specifications.
 
 
For the validation of TILCO, TILCO-X and C-TILCO specifications some tools have been developed. These tools are used to aid the validation of specifications by means of theorem-proving (using Isabelle) and/or by simulation using the temporal logic executor. In Figure~\ref{fig:tots}, the relationships between the developed tools are represented.
In the following, a short description of TOTS toolis reported:
  • Isabelle is the validation environment, via property proof, for TILCO specifications, Isabelle theories for TILCO, TILCO-X and C-TILCO have been developed and are used for the validation of specifications.
  • Giselle is a graphic user interface for Isabelle, its aim is to aid the interaction with Isabelle that is a text oriented application;
  • TILCOX2TIN is a translator, it reads textual specifications written in TILCO/TILCO-X and produces a temporal inference network (TIN) for executing the specification.
  • TIN Edit is a graphic editor for the visual specification of system properties. It permits the direct production of TIN files, it supports the basic components of TINs (joint, gate, delay, signal) and moreover other components such as @ and ? (over constant intervals) can be used and also generic sub-nets can be defined and used.
  • TINX is the executor. Basically, it gets in input the TIN file that contains the specification. Then it is capapble of reading the inputs and producing the outputs according to the specification.
  • Sgn Edit is a signal editor. It permits to create, view, and change the files representing the inputs/outputs of the system.
 

Isabelle TILCO Theories
For the validation of TILCO specifications within Isabelle, some Isabelle theories have been developed.
TILCO theory
  • Interval.thy extends the integers theory to define constant intervals.
  • Tilco.thy extends Interval.thy to define all the operator of logic TILCO.
C-TILCO theory
  • PPorts.thy extends the TILCO theory to provide primitive ports that permit to send/receive messages. It represents the low-level communication layer.
  • Ports.thy extends PPorts.thy to provide synchronous ports that permit to send/receive messages synchronously. It represents the high-level communication layer.
  • Process.thy extends Ports.thy to provide the concept of process with its variables, parameters, sub-processes.
TILCO-X theory
  • Time.thy extends the integers theory to provide the basic logical operators (and, or, not, forall, exists, etc.) over temporal variables.
  • IntervalX.thy extends Time.thy to provide the concept of dynamic intervals, it defines the after and before operators.
  • TilcoX.thy extends IntervalX.thy to provide at and happen operators as well as the other temporal operators with exception of Bounded Happen.
  • TilcoXX.thy extends TilcoX.thy to provide Bounded Happen operators.
 

Giselle
Giselle is a graphic user interface for Isabelle. Isabelle is a text oriented application, then to increase the usability the user interface called Giselle has been developed. Other user interfaces for Isabelle can be found (Proof General, XIsabelle) but are plug-ins for Emacs/X-Emacs or use tcl/tk.
The main window of Giselle is divided in tree parts: on the left, there is the current proof state; on the right, the tactics applied to the goal (the property to be proved) that produced the current proof state are reported; on the bottom, there are the tactics that can be applied to the current proof state. Clicking on a button a dialog appears where arguments of the tactic can be chosen.
The interface to tactics is completely configurable. In a textual configuration file, there is, for each tactic, its textual form and the corresponding user inputs are highlighted.
In Giselle, it is also possible to see the proof tree, where is reported how a particular sub-goal has been proved.
 

TIN Edit
The TIN Editor is a graphic editor that permits the visual creation of temporal inference networks. It can be regarded as a visual specification interface for TILCO.
The main characteristics of the TIN editor are:
  • it permits the construction of the TIN using the basic elements as joint, gate, delay, always and signals, connecting them together with arcs;
  • it permits to use non basic elements as the @ and the ? operators;
  • it permits to use TIN networks within another network, giving the possibility of decomposition/composition of the system specification;
  • it permits to save/load/print the networks;
  • it checks if some information is missing (the value of a delay, or the intervals of the at component, etc.).
  • it permits to generate the .tin file for the TINX executor.
 

TINX
TINX is the temporal logic executor, it executes the specification written in a .tin file describing the temporal inference network of the system. Each input/output signal is associated with a file .io where the values of the signal are stored. TINX reads the .io files of input signals and produces .io files of output signals.
A .tin file is a textual representation of the network. In the file the list of nodes of the network is reported. For each node, there is a line with the following form:
<node name>: <node type>; <parent node>,<left son>[,<right son>]
where: <node name> is the unique node name, <parent node>, <left son> and <right son> are name references to other nodes.
<node type> can be: G for a gate node, J for a joint node, D for a delay node eventually followed by an integer representing the delay value.
The executor can generate also a log where the events generated during execution are reported. Optionally the execution can be made by using only causal inference.
The values of a signal can be changed by clicking on the desired time instant and the logical value toggles form true to false, from false to undefined and from undefined to true. The values can be changed also selecting a portion of the signal and these instants can be forced to assume value all true, false, undefined, randomly true or false, or alternating true/false values. The executor can be directly invoked from the menu to quickly see the response of the system when an input signal is changed.
Technical report about the execution of TILCO specification
 

Dev-TILCO
Dev-TILCO is an integrated development environment for TILCO and C++. It allows the specification and implementation in TILCO of the timing constraints that can directly manage C++ applications. With this hybrid development system is possible to specify real-time constraints in TILCO for process and system control, to verify and validate them formally with Isabelle, to validate them with TINX performing history checking and finally to directly execute the TILCO specification by integrating the TILCO-Executor in your C++ software. Dev-TILCO integrates benefits of several approaches: denotational models, property proof, verification of histories, direct execution, and traditional programming language. A case study has been succesfully developed with such a development system and sources of the development are collected in a ZIP file.
Technical report about Dev-TILCO
Tecnical report about an example of development: Crossroad Control Simulator
Slide-show about Dev-TILCO and an application example (italian language)
Crossroad Control Simulator: an application developed with Dev-TILCO
Zip file contains a folder (Crossroad Executable) with:
  • Crossroad Controller Simulator.exe: the application
  • crossoroad.tin: Temporal Inference Network which model the crossroad behaviour
  • crossoroad_ic.evl: Initial conditions for the inference
Visual C++ project for Crossroad Control Simulator (with built-in Dev-TILCO development process)
Zip file contains a folder (Crossroad Controller Simulator) with:
  • Crossroad Controller Simulator.dsw & dspVisual C++ workspace and project
  • crossroad.tilco: Crossroad behaviour specification in TILCO
  • cross_con.th: Declaration file with the suitable interface object
  • *.cpp, *.h and other resources: application code and customized code for interface
  • README.txt: some useful instruction to properly use Dev-TILCO Tools
 

... Some Selected Related papers:
  • G. Bucci, M. Campanai, and P. Nesi, ``Tools for specifying real-time systems,''  Journal of Real-Time Systems, vol. 8, pp. 117--172, March 1995, also reprinted in Key Successful Software Development Readings, IEEE (1999) and in A Practical Approach to Real Time Systems, IEEE (P. Laplante, ed.) (1999).
  • R. Mattolini and P. Nesi, ``An interval logic for real-time system  specification,'' IEEE Transactions on Software Engineering, in press,  March-April, 2001.
  • P. Bellini, R. Mattolini, and P. Nesi, ``Temporal logics for real-time system  specification,'' ACM Computing Surveys, vol. 32, N.1, pp.12-42, March 2000.
  • P. Nesi and M. Campanai, ``Metric framework for object-oriented real-time  systems specification languages,'' The Journal of Systems and Software,  vol. 34, pp. 43--65, 1996.
  • P. Bellini, M. Bruno, and P. Nesi, ``Verification criteria for a compositional  model for reactive systems,'' Proc. of the IEEE Intern. Conf.  on Complex Computer Systems, Sept. 11-15 2000.
  • P. Bellini, M. A. Bruno, P Nesi, ``Verification of External Specifications of Reactive Systems'', IEEE Transactions on Systems Man and Cybernetics, IEEE Press, USA, in  press 2000 or 2001.
  • M. A. Bruno, P. Nesi, ``Life-Cycle of a formal Dual Object-Oriented Specification Model for Real-Time Systems'', Journal of Information and Software Technology,  Elsevier Publishers, USA, Vol.41, N.1, pp.35-52, 1999.
  • R. Mattolini, P. Nesi, ``Using TILCO for Specifying Real-Time Systems", Proc. of the 2nd IEEE International Conference on Engineering of Complex Computer Systems, ICECCS'96, IEEE Press, Montreal, Canada, October 1996.
 
0
Your rating: None