Contents:
General
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.
- Slides in Italian regarding TILCOX
- slides in Italian regarding the general aspects
- slides in Italian regarding all aspects (Ph.D. Doctorate of P. Bellini)
- Ph.D. Thesis of P. Bellini
- TOTS tools
In the following, a short description of TOTS tool is 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.
- Interval.thy extends the integers theory to define constant intervals.
- Tilco.thy extends Interval.thy to define all the operator of logic TILCO.
- 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.
- 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