"Formally Modeling and Analyzing Mathematical Algorithms with Software Specification Languages & Tools"
, in RISC, JKU, Serie Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria, RISC, JKU, Hagenberg, Linz, 1-2016
Formally Modeling and Analyzing Mathematical Algorithms with Software Specification Languages & Tools
Sprache des Titels:
In this thesis the behaviour of software specification languages and tools on mathematical algorithms shall be investigated. The main goal is to investigate how tools which have been designed for modeling and analyzing software in other application contexts can be applied to mathematical algorithms. For this purpose, two different mathematical algorithms, namely the DPLL method and Dijkstra?s Shortest Path Algorithm are selected. Furthermore five well-known software specification languages are selected: JML, Alloy, TLA/PlusCal, VDM and Event-B. It shall be examined how far the algorithms can be modeled and how far model checking respectively verification succeeds. The goal of the thesis is not a proper verification/check of every model with every tool but a survey of the potential as well as the difficulties of the usage of software specification languages for the analysis of mathematical algorithms. As a starting point for each algorithm a formal specification is derived and the algorithms are supplied in pseudo-code. A Java prototype is implemented for each algorithm which is then specified by JML annotations. Furthermore the algorithms are modelled in TLA/PlusCal, Alloy, VDM and Event-B and for each language the appropriate analysis supported by the tool is selected (visualizing, model checking, verification). The main result of the thesis is that each tool shows some success when it is used for specifying and analyzing mathematical algorithms, because modeling the algorithms succeeded in every language. In TLA, VDM and Alloy it was possible to completely model check the specifications. Furthermore it was possible to visualize the algorithms in Alloy. In JML and Event-B it was possible to verify major parts of the model;
Sprache der Kurzfassung:
Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria