Dagstuhl-Seminar 15182
Qualification of Formal Methods Tools
( 26. Apr – 29. Apr, 2015 )
(zum Vergrößern in der Bildmitte klicken)
Permalink
Bitte benutzen Sie folgende Kurz-Url zum Verlinken dieser Seite:
https://www.dagstuhl.de/15182
Organisatoren
- Darren Cofer (Rockwell Collins - Bloomington, US)
- Gerwin Klein (Data61 / NICTA - Sydney, AU)
- Konrad Slind (Rockwell Collins - Bloomington, US)
- Virginie Wiels (ONERA - Toulouse, FR)
Kontakt
- Andreas Dolzmann (für wissenschaftliche Fragen)
- Dagmar Glaser (für administrative Fragen)
Programm
Formal methods tools have been shown to be effective at finding defects in and verifying the correctness of safety-critical systems such as avionics systems. The recent release of DO-178C and the accompanying Formal Methods supplement DO-333 will make it easier for developers of software for commercial aircraft to obtain certification credit for the use of formal methods.
However, there are still many issues that must be addressed before formal verification tools can be injected into the design process for safety-critical systems. For example, most developers of avionics systems are unfamiliar with which formal methods tools are most appropriate for different problem domains. Different levels of expertise are necessary to use these tools effectively and correctly. Evidence must be provided of a formal method’s soundness, a concept that is not well understood by most practicing engineers. Finally, DO-178C requires that a tool used to meet its objectives must be qualified in accordance with the tool qualification document DO-330. The qualification of formal verification tools will likely pose unique challenges.
Qualification is not a widely understood concept outside of those industries requiring certification for high-assurance, and different terminology is used in different domains. The seminar will include sharing of knowledge from certification experts so that formal methods researchers can better understand the challenges and barriers to the use of formal methods tools.
The seminar will include presentations from researchers who have developed initial approaches to address qualification requirements for different classes of formal methods tools. We are especially interested in sharing case studies that are beginning to address tool qualification challenges.
As a practical matter, we plan to focus much of our discussion on the aerospace domain since there are published standards addressing both formal methods and tool qualification for avionics software. The seminar will also include researchers from other domains so we can better understand the challenges and tool qualification approaches that are being discussed in those domains.
In summary, the objectives of this Dagstuhl Seminar are to
- investigate the sorts of assurances that are necessary and appropriate to justify the application of formal methods tools throughout all phases of design in real safety-critical settings,
- discuss practical examples of how to qualify different types of formal verification tools, and
- explore promising new approaches for the qualification of formal methods tools for the avionics domain, as well as in other domains.
Motivation and objectives
Dagstuhl Seminar 13051, Software Certification: Methods and Tools, convened experts from a variety of software-intensive domains (automotive, aircraft, medical, nuclear, and rail) to discuss software certification challenges, best practices, and the latest advances in certification technologies. One of the key challenges identified in that seminar was tool qualification. Tool qualification is the process by which certification credit may be claimed for the use of a software tool. The purpose of tool qualification is to provide sufficient confidence in the tool functionality so that its output may be trusted. Tool qualification is, therefore, a significant aspect of any certification effort. Seminar participants identified a number of needs in the area of formal methods tool qualification. Dagstuhl Seminar 15182 Qualification of Formal Methods Tools, was organized to address these needs.
Software tools are used in development processes to automate life cycle activities that are complex and error-prone if performed by humans. The use of such tools should, in principle, be encouraged from a certification perspective to provide confidence in the correctness of the software product. Therefore, we should avoid unnecessary barriers to tool qualification which may inadvertently reduce the use of tools that would otherwise enhance software quality and confidence.
Most software tools are not used in isolation, but are used as part of a complex tool chain requiring significant integration effort. In general, these tools have been produced by different organizations. We need to develop better and more reliable methods for integrating tools from different vendors (including university tools, open source tools, and commercial tools).
A given software tool may be used in different application domains having very different requirements for both certification and tool qualification. Furthermore, the methods and standards for tool development varies across domains. Consistent qualification requirements across different domains would simplify the process.
Despite the additional guidance provided for the avionics domain in recently published standards (DO-178C, DO-330, and DO-333), there are still many questions to be addressed. For one thing, most practicing engineers are unaware of how to apply different categories of formal verification tools. Even within a particular category, there are a wide variety of tools, often based on fundamentally different approaches, each with its own strengths and weaknesses.
If formal verification is used to satisfy DO-178C objectives, DO-333 requires the applicant to provide evidence that the underlying method is sound, i.e., that it will never assert something is true when it is actually false, allowing application software errors to be missed that should have been detected. Providing an argument for the soundness of a formal verification method is highly dependent on the underlying algorithm on which the method is based. A method may be perfectly sound when used one way on a particular type of problem and inherently unsound when used in a different way or on a different type of problem. While these issues may be well understood in the research community, they are not typically collected in one place where a practitioner can easily find them. It is also not realistic to expect avionics developers to be able to construct an argument for the soundness of a formal method without help from experts in the field.
At the same time, it is also important to not make the cost of qualification of formal methods tools so great as to discourage their use. While it is tempting to hold formal verification tools to a higher standard than other software tools, making their qualification unnecessarily expensive could do more harm than good.
The objectives of this Dagstuhl Seminar were to
- investigate the sorts of assurances that are necessary and appropriate to justify the application of formal methods tools throughout all phases of design in real safety-critical settings,
- discuss practical examples of how to qualify different types of formal verification tools, and
- explore promising new approaches for the qualification of formal methods tools for the avionics domain, as well as in other domains.
Accomplishments
Qualification is not a widely understood concept outside of those industries requiring certification for high-assurance, and different terminology is used in different domains. The seminar was first a way of sharing knowledge from certification experts so that formal methods researchers could better understand the challenges and barriers to the use of formal methods tools.
The seminar also included presentations from researchers who have developed initial approaches to address qualification requirements for different classes of formal methods tools. We were especially interested in sharing case studies that are beginning to address tool qualification challenges. These case studies include tools based on different formal methods (model checking, theorem proving, abstract interpretation).
As a practical matter, we focussed much of our discussion on the aerospace domain since there are published standards addressing both formal methods and tool qualification for avionics software. The seminar also included researchers from other domains (nuclear, railway) so we could better understand the challenges and tool qualification approaches that are being discussed in those domains.
We managed to bridge a lot of the language between the certification domains, mostly railway, avionics, and nuclear, and bits of automotive, and related the qualification requirements to each other. Some of the otherwise maybe less stringent schemes (e.g. automotive) can end up having stronger qualification requirements, because formal methods are not specifically addressed in them. There is some hope that DO-333 might influence those domains, or be picked up by them in the future, to increase the use of FM tools which would increase the quality of systems.
For the academic tool provider side, we worked out and got the message across that tool qualification can be a lot easier and simpler than what we might strive for academically, and discussed specific tools in some detail, clarifying what would be necessary for a concrete qualification. Finally, we also investigated tool architectures that make tools easier to qualify (verification vs code generation).
Creative Commons BY 3.0 Unported license
Darren Cofer, Gerwin Klein, Konrad Slind, and Virginie Wiels
- June Andronick (UNSW - Sydney, AU) [dblp]
- Rob Arthan (Lemma 1 Ltd. - Twyford, GB) [dblp]
- Jasmin Christian Blanchette (INRIA Lorraine - Nancy, FR) [dblp]
- Sandrine Blazy (IRISA - Rennes, FR) [dblp]
- Matteo Bordin (AdaCore - Paris, FR) [dblp]
- Darren Cofer (Rockwell Collins - Bloomington, US) [dblp]
- David Cok (GrammaTech Inc. - Ithaca, US) [dblp]
- Rémi Delmas (ONERA - Toulouse, FR) [dblp]
- Michael Dierkes (Rockwell Collins France - Toulouse, FR) [dblp]
- Eric Engstrom (SIFT - Minneapolis, US) [dblp]
- Gerwin Klein (Data61 / NICTA - Sydney, AU) [dblp]
- Ramana Kumar (University of Cambridge, GB) [dblp]
- Mark Lawford (McMaster University - Hamilton, CA) [dblp]
- Xavier Leroy (INRIA - Le Chesnay, FR) [dblp]
- Stefan Leue (Universität Konstanz, DE) [dblp]
- Alain Mebsout (University of Iowa - Iowa City, US) [dblp]
- Stephan Merz (INRIA Lorraine - Nancy, FR) [dblp]
- César A. Muñoz (NASA Langley ASDC - Hampton, US) [dblp]
- Magnus Myreen (University of Cambridge, GB) [dblp]
- Scott Owens (University of Kent, GB) [dblp]
- Marc Pantel (University of Toulouse, FR) [dblp]
- Markus Pister (AbsInt - Saarbrücken, DE) [dblp]
- Werner Schütz (Thales - Wien, AT) [dblp]
- Konrad Slind (Rockwell Collins - Bloomington, US) [dblp]
- Nick Tudor (D-RisQ Limited - Malvern, GB) [dblp]
- Lucas Wagner (Rockwell Collins - Cedar Rapids, US) [dblp]
- Michael W. Whalen (University of Minnesota - Minneapolis, US) [dblp]
- Virginie Wiels (ONERA - Toulouse, FR) [dblp]
Klassifikation
- semantics / formal methods
- software engineering
- verification / logic
Schlagworte
- dependable systems
- certification
- qualification
- formal methods
- verification tools
