The tool checks for validity of discrete time Duration Calculus formula,
and produces scenarios of (counter) models
of formulae.It is based on the validity checker for WS1S formula, MONA, from the BRICS project at Aarhus University, Denmark. Future version of DCVALID will include dense-time linear constraints and allow model checking .
Associated tools DCEST, DCSMV and DCSPIN allow modelchecking designs
SMV and SPIN format.
This page was created on 10 December, 1997 by Paritosh K. Pandya. Last modified on 25December, 1997.