Bounded Model Construction for Duration Calculus | Jacob Enslev, Anne-Sofie Nielsen
| | Abstract | In this thesis, we shall present a tool, the BMC/DCValidator for automatic validation of duration calculus formulas. Duration calculus (DC for short) is a temporal logic, i.e. a logic for reasoning about time. DC may be used for specifying systems at an abstract level and the purpose of the tool is to verify that the system meets certain requirements, which are also specified using DC. The abstractness and expressiveness of DC makes it well-suited for system description, but hard to verify properties by automatic means.
Our tool provides an e cient implementation of the work of [MF02] whose main idea is to translate DC formulas to propositional clauses or linear constraint systems, both of which may be handed over to an external solver. The timing aspects of the formulas are represented in a discrete way, and the properties of the formulas are validated within a bounded time interval, as the unbounded validation turns out to be undecidable. In some cases, it is possible to determine a bound such that bounded validity implies general validity.
The tool has been implemented with a multitude of options such as polarity optimisation and output format that allow us to experiment with the translation algorithm. Our benchmark results show that the tool has good performance in general, but that the success of the tool is extremely dependent on the implementation details of the solver. | | Type | Master's thesis [Academic thesis] | | Year | 2005 | | Publisher | Informatics and Mathematical Modelling, Technical University of Denmark, DTU | | Address | Richard Petersens Plads, Building 321, DK-2800 Kgs. Lyngby | | Series | IMM-Thesis-2005-05 | | Note | Supervised by Assoc. prof. Martin Franzle and Assoc. prof. Michael R. Hansen, | | Electronic version(s) | [pdf] [ps] | | BibTeX data | [bibtex] | | IMM Group(s) | Computer Science & Engineering |
|