Pisa - Dipartimento di Informatica - Research Evaluation Exercise 1999


Specification and verification
of
embedded systems



Proposer: Andrea Maggiolo-Schettini


Summary:

Purpose of the project is to tackle the problem of designing embedded systems. The research will concentrate on the study of formalisms, with adequate semantics to support implementation, specification methods and verification, and on the development of verification methods and tools.

State of the art and trends:

Embedded systems are computer systems which form an integral part of a larger system (a car, an airplane, a household utensil), determining its functionality. The embedded system gathers information through sensors, processes information and sends signals to actuators. In the last few years embedded systems have been pervasively introduced in all kinds of goods and a significant number of them contain safety critical aspects. At the same time there is an increasing awareness of the fact that formal specifications and application of verification techniques may significantly reduce the risk of errors in the development of systems, compared with traditional informal specification and testing. Actually, with complex embedded systems, system testing can only cover a subset of all possible input variations, whereas verification can systematically test all of them, and therefore it is more apt to find deeply nested errors. From a computer science point of view, embedded systems are real-time distributed reactive systems.

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 $\phi$% WIDTH=16 HEIGHT=34 can be mapped to a program $\Omega$% WIDTH=20 HEIGHT=17 which runs in parallel with a program P and observes its behavior, in the sense that at each instant $\Omega$% WIDTH=20 HEIGHT=17 reads both inputs and outputs of P. If $\Omega$% WIDTH=20 HEIGHT=17 detects that P has violated $\phi$% WIDTH=16 HEIGHT=34 then it broadcast an "alarm" signal.

Research activities of the participants:


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 $\phi$% WIDTH=16 HEIGHT=34 , the equivalence is based on the set, $\rho$% WIDTH=14 HEIGHT=33 , of actions occurring inside the modal operators of $\phi$% WIDTH=16 HEIGHT=34 , and it is called $\rho$% WIDTH=14 HEIGHT=33 -equivalence. A selective mu-calculus formula $\phi$% WIDTH=16 HEIGHT=34 , with $\rho$% WIDTH=14 HEIGHT=33 as the set of occurring actions, has the same truth value on all the $\rho$% WIDTH=14 HEIGHT=33 -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).

Short term plans and expected results:

We want to study how LTSs with richer information on labels can be used as semantic models for synchronous formalisms. We shall take Boudol and Castellani's Proved Transition Systems (PTS) which have in their labels information on rules applied to derive transitions, and we shall consider Esterel in particular. We expect that information in PTSs can be used both to optimize hardware implementation and to improve the verification phase when the observer monitoring technique is adopted. As regards circuit implementation, we expect to deduce from PTSs the latch encoding of program states, so that redundant latches resulting from the compilation technique may be removed. As regards verification, given a program P and a property $\phi$% WIDTH=16 HEIGHT=34 with corresponding program $\Omega$% WIDTH=20 HEIGHT=17 , from the PTS of $P \parallel \Omega$% WIDTH=55 HEIGHT=37 we expect to derive causality relations between actions of P and the action of alarm broadcasting of $\Omega$% WIDTH=20 HEIGHT=17 . This would allow to isolate the parts of P actually causing the violation of $\phi$% WIDTH=16 HEIGHT=34 .

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 $\phi$% WIDTH=16 HEIGHT=34 (with a set $\rho$% WIDTH=14 HEIGHT=33 of occurring actions), we can either hide the actions not occurring in $\phi$% WIDTH=16 HEIGHT=34 , 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 $\rho$% WIDTH=14 HEIGHT=33 -equivalent to it, or follow a semantic approach, where the reduction, with respect to a given set $\rho$% WIDTH=14 HEIGHT=33 of actions, is made using a non-standard semantics, able to reduce the transition system during the generation phase.

Long term scenarios:

The advantage of using formal specification, validation and code generation in a coherent and integrated fashion are generally recognized. Many tools have been developed both in academic and industrial research settings (see the workshops on "Formal Design of Safety-critical Embedded Systems", which involve industry and academia). Some of these tools are powerful enough to be considered for serious industrial application.

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:

