DCVALID: 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), 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.

References in zbMATH (referenced in 14 articles )

Showing results 1 to 14 of 14.
Sorted by year (citations)

  1. Hansen, Michael R.; Phan, Anh-Dung; Brekling, Aske W.: A practical approach to model checking duration calculus using Presburger arithmetic (2014)
  2. Cau, Antonio; Janicke, Helge; Moszkowski, Ben: Verification and enforcement of access control policies (2013)
  3. Konur, Savas: A survey on temporal logics for specifying and verifying real-time systems (2013)
  4. Zu, Quan; Zhang, Miaomiao; Zhu, Jiaqi; Zhan, Naijun: Bounded model-checking of discrete duration calculus (2013)
  5. Bolander, Thomas; Hansen, Jens Ulrik; Hansen, Michael R.: Decidability of a hybrid duration calculus (2007)
  6. Schäfer, Andreas: Axiomatisation and decidability of multi-dimensional Duration Calculus (2007)
  7. Krishna, Shankara Narayanan; Pandya, Paritosh K.: Modal strength reduction in quantified discrete duration calculus (2005)
  8. Pandya, Paritosh K.: Finding extremal models of discrete duration calculus formulae using symbolic search (2005)
  9. Sharma, Babita; Pandya, Paritosh. K.; Chakraborty, Supratik: Bounded validity checking of interval duration logic (2005)
  10. Gómez, R.; Bowman, H.: PITL2MONA: implementing a decision procedure for propositional interval temporal logic (2004)
  11. Chakravorty, Gaurav; Pandya, Paritosh K.: Digitizing interval duration logic. (2003)
  12. Ma, HuaDong: Specification and verification of multimedia synchronization in duration calculus (2003)
  13. Pandya, Paritosh K.: Interval duration logic: expressiveness and decidability (2002)
  14. Pandya, Paritosh K.: Model checking CTL*[DC] (2001)