JUCS - Journal of Universal Computer Science 3(4): 304-319, doi: 10.3217/jucs-003-04-0304
The Constrained Shortest Path Problem: A Case Study in Using ASMs
expand article infoKarl Strötmann
‡ Siemens AG, Munich, Germany
Open Access
This paper addresses the correctness problem of an algorithm solving the constrained shortest path problem. We define an abstract, nondeterministic form of the algorithm and prove its correctness from a few simple axioms. We then define a sequence of natural refinements which can be proved to be correct and lead from the abstract algorithm to an efficient implementation due to Ulrich Lauther [Lauther 1996] and based on [Desrosiers et al. 1995]. Along the way, we also show that the abstract algorithm can be regarded as a natural extension of Moore s algorithm [Moore 1957] for solving the shortest path problem.
abstract state machine, software verification, shortest path problem, constrained shortest path problem