EARLY HEARING DETECTION AND INTERVENTION VIRTUAL CONFERENCE
MARCH 2-5, 2021
(Virtually the same conference, without elevators, airplane tickets, or hotel room keys)
9/27/2017 | 1:05 PM - 1:50 PM | Guidance for Introducing Formal Methods into a Software Verification Infrastructure | Track 5 - Test and Verification
Guidance for Introducing Formal Methods into a Software Verification Infrastructure
Formal methods -- languages and tools that support mathematics-based reasoning about program properties -- can be a practical component of the verification activities for high assurance software, thanks in part to advances in hardware technology and proof engine power and performance. In safety-critical or high-security systems, testing might not by itself be sufficient to achieve the required level of confidence in a program's correctness.
Despite its advantages, however, adopting formal methods may seem like "culture shock" to many organizations. Issues of concern include personnel training, tool integration, and how to use formal methods in conjunction with (or perhaps instead of) testing or other static or dynamic analysis techniques. This presentation will describe a set of guidelines and processes that can ease the job of adopting formal methods, and summarize some practical experience with their application in industrial projects. The guidance is based on the SPARK language [1, 2] (an Ada subset specifically designed for formal verification) and technology; it can be used either for introducing SPARK into an existing project or for adopting SPARK at the outset. With some adaptation the approach could also be applied to other technologies, e.g. Frama-C.
The guidance has been used in pilot projects by a major aerospace company (Thales) and is documented in a handbook co-authored by AdaCore and Thales [3]. In brief, introducing formal methods can be achieved at several levels based on a project's assurance goals:
1. Stone level - Adhering to the SPARK subset. This is an intermediate step during technology adoption.
2. Bronze level – Proving proper initialization and correct data flow. This level is recommended for the largest part of the code that is possible and will, among other things, prevent reads of uninitialized variables and misuses of global data.
3. Silver level - Proving absence of run-time errors. This level is recommended for critical software, for example if it needs to be certified against software standards such as DO-178B and DO-178C (avionics) or EN 50128 (rail).
4. Gold level - Proving key integrity properties. This level is appropriate for a subset of code where critical safety or security properties need to be shown.
A fifth level, Platinum, entails a full functional proof that the software meets its formally specified requirements. This level may be appropriate in applications demanding ultra-high reliability but is outside the scope of the approach documented in [3].
The guidance at each level analyzes the benefits gained at that level, the impact on processes, and the costs and limitations. The level-based approach is consistent with the objectives in the Formal Methods supplement (DO-333) to the DO-178C standard for airborne software, and it supports the use of "hybrid verification" in which traditional (testing-based) approaches are used to verify some program properties, and formal methods are used to verify others.
References
[1] J. McCormick and P. Chapin; Building High Integrity Applications with SPARK; Cambridge University Press, 2015.
[2] http://www.spark-2014.org/
[3] AdaCore and Thales, Implementation Guidance for the Adoption of SPARK; January 2017.
http://www.adacore.com/knowledge/technical-papers/implementation-guidance-spark/
Presentation:
This presentation has not yet been uploaded.
Handouts:
Handout is not Available
Transcripts:
CART transcripts are NOT YET available, but will be posted shortly after the conference
Presenters/Authors
Benjamin Brosgol
(), AdaCore, brosgol@adacore.com;
Dr. Benjamin Brosgol is a senior member of the technical staff at AdaCore. He has delivered tutorials and presentations at previous STC and SSTC conferences, on topics including safety, security, and programming language technology. He was a member of the Expert Groups for the Real-Time Specification for Java and for Safety-Critical Java Technology, and has also participated in ISO SC22's Working Group on vulnerabilities. In 2006 Dr. Brosgol received ACM SIGAda's Outstanding Ada Community Contributions award, and he has also received ''Best Paper'' and ''Best Presentation'' awards at several Ada-Europe conferences. He holds a BA in Mathematics (with honors) from Amherst College, and MS and PhD degrees in Applied Mathematics from Harvard University.
ASHA DISCLOSURE:
Financial -
Nonfinancial -