The application of formal
methods to the development of validated embedded systems mainly
concentrates on specification
languages, with
semantics adequate to support implementation and
verification, and
methods and tools for verifying specifications with respect to
properties expressed in suitable formalisms.
Specification formalisms.
The concept of reactivity has been proposed by Harel and
Pnueli to describe one of the main
characteristics of embedded systems.
Such systems continuously interact with their environment.
Reactivity means that the system must respond to stimuli, issued
by the environment at an instant, within a bounded time, at least
within the next instant, so that reactions do not overlap.
Synchronous formalisms are based on the synchronous hypothesis
[5] which states that reactions of a system are instantaneous.
This hypothesis simplifies reasoning about reactive systems and presents at
least two advantages.
The first is that the construct of parallel composition does not give rise to
nondeterminism, namely the various components of a system act
synchronously and their actions cannot arbitrarily interleave.
The second is that there is no
special construct to deal with physical time, but this
is replaced by a notion of ordering among
events.
On the other hand, a problem common to all synchronous formalisms due to the
assumption of instantaneous communication are paradoxes of causality between
communicated signals,
such that system reaction may be not defined or not unique.
Synchronous formalisms can be classified in three classes. State oriented formalisms, such as the visual formalisms Statecharts and Argos and the imperative language Esterel, are tailored for systems where the control handling aspects are predominant. Data-flow formalisms, such as the languages Lustre and Signal, are tailored for systems where the data processing aspects are predominant. Constraint based formalisms, such as Timed Concurrent Constraint Programming (TCCP) and Timed Default Concurrent Constraint Programming (TDCCP) integrate synchronous programming with the programming by constraint paradigm.
Statecharts and Argos, which extend automata with hierarchy of states, parallelism and broadcast communication, are endowed with operational semantics in terms of sequences of sets of transitions. For Esterel a semantics has been given in terms of sequences of sets of input and output signals. TCCP and TDCCP have been given semantics in terms of sequences of constraints. Also Labeled Transition Systems (LTS) with states corresponding to program states, transitions corresponding to reactions and labels carrying information about signal causality, have been proposed as semantic models for synchronous formalisms ([5], [33], [23]).
In order to satisfy the bounded response time property, efficient implementations for synchronous formalisms in terms of input-output automata and of sequential circuits have been proposed. Every reaction of a system corresponds to a transition of the automaton or to a one-clock execution of the circuit, respectively. Note that circuits are synthesized directly from programs, compositionally w.r.to their structure.
Real-time and distributedness of embedded systems have motivated proposals of many extensions of the formalisms mentioned [15,22].
Current research efforts aim at the optimization of hardware implementations
[27,28],
distributed implementations [6], integration of formalisms
[25,26].
Verification.
The correctness of a
system with respect to a desired behavior is verified by checking whether a structure that models the system satisfies a formula
describing that behavior.
Such a formula is usually written by using a temporal logic.
Most existing verification techniques
are based on a
representation of the concurrent system by means of a
LTS.
In this approach to verification, state explosion
is one of the most serious problems: embedded systems
are often described by transition systems with a prohibitive number of
states.
Two main methods have been successfully used to extend the applicability of both algorithmic and deductive verification techniques to real industrial-size systems: compositional reasoning and LTS reduction.
In a compositional approach the verification of a system is reduced to the verification of suitable derived formulas for its basic components. In this way the task of verifying a large system is broken into several tasks of verifying smaller and simple systems. In addition, compositional verification allows reducing the verification of a partial modification of the system to the check of the modified components only. Local model checking is a popular method to avoid the exploration of the whole state-space of the system to be verified. The idea is that of checking whether a state of the system satisfies a formula without computing all the states that satisfy the formula. In the framework of propositional mu-calculus several interesting deductive system for local model checking have been proposed [30]. Local model checking has been combined with compositional verification methods in the framework of CCS.
Another solution to state explosion is the definition of suitable reduction criteria on the basis of which a labeled transition system can be reduced to a smaller one, on which the formula can be checked. This problem is often approached by using two different techniques: equivalence based reduction and abstract interpretation. The former approach is based on the notion of equivalence between transition systems. If an equivalence relation preserves the property to be checked, it is possible to define a smaller transition system equivalent to the original one, and therefore to check the property more efficiently. The latter one is based on the notion of correct approximation: if the approximated system verifies a property, then the same property is verified by the original one; the vice versa does not hold, in general.
Many works have been done on equivalence based reduction. A thorough discussion about this approach can be found in [34]. [7,14,29] deal with transformations of transition systems preserving properties expressible by fragments of a temporal logic (for example avoiding the use of some operators). An interesting method is presented in [2], where, given a CTL formula, an equivalence based on it is defined. While this last approach has the advantage of introducing a coarser equivalence, by basing it on a particular formula, it has the drawback of traversing the transition system to determine such an equivalence. In [8] "ad hoc" equivalences are applied to verify mu-calculus formulas in real case studies.
Abstract interpretation is a method for analyzing programs in order to collect approximate information about their run-time behavior; this information can be used as a guide to the construction of reliable and efficient systems. Abstract interpretation is based on a non-standard semantics, that is a semantic definition in which the standard (concrete) domain is replaced by a simpler (abstract) one, and operations are interpreted on the new domain. One of the most popular approaches to abstract interpretation is defined in by P. and R. Cousot. By using this approach a variety of different analyses can be systematically defined. Moreover, the proof of correctness of the analysis can be done in a standard way. Several methods to combine abstract interpretation and model checking have been proposed in the last few years [9,10,11].
A verification technique successfully used for synchronous formalisms
is that of observer monitoring [12].
According to this technique, a safety property
can be mapped
to a program
which runs in parallel with a program P
and observes its behavior, in the sense that at each instant
reads both inputs and outputs of P.
If
detects that P has violated
then it broadcast
an "alarm" signal.
Semantic models of synchronous formalisms.
In [16,23] we have defined
LTS semantics for Statecharts.
In [16] for Statecharts represented as processes of a
CCS-like process
algebra, a semantics is given which is equivalent to Pnueli and
Shalev's "step semantics".
The semantics considered in [23] differs from the previous one
insofar as the reaction of a statechart to the environment is always defined.
In [31] we have given a semantic model for TDCCP in terms of LTSs. In [32] we have proposed an interpretation for Esterel in terms of LTSs reflecting the behavior of circuits corresponding to programs.
Equivalence relations over programs can be derived from
bisimulation over LTSs.
For Statecharts, which admits a constructs of
nondeterministic choice, coarser notions of equivalences can be studied
[23].
Bottom-up and top-down development of specifications.
The success of Statecharts as a general specification language motivates reserch
on the problem of bottom-up and top-down development of specifications. As
regards bottom-up construction of statecharts and reuse of components, they are limited by Huizing and Gerth's result that synchronous hypothesis, causality and modularity cannot be combined
in one semantics.
In [24] we have proposed a notion weaker that modularity,
projectability, and defined a projectable semantics for Statecharts.
As regards construction of statecharts by stepwise refinement this
is limited by
the
"step semantics" which guarantees finiteness of
the reaction by asking that transitions in the step affect states in
different components. So, a semantic better suited to specification refinement arises from allowing sequences of transitions in the same component, with the
request that, in order to keep the reaction finite, a transition is not
performed twice in the same instant ("chain semantics").
Extensions of formalisms.
Statecharts as proposed originally are
not suitable to express priorities and real-time, and syntactic and semantic
extensions may be needed.
In [21] we tackle the problem of expressing priorities and
preemption for
transitions which are enabled at an instant and are mutually exclusive.
A general kind of priority can be expressed by negated signals or,
alternatively, by associating explicit priorities to transitions.
Also the hierarchy of states can be exploited to express a priority
("interrupt ") which results to be weaker than the previous one.
A syntactic extension of the language allows expressing
preemption (in the chain semantics).
In [22]
we have considered a version of Statecharts having
transitions with duration and studied techniques supporting a methodology for
timed statecharts development.
Given an
abstract specification with partial temporal information, such as
absolute duration of some transitions, ratio of transition durations
and speed of the environment,
a time refinement ("retiming") allows to pass to a more
detailed specification good for implementation while preserving
behavior.
Compositional verification.
In [20] we have defined a compositional proof system for
checking mu-calculus properties of Statecharts processes.
The proof system combines local model checking with compositionality as done in
[1]
but the new and complex constructors of statecharts processes are considered.
Processes are verified in a compositional way
on the structure of the process without constructing the underlying
LTS.
In [17] we consider
an extension of Statecharts processes with real-time features
with respect to a discrete time domain. Moreover, we extend
the compositional proof system of [20] to
the timed case for a discrete extension of mu-calculus with freeze
quantifiers and timing constraints.
Equivalence based reduction. Our work in this field has been devoted to the definition of a new branching time temporal logic, selective mu-calculus [3], obtained from mu-calculus by defining new selective modal operators.
The selective mu-calculus is as powerful as the mu-calculus and can
be used to characterize a formula based equivalence
of LTSs.
Given a selective mu-calculus formula ,
the equivalence is based on the set, ,
of actions occurring inside
the modal operators of ,
and it is called -equivalence.
A selective mu-calculus formula ,
with
as the set of occurring
actions,
has the same truth value on all
the -equivalent LTSs.
By suitably choosing a LTS in this class,
the verification process
becomes more efficient.
Abstract interpretation.
Two main classes of abstractions have been considered:
data-values abstractions and control-behavior abstractions.
In [18] we propose a method to effectively build a correct abstract model for value-passing concurrent processes over infinite domains of values. We define a symbolic semantics of processes, which differs from the classical one [13] mainly for the treatment of recursion and for the representation of branching of transitions by means of explicit relations of alternative and non-deterministic choices. The symbolic representation provides a finite representation similar to classical flowcharts of the classical infinite LTSs. We develop a technique to compute a correct abstract model for full mu-calculus by interpreting the symbolic graph on a finite set of abstract values rather than on concrete values. This approach allows deriving a correct and quite precise abstract model directly from processes without looking at the concrete infinite model.
One of the main drawbacks of the abstract model checking methods based on values abstraction is that, in general, it is difficult to find out a precise enough abstraction for the formula to be verified. In [18] we propose a slight different approach in the framework of value-passing concurrent processes, where the precise abstraction is constructed on-the-fly by means of first-order constraints. The model checking algorithm terminates with a precise answer for full mu-calculus if recursion of processes satisfy some non-trivial conditions. When the algorithm does not terminate, as typically for liveness properties, an approximation can be suitably obtained by abstracting constraints to weaker ones.
Actually, when dealing with concurrent systems, a number of interesting properties are independent from the computed values, while they strongly depend on the behavior of systems in terms of performed sequences of actions. In [4] we apply abstract interpretation to the analysis of such a behavior. The analysis we perform is called interesting actions analysis: the behavior of a process P is observed in an "abstract" way, while disregarding all the non-interesting actions. This abstraction has been used to efficiently verify properties of processes of CCS without values, but we claim that the approach can be applied to synchronous formalisms with values as well.
Among the collaborations in which the participants
of the project are involved, two
are particularly related to the subject of modeling
and specification: the HCM ABILE (Abstract Interpretation of
Declarative Languages) and the E.C. Working Group COTIC (Concurrent
Constraint Programming for Time-critical Applications).
Among synchronous specification formalisms, TCCP and TDCCP are those most recently introduced and expressive power w.r.to other formalisms mentioned, implementation and application are matter of investigation. We are interested primarily in the study of expressive power and we expect that TCCP and TDCCP are sufficiently powerful for encoding classical constructs of data-flow and state-oriented formalisms.
The automaton theoretic approach to concurrent system modeling and verification has been very successful. Alur and Dill have proposed augmenting Büchi's automata with time and Harel and Drusinsky have endowed finite state automata with parallelism and communication. We want to develop a concept of "Timed Communicating Automaton" (TCA), find for it results on languages accepted, succinctness, closure properties, and study retiming on a model simpler than statecharts, which should be codifiable in TCAs.
In addition, we
want to study the use of selective mu-calculus to define methods
to make the verification process more efficient.
Given a selective mu-calculus formula
(with a set
of occurring
actions), we can either
hide the actions
not occurring in ,
and minimize the transition system generated
by the environment for P accordingly
(this is possible because almost all the existing verification
environments, such as Concurrency Worchbench, CADP,
offer hiding and minimization facilities), or
syntactically transform the given specification P into
another specification Q
such that the transition system corresponding to Q is smaller than that
corresponding to P , but
is -equivalent to it, or
follow a semantic approach, where the reduction, with respect
to a given set
of actions, is made using a non-standard semantics,
able to reduce
the transition system during the generation phase.
Our long term aim is to contribute to a design methodology based on formal methods which can be accepted in a wider range of industrial projects. Crucial points in the definition of such a methodology are:
Francesca Levi obtained from the University of Pisa the laurea degree in
Computer Science in 1991, and a Ph.D. in Computer Science in 1997 with a
thesis on "A compositional -calculus proof system for Statecharts
processes". At the present she is assistant professor.
Her research is focussed on formal verification problems with a
particular interest in the application of abstract interpretation techniques
and abstract model checking.
She devotes 50 % of her time to this project.
Andrea Maggiolo-Schettini is full professor of Programming Languages in Pisa since 1983.
He has done research on computability, automata theory, graph grammars,
concurrency.
He has been Chairman of the Department of Computer Science and at the
present is Director of the Postgraduate School in Computer Science.
He is full-time on this project.
Simone Tini graduated in Computer Science in Pisa in 1995 with a thesis
on "Equivalence of Statecharts".
At the present he is a graduate student in Computer Science and is expected
to discuss a Ph.D. thesis on "SOS semantics for synchronous formalisms"
by December 1999.
He is full-time on this project.