Go home now Header Background Image
Submission Procedure
share: |
Follow us
Volume 3 / Issue 4

available in:   PDF (293 kB) PS (85 kB)
Similar Docs BibTeX   Write a comment
Links into Future
DOI:   10.3217/jucs-003-04-0304


The Constrained Shortest Path Problem: A Case Study in Using ASMs

Karl Strötmann (Siemens AG, Germany)

Abstract: 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.

Keywords: abstract state machine, constrained shortest path problem, shortest path problem, software verification

Categories: D.2.4, F.3.1, G.2.2