Application name:

Constrained Shortest Path Problem: A Case Study in Using ASMs

Organisation:

Siemens AG, Corporate Technology

Method:

Gurevich's Abstract State Machines

Tools:

Pencil and paper.

Domain:

Graph theoretical algorithms (the algorithm described is used in telecommunications).

Period:

January 1997 - March 1997

Size:

The original C++-program implementing the algorithm to be verified has a size of 500 lines of code.

Description:

We verify an algorithm to solve the "constrained shortest path problem". This verification is done in six steps: 1. The notion of "shortest path problem" is generalized by introducing abstract data types. 2. It is shown that the "relabeling algorithm" solves the generalized "shortest path problem". 3. The relabeling algorithm is refined into a more efficient "relabeling and scanning algorithm". This refinement is proved correct. 4. Using data type refinement, the "relabeling and scanning algorithm" is refined into Moore's algorithm. 5. It is shown that the "constrained shortest path problem" can be reduced to the generalized "shortest path problem" by introducing step functions. 6. Finally, an implementation of step functions is provided.

Conclusions:

We have done several case studies in verification. The case studies prior to the case study "constrained shortest path problem" were done with interactive theorem provers. It was felt that this approach is not cost effective. In contrast, the present case study seems to suggest that the use of ASMs is cost effective. Of course, on has to keep in mind that the ASM-method is basically a paper-and-pencil method of verification and is therefore less rigorous than a method that produces machine-checked proofs. However, we think that even if a more formal approach is taken and proofs are machine-checked, then an ASM-based paper-and-pencil proof should be done first in order to prepare for the machine-checked proof.

Publications:

"The Constrained Shortest Path Problem: A Case Study in Using ASMs". Journal of Universal Computer Science (J.UCS). 3(4):304-319. 1997.

Contact:

Name:	Karl Stroetmann
Organisation:	Siemens AG
Address:	ZT AN 1 D-81730 Munich
Country:	Germany
Phone number:	+49 (89) 636 49 555
Fax:	+49 (89) 636 42 284
E-mail:	Karl.Stroetmann@mchp.siemens.de
Personal website:	http://www.iicm.edu/jucs_3_4/shortest_path_problem

URL:

http://www.iicm.edu/jucs_3_4/shortest_path_problem

© copyright 2004 | Formal Methods Europe