Beta 1

Title An Efficient Model Checker for Duration Calculus
Author Heise, William Pihl
Supervisor Hansen, Michael Reichhardt (Embedded Systems Engineering, Department of Informatics and Mathematical Modeling, Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark)
Institution Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark
Thesis level Master's thesis
Year 2010
Abstract 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 [5]. 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.
Imprint Technical University of Denmark (DTU) : Kgs. Lyngby, Denmark
Series IMM-M.Sc.-2010-50
Original PDF ep10_50_net.pdf (1.71 MB)
Admin Creation date: 2010-09-10    Update date: 2010-09-10    Source: dtu    ID: 266706    Original MXD