DCEST:

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

Paritosh Pandya
(This page is being revised. Please bear with us.)
 
  • Overview
  • Papers and documents
  • Usage
  • Examples
         Microware Oven
         Synchronous Bus Arbiter
  • Links

  •  


    Overview

    DCEST provides facility for model-checking properties of Esterel programs. The properties are written in a logic called QDDC, or Quantified Discrete Duration Calculus (syntax and semantics). This logic is closely related to the Interval Temporal Logic of Moskowski and the Duration Calculus of Zhou et al.  The actual modelchecking is performed using DCEST together with the Esterel verification tools, .e.g. xeve and xes.

    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:

    DCEST is supplied together with DCVALID suite of tools and installed with it. Please refer to the DCVALID   page for instructions on obtaining and installing DCVALI D and DCEST.

    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)
    (Adapted from paper "A Formal Approach to Reactive System Software: A Telecommunications Application in Esterel," Lalita J. Jagadeesan, Carlos Puchol and James Von Olnhausen, International Workshop on Industrial-Strength Formal Methods, Boca Raton, FL, April 1995. )
  • 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)
    Adapted from report "XEVE: An ESTEREL verification environment", Amar Bouali,
    Technical Report No. 0214, INRIA, Sophia Antipolis, France)
  • 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

  • Esterel Programming Language by  Gerard Berry et al, INRIA, France
  • Esterel Verification Tools (part of Meije project at INRIA, France)
  • TEMPEST program verification tool set.
  • DCVALID -- A validity checker for discrete time duration calculus formulae
  • MONA -- an efficient BDD based decision procedure for WS1S from Brics, Aarhus, Denmark.



  • This page was created by Paritosh K. Pandya on 6 April, 1999. Last modified on 3 August, 2000.