-
the formal definition of adequate formalisms able to express synchronous, asynchronous, distributed and real-time aspects of systems,

-
the development of formal verification techniques which can handle the complexity of typical design,

-
the interaction with existing tools and design processes.

Bibliography

1
H.R. Andersen, C. Stirling, G. Winskel A Compositional Proof System for the Modal mu-Calculus. Proc. LICS '94, 1994, 144-153.

2
A. Aziz, T.R. Shiple, V. Singhal, A.L. Sangiovanni-Vincentelli: Formula-Dependent Equivalence for Compositional CTL Model Checking. Proc. CAV '94, Springer LNCS 818, 1994, 324-337.

3
R. Barbuti, N. De Francesco, A. Santone, G. Vaglini: Selective mu-calculus: New Modal Operators for Proving Properties on Reduced Transition Systems. Proc. FORTE X/PSTV XVII, Chapman & Hall, 1997, 519-534.

4
R. Barbuti, N. De Francesco, A. Santone, G. Vaglini: Abstract Interpretation of Trace Semantics for Concurrent Calculi. To appear on Information Processing Letters.

5
G. Berry, G. Gonthier: The ESTEREL Synchronous Programming Language: Design, Semantics, Implementation. Science of Computer Programming 19, 1992, 87-152.

6
G. Berry, E. Santovich: An Implementation of Constructive Synchronous Programs in Polis. URL: http://www.inria.fr/meije/personnel/Gerard.Berry.html.

7
A. Bouajjani, J.C. Fernandez, S. Graf, C. Rodriguez, J. Sifakis: Safety for Branching Time Semantics. Proc. ICALP '91, Springer LNCS 510, 1991, 76-92.

8
G. Bruns: A Practical Technique for Process Abstraction. Proc. CONCUR '93, Springer LNCS 714, 1993, 37-49.

9
E.M. Clarke, O.Grumberg, D.E. Long: Model Checking and Abstraction. ACM TOPLAS 16, 1994, 1512-1542.

10
R. Cleaveland, J. Riely: Testing-Based Abstractions for Value-Passing Systems. Proc. CONCUR '94, Springer LNCS 836, 1994, 417-432.

11
D. Dams, O. Grumberg, R. Gerth: Abstract interpretation of reactive systems. ACM TOPLAS 19, 1997, 253-291.

12
N. Halbwachs, F. Lagnier and P. Raymond: Synchronous Observers and the Verification of Reactive Systems. Proc. AMAST '93, 1993.

13
M. Hennessy, H. Lin: Symbolic bisimulations. Theoretical Computer Science 138, 1995, 353-389.

14
R. Kaivola, A. Valmari: The weakest propositional semantic equivalence preserving nexttime-less Linear Temporal Logic. Proc. CONCUR '92, Springer LNCS 630, 1992, 207-221.

15
Y. Kesten, A. Pnueli: Timed and Hybrid Statecharts and their Textual Representation. Springer LNCS 571, 1992, 591-620.

16
F. Levi: A Process Language for Statecharts. Proc. LOMAPS Workshop, Springer LNCS 1192, 1996, 388-403.

17
F. Levi: Compositional Verification of Timed Statecharts. Proc. ICTL '97, 1997, Applied Logic Series, Kluwer Academic Publishers, to appear.

18
F. Levi: A Symbolic Semantics for Abstract Model Checking. Proc. SAS '98, Springer LNCS 1503, 1998, 134-151.

19
F. Levi: Abstract Model Checking by Constraints Abstraction Second Int. Workshop on "Verification, Model Checking and Abstract Interpretation", 1998.

20
F. Levi: A Compositional $\mu$% WIDTH=16 HEIGHT=33 -calculus Proof System for Statecharts Processes. Theoretical Computer Science 216, 1999, 271-311.

21
A. Maggiolo-Schettini, M. Merro: Priorities in Statecharts. Proc. LOMAPS Workshop, Springer LNCS 1192, 1996, 404-430.

22
A. Maggiolo-Schettini, A. Peron: Retiming Techniques for Statecharts. Proc. FTRTFT '96, Springer LNCS 1135, 1996, 55-71.

