26.04.15 - 29.04.15, Seminar 15182

Qualification of Formal Methods Tools

Diese Seminarbeschreibung wurde vor dem Seminar auf unseren Webseiten veröffentlicht und bei der Einladung zum Seminar verwendet.

Motivation

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

  1. 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,
  2. discuss practical examples of how to qualify different types of formal verification tools, and
  3. explore promising new approaches for the qualification of formal methods tools for the avionics domain, as well as in other domains.