A tool for modelchecking Duration Calculus Formulae

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

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.

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.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.

Download advance trial version here (Linux Pentium PC Binaries)

(Open Source version coming soon!!)

Extended logic called CTL[DC]. Extends CTL with past and timing properties.

TCS00-PKP-2techincal report on CTL*[DC] modelchecking

(draft report onCTLDC 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).

LIDL, Interval Duration Logic with Located Constraints. It will work in conjunction with UPPAAL.

(Trial version 1.4 released 2 October 2000. See here)

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)

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.

(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.

P.K. Pandya, Specifying and Deciding Qauntified Discrete-time Duration Calculus formulae using DCVALID, in Proc. Real-Time Tools, RTTOOLS'2001, Aalborg, August, 2001 (affiliated with CONCUR 2001).Technical Report TCS-00-PKP-1, Tata Institute of Fundamental Research, Mumbai, 2000.P.K. Pandya, Model checking CTL[DC], in Proc. TACAS 2001, Genova, LNCS 2031, Springer-Verlag, April 2001.Technical Report TCS-00-PKP-2, Tata Institute of Fundamental Research, Mumbai, 2000.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, The saga of synchronous arbiter: On model checking quantitative timing properties of synchronous programs, in Proc. Workshop on synchronous languages, applications and programs SLAP'2002, Grenoble, 2002 (affiliated with EATPS 2002), Electronic Notes on Theoertical Computer Science ENTCS 65.5, Elsevier Scientific Publishers, 2002.P.K. Pandya, Interval Duration Logic: Expressiveness and Decidability, in Proc. Workshop on Theory and Practice of Timed Systems TPTS'2002, Grenoble, 2002 (affiliated with EATPS 2002), Electronic Notes on Theoertical Computer Science ENTCS 65.6, Elsevier Scientific Publishers, 2002. (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. P.K. Pandya, Finding Extremal models of discrete duration calculus formulae using symbolic search, to appear in Proc. AVOCS 2004, Electronic Notes in Theoretical Computer Science, ENTCS, Elsevier Scientific Publishers, 2005. Technical Report, May 2004. first presented at Workshop on Reasoning about large and infinite state systems, Chennai, DecembTer 2001. Gaurav Chakravorty and P.K. Pandya, Digitizing Interval Duration Logic, in Proc. CAV 2003, Colorado, Boulder, July 2003. LNCS 2725, 2003, (Technical Report, TCS-02-PKP-1 , Tata Institute of Fundamental Research, 2002).B. Sharma, P.K. Pandya and S. Chakraborty, Bounded Validity Checking of Interval Duration Logic, in Proc. TACAS 2005, Edinburgh, 2005 , LNCS 3440, (Technical Report, October 2004.) S.N.Krishna and P.K. Pandya, Modal Strength Reduction in Quantified Discrete Duration Calculus, To appear in Proc. FSTTCS 2005, Hyderabad, 2005. LNCS, Springer-Verlag (2005). (Technical Report, CDFVS, IIT Bombay, 2005). R. Kazmiakin, P.K. Pandya, M. Pistore, Modelling and Analysis of Time Related Properties in Web Service Compositions, To appean in Proc. First International Workshop on Engineering Service Compositions (WESC 2005), Affiliated with ICSOC 2005, Amsterdam, (2005)

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

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