23
A. Maggiolo-Schettini, A. Peron, S. Tini: Equivalences for Statecharts. Proc. CONCUR '96, Springer LNCS 1119, 1996, 687-702.

24
A. Maggiolo-Schettini, S. Tini: Projectable Semantics for Statecharts. Proc. MFCS Workshop on Concurrency. Electronic Notes in Theoretical Computer Science 18, 1998.

25
F. Maraninchi, Y. Remond: Compositionality Criteria for Defining Mixed-styles Synchronous Languages. Proc. of International Symposium on Compositionality. Malente/Holsten, 1997.

26
F. Maraninchi, Y. Remond: Mode-Automata: About Modes and States for Reactive Systems. Proc. ESOP '98, 1998.

27
E.M. Santovich, H.Toma and G. Berry: Latch Optimization in Circuits Generated from High-level Descriptions. Proc. ICCAD '96, 1996.

28
E.M. Santovich, H.Toma and G. Berry: Efficient Latch Optimization Using Exclusive Sets. Proc. DAC '97, 1997.

29
J. Sifakis. Property Preserving Homomorphisms of Transition Systems. Logics of Programs, Springer LNCS 164, 1983.

30
C. Stirling and D. Walker: Local Model Checking in the Modal mu-Calculus. Theoretical Computer Science 89, 1991, 161-177.

31
S. Tini, A. Maggiolo-Schettini: Two Semantics for Timed Concurrent Constraint Programming. Proc. Workshop "Constraint Programming for Time Critical Application". Electronic Notes in Theoretical Computer Science 16, 1998.

32
S. Tini, A. Maggiolo-Schettini: A SOS Semantics for Esterel. Submitted for publication.

33
A.C. Uselton, S.A. Smolka: A Process Algebraic Semantics for Statecharts via State Refinement. Proc. IFIP Working Conference on Programming Concepts, Methods and Calculi, 1994, 128-148.

34
A. Valmari: Compositionality in state space verification methods. Proc. Int. Conf. on "Applications and theory of Petri nets", Springer LNCS 1091, 1999, 29-56.

CV's of participants:


Roberto Barbuti is Associate Professor of Programming at the University of Pisa since 1989. His research interests regard abstract interpretation of imperative, logic and concurrent programming, and semantics of programming languages. He is full-time on this project.

1.
Barbuti, R., Giacobazzi, R., Levi, G.: A General Framework for Semantics-based Bottom-up Abstract Interpretation of Logic Programs. ACM TOPLAS 15, 1993, 133-181.
2.
R. Barbuti, N. De Francesco, A. Santone, G. Vaglini: Selective mu-calculus and Formula based Equivalence of Transition Systems. To appear on Journal of Computer and System Sciences.


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 $\mu$% WIDTH=16 HEIGHT=33 -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.

1.
Levi, F.: A Symbolic Semantics for Abstract Model Checking. Proc. SAS '98, Springer LNCS 1503, 1998, 134-151.
2.
Levi, F.: A Compositional $\mu$% WIDTH=16 HEIGHT=33 -calculus Proof System for Statecharts Processes. Theoretical Computer Science 216, 1999, 271-311.


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.

1.
Maggiolo-Schettini, A., Peron, A.: Retiming Techniques for Statecharts. Proc. FTRTFT '96, Springer LNCS 1135, 1996, 55-71.
2.
Cerone, A., Maggiolo-Schettini, A., Time Based Expressivity of Time Petri Nets for System Specification, Theoretical Computer Science 216, 1999, 1-53 .


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.

1.
A. Maggiolo-Schettini, A. Peron, S. Tini: Equivalences for Statecharts. Proc. of CONCUR '96, Springer LNCS 1119, 1996, 687-702.

Collaborators:


Nicoletta De Francesco (associate professor), Antonella Santone (assistant professor), Gigliola Vaglini (associate professor), Dipartimento di Ingegneria dell' Informazione, University of Pisa;
Adriano Peron (assistant professor) Dipartimento di Matematica e Informatica, University of Udine.

Keywords:

Embedded systems, Synchronous formalisms, Operational semantics, Formal verification, Abstract interpretation.



Index Page