@**thesis**{RISC5224,author = {Daniela Ritirc},

title = {{Formally Modeling and Analyzing Mathematical Algorithms with Software Specification Languages & Tools}},

language = {english},

abstract = {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;},

year = {2016},

month = {January},

translation = {0},

school = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},

keywords = {formal methods, model checking, program verification},

length = {167},

type = {mathesis}

}