DCVALID 
A tool for modelchecking Duration Calculus Formulae

Paritosh Pandya
 
  • Introduction
  • Overview , User manual User Manual  and Technical Report
  •  CTL[DC] modelchecking of SMV, Verilog and Esterel (trial version available for download).
  • Distribution and Installation
  • Examples
  • Papers
  • Lecture Notes/Slides
  • Links


    • DCVALID is a program to check validity of  Duration Calculus Formulae. It can be used as a tool to visualize DC specification and to check for their consistency. It can also be used in conjunction with other tools to model check DC properties of systems. Currently, systems written in SMV, Verilog (VIS), ESTEREL and SPIN are supported.

    DCVALID is based on an automata theoretic decision procedure for Quantified Discrete-time Duration Calculus (QDDC). For every formula D, we construct a finite state automaton A(D) precisely accepting the finite state sequences satisfying D. The automaton can be used to find models and counter models, or as a synchronous observer (or monitor) for model checking. DCVALID makes use of MONA which provides efficient multi-terminal BDD based representation of automata and  has implemented algorithms  for operations on automata such as product, projection, determinisation and minimisation. See Technical Report for details.

    Click for a quick overview  of  DCVALID.  The user manual gives syntax, semantics and usage.
    Click for a paper on QDDC decidability and its implmentation in DCVALID.

    DCVALID was designed and programmed by Paritosh K. Pandya at Tata Institute of Fundamental Research, Mumbai, India. Some recent extensions were carried out under the aegis of UNU/IIST offshore R&D project Semantics and Verification of Real-time programs using Duration Calculus.

    Acknowledgements DCVALID1.4 makes use of the validity checker for WS1S formulae, MONA 1.4, developed within the BRICS project at Aarhus University, Denmark. We are grateful to its designers for permission to use  and distribute it with DCVALID.
    The compiler construction system  GENTLE   was used in the implementation.
    For model checking, CTLDC makes use of existing model checkers SMV, VIS, Xeve.

    Current Stable Version

    DCVALID1.3 allows checking validity of Quantified Discrete time Duration Calculus (QDDC) formulae. It also provides support for checking dense time DC formulae without lengths or durations. DCVALID1.3  includes:
  •  DCEST which allows modelchecking of QDDC formulae against ESTEREL programs using the Esterel verification tools.  See the documentation.
  • DCSMV allows model checking of QDDC properties of SMV designs using the SMV checker.

    • See example files supplied with distribution for details.
  • DCSPIN allows model checking of QDDC properties of Promella designs using the SPIN checker.
    • QDDC allows formulation of safety and bounded-liveness properties of systems. Support for more general class liveness and branching properties is provided using logic CTL[DC] in the Version 1.4 which also allows model checking SMV, Verilog and Esterel designs.

    CTL[DC] model checking of SMV, Verilog and Esterel designs

    Version 1.4 Ready for Release 
       Download advance trial version here (Linux Pentium PC Binaries)
       (Open Source version coming soon!!)

    DCVALID 1.4 has  following New features:
          Extended logic called CTL[DC]. Extends CTL with past and timing properties.
               TCS00-PKP-2 techincal report  on CTL*[DC] modelchecking
                     (draft report on  CTLDC specification format and model checking SMV, Verilog and Esterel. )
          Checks SMV designs using tool CTLDC and SMV
          Checks VERILOG  designs using tool CTLDC  and VIS
          Checks  ESTEREL designs using tool  CTLDC, Esterel Compiler and  XEVE or VIS.
          Checks  SPIN (promella) designs using tool DCSPIN and SPIN.

          Examples:
               Examples from literature of complex properties which can be formalised in CTL[DC]

               Some complex properties of a synchronous bus arbiter
                 Conclusions
                 Solution  using CTLDC  and SMV   (see readme.txt)
                 Solution   using CTLDC  and VIS     (see readme.txt)
                 Solution   using CTLDC  and Esterel    (see readme.txt)

               Analysis of Gigamax Cache coherence protocol (documentation in preparation)

    New:  CTLDC can now compute length of smallest and longest subsequence within executions of system which satisfies a   formula D. These are specified as MINDCLEN(D) and MAXDCLEN(D).

    Future Release

    Future release will have capabilities for model-checking dense-time properties written in logic
    LIDL, Interval Duration Logic with Located Constraints. It will work in conjunction with UPPAAL.

    Distribution (version 1.3 released 10 August, 1999)
     (Trial version 1.4 released 2 October 2000. See here)

    DCVALID is available free of cost for educational use. See LICENSE before downloading.
    The current version is DCVALID 1.3.

    Please send me an email if you download this software.
    This will allow me to notify you about new releases and changes.

  • V1.3 linux-elf distribution for Pentium PC

    •          (UPDATED version 1.3 released on 10 August, 1999) ( 323646 Bytes)

    Installation and Usage

    Installation notes are in README file contained in the distribution.
    The documentation is contained in file dcvalid.txt.
    Several example specifications are including the mine pump, delay insensitive oscillator and Fischer's mutual exclusion protocol are supplied with the distribution.

    Examples

  • Fischer's Mutual Exclusion Algorithm (24 seconds) source
  • Lift specification (82 seconds) source
  • Mine pump (25 seconds) source
  • Delay insensitive oscillator using Mueller's C-gate (43 seconds) source

    • (All times are for PC Linux system with 75 MHz Pentium processor and 32Mbyte ram)
    NEW: Finding OPTIMAL solution to JOB-SHOP Scheduling Problems (one, two).
               This uses the ability of DCVALID to find SHORTEST model.

    Papers and Technical Reports

  •  P.K. Pandya, Specifying and Deciding Qauntified Discrete-time Duration Calculus formulae using DCVALID, Technical Report TCS-00-PKP-1, Tata Institute of Fundamental Research, Mumbai, 2000. To appear in Proc. Real-Time Tools 2001, Aalborg, August, 2001
    (affiliated with CONCUR 2001).
  •  P.K. Pandya, Model checking CTL[DC],  Technical Report TCS-00-PKP-2, Tata Institute of Fundamental Research, Mumbai, 2000. Appeared in Proc. TACAS 2001, Genova, LNCS 2031, Springer-Verlag, April 2001.
  • P.K. Pandya, Model checking CTL[DC] properties of SMV, Verilog and Esterel Designs, DRAFT Technical Report TCS-00-PKP-3, Tata Institute of Fundamental Research, Mumbai, 2000.
  • P.K. Pandya, Interval Duration Logic: Expressiveness and Decidability, Technical Report

    • TCS-00-PKP-5, Tata Institute of Fundamental Research, Mumbai, 2000.
  • P.K. PAndya, DCVALID: An Overview, Technical Note TN-2000-01, (Web document), 2000.

    • Lecture Notes/Slides

  • Symbolic Model Checking: An introduction  Lecture Slides (postscript), presented at

    • Workshop on Formal Methods in Safety-Critical and Industrial Applications, IIT Mumbai, 16-18 November, 2000.
  • Intoduction to Interval Temporal Logics and Duration Calculus, Lecture slides (postscript), Tutorial presentation at FTRTFT 2000, Pune, September, 2000.

    •      Part 1: Introduction, Lecture Note LN-2000-01
         Part 2: Deciding QDDC using DCVALID, Lecture Note LN-2000-02
         Part 3: Interval Duration Logic with Located Constraints, LN-2000-03

    Some links of Interest

  • MONA - a validity checker for WS1S
  • PC/DC -- A Duration Calculus Proof Assistant based on PVS.
  • Interval temporal logic  by Ben Moszkowski and collegues
  •  SMV, and NuSMV
  • VIS
  • ESTEREL
  • Jonathan Bowen's Formal Methods Page
  • Formal Methods in India
  • GENTLE  compiler construction system


    • This page was created by Paritosh K. Pandya on 24 December, 1997. Last modified July, 2001.