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.
Examples from literature of complex properties which can be formalised in CTL[DC]
properties of a synchronous bus arbiter
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).
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)
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.
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