Managed by P. Bellini
and P. Nesi
service provided by http://www.digits.com/
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.
In the following, a short description of TOTS tool is reported:
For the validation of TILCO specifications within Isabelle, some Isabelle theories have been developed.
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.
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:
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
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:
Visual C++ project for Crossroad Control Simulator
(with built-in Dev-TILCO development process)
Zip file contains a folder (Crossroad Controller Simulator) with: