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.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    From Formal Specification to Verified Implementation


    Beteiligte:


    Erscheinungsdatum :

    29.09.2024


    Format / Umfang :

    627634 byte





    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch



    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


    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


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

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