DROPS

Document

Qualification of Formal Methods Tools (Dagstuhl Seminar 15182)

Authors: Darren Cofer, Gerwin Klein, Konrad Slind, and Virginie Wiels

Published in: Dagstuhl Reports, Volume 5, Issue 4 (2015)

Abstract

Formal methods tools have been shown to be effective at finding defects in and verifying the correctness of safety-critical systems, many of which require some form of certification. However, there are still many issues that must be addressed before formal verification tools can be used as part of the certification of 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. In most certification processes, a tool used to meet process objectives must be qualified. The qualification of formal verification tools will likely pose unique challenges.

Cite as

Darren Cofer, Gerwin Klein, Konrad Slind, and Virginie Wiels. Qualification of Formal Methods Tools (Dagstuhl Seminar 15182). In Dagstuhl Reports, Volume 5, Issue 4, pp. 142-159, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Article{cofer_et_al:DagRep.5.4.142,
  author =	{Cofer, Darren and Klein, Gerwin and Slind, Konrad and Wiels, Virginie},
  title =	{{Qualification of Formal Methods Tools (Dagstuhl Seminar 15182)}},
  pages =	{142--159},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2015},
  volume =	{5},
  number =	{4},
  editor =	{Cofer, Darren and Klein, Gerwin and Slind, Konrad and Wiels, Virginie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.5.4.142},
  URN =		{urn:nbn:de:0030-drops-53543},
  doi =		{10.4230/DagRep.5.4.142},
  annote =	{Keywords: Dependable systems, Certification, Qualification, Formal methods, Verification tools}
}

Document

DOI: 10.4230/DagRep.3.1.111

Software Certification: Methods and Tools (Dagstuhl Seminar 13051)

Authors: Darren Cofer, John Hatcliff, Michaela Huhn, and Mark Lawford

Published in: Dagstuhl Reports, Volume 3, Issue 1 (2013)

Abstract

With the pervasive deployment of software in dependable systems used in everyday life,society is increasingly demanding that software used in critical systems must meet minimum safety, security and reliability standards. Certification is the procedure by which an authorized person or agency assesses and verifies characteristics of a system or product in accordance with established requirements, standards, or regulations. For software, it encompasses traditional notions of verification, but also includes the evidence, tools, methods, and personnel qualifications that are needed to convince the certification authority that the system or product conforms to the relevant standard. Manufacturers of these systems need consistent and effective guidelines as to what constitutes acceptable evidence of software quality, and how to achieve it. Compared to process-oriented certification procedures, recent approaches provide evidence for dependability by the thorough evaluation of the product itself and the adequacy, coverage and maturity of design and quality assurance methods. Substantial progress has been made in areas including safety and assurance cases, the conceptual foundation of evidence and formal methods, and tooling for software design and verification. New approaches are necessary to develop holistic and cost-effective methodologies and to provide integrated tool support for creating certifiable software-intensive systems, as well as product-focused approaches to certifying these systems. Experts from academia and industrial practitioners met in the Dagstuhl Seminar 13051 "Software Certification: Methods and Tools" to discuss and software certification challenges, best practices, and the latest advances in certification technologies in several different software-intensive domains (automotive, aircraft, medical, nuclear, and rail).

Cite as

Darren Cofer, John Hatcliff, Michaela Huhn, and Mark Lawford. Software Certification: Methods and Tools (Dagstuhl Seminar 13051). In Dagstuhl Reports, Volume 3, Issue 1, pp. 111-148, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@Article{cofer_et_al:DagRep.3.1.111,
  author =	{Cofer, Darren and Hatcliff, John and Huhn, Michaela and Lawford, Mark},
  title =	{{Software Certification: Methods and Tools (Dagstuhl Seminar 13051)}},
  pages =	{111--148},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2013},
  volume =	{3},
  number =	{1},
  editor =	{Cofer, Darren and Hatcliff, John and Huhn, Michaela and Lawford, Mark},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.3.1.111},
  URN =		{urn:nbn:de:0030-drops-40119},
  doi =		{10.4230/DagRep.3.1.111},
  annote =	{Keywords: dependable systems,safety security, certification, formal methods, model-driven development, validation \& verification, tools}
}

Search Results

Documents authored by Cofer, Darren

Qualification of Formal Methods Tools (Dagstuhl Seminar 15182)

Abstract

Cite as

Software Certification: Methods and Tools (Dagstuhl Seminar 13051)

Abstract

Cite as

Thanks for your feedback!

Could not send message