With increasingly complex algorithms used in autonomous systems, ensuring the safety, security, and correctness of software is paramount. We present a process for developing high-quality software, encompassing formal specification, implementation, and verification processes. Our approach focuses on developing high-assurance systems using PVS for formal specification, SPARK Ada for implementation, and the SPARK Pro toolset for formal verification, augmented by FAN (Friendly Argument Notation) arguments. This methodology is demonstrated through a detailed case study involving the design and verification of a polygon merge algorithm for OpenUxAS. In our case study, we define and prove critical properties of the algorithm, such as the preservation of all input points in the output and the containment of output points within the original polygons or generated holes. The formal specification has been added to the NASA PVS library, expanding the formalized knowledge about polygons. This integrated approach offers a higher level of assurance than conventional methods, addressing the limitations of traditional testing and debugging practices. By combining PVS, SPARK Ada, and FAN, we streamline the verification process while maintaining correctness assurance, contributing to the advancement of software development practices for safety-critical and autonomous systems.
From Formal Specification to Verified Implementation
2024-09-29
627634 byte
Conference paper
Electronic Resource
English
Formal Specification Method for Systems Automation
British Library Online Contents | 2006
|Formal specification of the TCAS protocol
AIAA | 1993
|Formal Specification of the TCAS Protocol
British Library Conference Proceedings | 1993
|Formal Specification of Railway Control Systems
Springer Verlag | 2013
|British Library Conference Proceedings | 2000
|