Paper Info
Title
Formal specification, refinement, and implementation of path planning
Abstract
We investigate navigation algorithms, and specifically path planning, a fundamental function of autonomous robots. We formally address the issue of enhancing reliability of the widely-used A* path planning algorithm. In our step-wise refinement process, we capture successively more concrete specifications by transforming a high-level specification into an equivalent executable program. To elaborate an initial representation of the A* algorithm, we express it in an abstract and intuitive, yet formal, description. We use traditional mathematical concepts, such as sets, functions and predicate logic to capture this description. We then use the Z specification language to effect the transformation from the mathematical description into Z schemas, thus obtaining a formal specification. We use CZT to perform syntax and type checking and the Z/EVES tool to automatically prove some properties about the specification. Subsequently, we use the Z formal refinement theory to generate the implementation specification. This stage involves both data and operation refinement and is carried out in several basic sub-steps. A Java-based simulation prototype that mirrors the implementation specification is developed in order to demonstrate the applicability of our software development approach.
Year
DOI
Venue
2016
10.1109/INNOVATIONS.2016.7880015
2016 12th International Conference on Innovations in Information Technology (IIT)
Keywords
Field
DocType
path planning,A∗ algorithm,formal specification,refinement,mobile robot simulation
Specification language,Data mining,Programming language,Computer science,Theoretical computer science,Formal specification,Language Of Temporal Ordering Specification,Refinement,Formal methods,Predicate logic,Software development,Executable
Conference
ISSN
ISBN
Citations 
1819-9127
978-1-5090-5344-5
2
PageRank 
References 
Authors
0.38
9
2
Name
Order
Citations
PageRank
Eman Rabiah120.38
Boumediene Belkhouche25517.44