The Eight Reasons For Using SPARK

by Yannick Moy in Formal Verification, Design Method, Certification, Papers and Slides – September 21, 2015

Based on our many years of experience with our customers using SPARK in their projects, we have come up with a list of eight objectives that are most commonly targeted when using SPARK. Most projects only target a few of them, but in theory one could try to achieve all of them with SPARK on a project. This list may be useful for those who want to assess if the SPARK technology can be of benefit in their context, and to existing SPARK users to compare their existing practice with what others do. Each objective is described with some details in a separate section of the SPARK User's Guide.

Objectives 1 to 4 are applicable to most projects:

    Objective 1 (the simplest): Safe Coding Standard for Critical Software
    Objective 2 (the most common): Prove Absence of Run-Time Errors (AoRTE)
    Objective 3 (a touch of functional): Prove Correct Integration Between Components
    Objective 4 (the richest): Prove Functional Correctness

Objectives 5 to 8 address specific issues:

    Objective 5 Ensure Correct Behavior of Parameterized Software
    Objective 6 Safe Optimization of Run-Time Checks
    Objective 7 Address Data and Control Coupling
    Objective 8 Ensure Portability of Programs

If you feel that your own objectives for using SPARK are not represented in the list above, please let us know. Our aim is to enrich this list in the future to represent most (if not all) SPARK projects.

comments powered by Disqus