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.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    From Formal Specification to Verified Implementation


    Contributors:


    Publication date :

    2024-09-29


    Size :

    627634 byte





    Type of media :

    Conference paper


    Type of material :

    Electronic Resource


    Language :

    English



    Formal Specification Method for Systems Automation

    Petin, J.-F. / Morel, G. / Panetto, H. | British Library Online Contents | 2006


    Formal specification of the TCAS protocol

    Schaefer, Carl | AIAA | 1993


    Formal Specification of the TCAS Protocol

    Schaefer, C. / AIAA | British Library Conference Proceedings | 1993


    Formal Specification of Railway Control Systems

    Xu, Bingqing / Zhang, Lichen | Springer Verlag | 2013


    Relevance, Integration and Classification of Specification Formalisms and Formal Specification Techniques

    Ehrig, H. / Orejas, F. / Padberg, J. et al. | British Library Conference Proceedings | 2000