DCEST:

A tool for checking safety and bounded liveness properties
of Esterel Designs

---

Overview

DCEST is part of  DCVALID suite of tools for duration calculus programmed by Paritosh K. Pandya at Tata Institute of Fundamental Research.  Development of DCEST  has been partly carried out under the aegis of the UNU/IIST offshore project  Semantics and Verification of Real-time programs using Duration Calculus.

DCEST relies on the automata theoretic decision procedure of QDDC which translates each  formula into a deterministic finite state automaton recognizing exactly the behaviours satisfying the formula. Duration Calculus formula specifies (initial finite fragments) of Esterel program behaviour whose occurrence must be flagged by a signal. (Thus the formula is usually  of the form not (property) and occurrence of the signal specifies violation of the property. But the user may directly specify error condition  too.)

DCEST translates a duration calculus formula into a synchronous observer which emits an error signal whenever behaviour fragment matching the property is found.  The program together with the synchronous observer can be compiled into automaton form using the Esterel compiler, and then checked for existence of behaviours leading to emission of error signal using  the Esterel verification tool xeve or checkblif. In case of error, a scenario leading to the error generated by xeve and this can be simulated using xes.

There are several advantages to using QDDC to formulate properties:

QDDC is expressive enough to capture the logical semantics of Esterel programs in a compositional manner.

QDDC provides a convenient property based notation for  test conditions.

QDDC is a form of interval temporal logic. It provides a comprehensive set of operators including conjunction, negation and interval modalities.

Papers and Documents:

A tutorial on specifying properties of Esterel programs using QDDC (in preparation)

Compositional semantics of Esterel in QDDC (in preparation)

Papers on Duration Calculus (links to be added)

Foundations of Duration Calculus
Quantified Duration Calculus: Expressiveness and Decidablity
Semantics of Timed CSP in Duration Calculus
Semantics of Esterel in Duration Calculus

Usage:

Esterel compiler (version 5.10 or later) and Esterel verification tools xeve and xes must be separately downloaded and installed.

Install  DCVALID version 1.3.  Make sure that  the installed executable script dcestobs is in your search path.

Create a file consisting of the Esterel program to be model-checked. For example,  micro.strl

Create a file consisting of the QDDC property specifying the property to be verified. For example,   test1, test2, test3.   Each file contains a QDDC formula.

Execute  command "dcestobs  file" with name of file containing test property. This generates a synchronous observer for the property on   standard output. Typical usage is:

          dcestobs test1 >  test1.strl
This gives the file   test1.strl containing the synchronous observer module test1. This modules emits an output signal DCERR whenever its environment generates a pattern of behavior (finite sequence of instances) satisfying the QDDC property test1.

Create a main module (e.g. main.strl) for running the Esterel  program  (e.g. micro.strl) and the  synchronous observers (e.g. test1.strl, test2.strl, test3.strl) in parallel.

Compile the modules main.strl, test1.strl, test2.strl, test3.strl and micro.strl into automaton micro.blif using the Esterel Compiler. Use command

                 esterel -Lblif test1.strl test2.strl test3.strl micro.strl -Bmain
This give a file main.blif containing the automaton.

Check whether error signal is reachable  in this automaton (i.e. emitted  in some execution). This can be done using Esterel verification  tool xeve (or checkblif). E.g

$checkblif -output { DCERR1 DCERR2 DCERR3 } -rel main.rel  main.blif
--- checkblif: Computing the FSM reachable states
--- checkblif: Output DCERR1 NEVER EMITTED
--- checkblif: Output DCERR2 NEVER EMITTED
--- checkblif: Output DCERR3 NEVER EMITTED

The above file micro.strl is such that none of the errors occur. Hence, xeve reports that signals DCERR1, DCERR2 and DCERR3 are never emitted showing that the design is verified against the properties.

In case an error is found, the scenario leading to error is recorded in a file. We modify the controller micro.strl to a new controller micro1.strl which suffers from errors violating each  of the property being tested.

The above steps are followed with this new file.

Xeve now reports that signals DCERR1, DCERR2 and DCERR3 can all be possibly emitted and generates error trails in files DCERR1.csimul, DCERR2.csimul,   DCERR3.csimul .

The scenario leading to error can be graphically displayed  using the Esterel simulator tool xes.

Examples:

Microwave Oven (document in preparation)

The toy microwave oven controller micro.strl

Properties  in Duration Calculus

test1  and corresponding synchronous observer test1.strl
test2  and corresponding synchronous observer  test2.strl
test3  and corresponding synchronous observer  test3.strl

The main module running micro.strl and synchronous observers in parallel.

Output of xeve shows that signals DCERR1, DCERR2 and DCERR3 are never emitted. Hence, the controller satisfies all the properties.

The new microwave oven controller with errors micro1.strl

Output of xeve showing that the new controller violates

property1.: The error trail  DCERR1.csimul
property2 : The error trail DCERR2.csimul,
property3 : The error trail DCERR3.csimul

Bus Arbiter (document in preparation)

The bus arbiter circuit circuit. Esterel code modelling arbiter circuit. (Both are due to Amar Bouali).

Properties of bus arbiter in Duration Calculus

Exclusion property and corresponding synchronous observer Exclusion.strl
Response property and corresponding synchronous observer Response.strl
Fairness property  and corresponding synchronous observer  Fairness.strl

The main module running arbiter and synchronous observers in parallel.

Xeve shows that error signals are never emitted. thereby verifying that Exclusion, Response and  Fairness properties for each cell are satisfied.

A new Fairness property Fairness1

Output of xeve shows that the arbiter violates the new fairness property for

cell1 (RequestIn1, AckOut1)  with error trail Fairness_FAIL1.csimul
cell2 (RequestIn2, AckOut2)  with error trail Fairness_FAIL2.csimul
cell3 (RequestIn3, AckOut3)  with error trail Fairness_FAIL3.csimul
cell4 (RequestIn4, AckOut4)  with error trail Fairness_FAIL4.csimul

Links