||An Efficient Model Checker for Duration Calculus
||Heise, William Pihl
||Hansen, Michael Reichhardt (Embedded Systems Engineering, Department of Informatics and Mathematical Modeling, Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark)
||Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark
||This project present a model checker for the interval logic Duration Calculus.
The model checker is an implementation of the second model checking algorithm
from . The approximation behind this algorithm allows the model checking
problem to be reduced to solving Presburger arithmetic.
The purpose has been to achieve an efficient model checker, and to extend the
model checking algorithm with some optimizations and include time on states
in the model.
The model checker integrates the SMT solver Z3 to solve the generated Presburger
constraints. The whole model checker is in a single program, which is a
command line based tool.
A systematical test of nine models and five formulas have been conducted. Test
have shown that small models are verifiable on a single PC, and using some extensions
to the model checking algorithm, expressive formulas are verified within
reasonable time. Memory problems occurred when generating the constraints
for formulas with chop for model with 30 states and less, for formulas without
chop the model checker could handle model with 100 states and more.
The functional language F# makes an succinct implementation of the model
checking algorithm, and the .NET platform is an effective platform to implement
the model checker.
||Technical University of Denmark (DTU) : Kgs. Lyngby, Denmark
Creation date: 2010-09-10
Update date: 2010-09-10