January 27 – February 1 , 2013, Dagstuhl Seminar 13051

Software Certification: Methods and Tools


Darren Cofer (Rockwell Collins – Cedar Rapids, US)
John Hatcliff (Kansas State University, US)
Michaela Huhn (TU Clausthal, DE)
Mark Lawford (McMaster University – Hamilton, CA)

For support, please contact

Dagstuhl Service Team


Dagstuhl Report, Volume 3, Issue 1 Dagstuhl Report
Aims & Scope
List of Participants
Shared Documents
Dagstuhl Seminar Wiki
Dagstuhl Seminar Schedule [pdf]

(Use seminar number and access code to log in)



An increasingly important requirement for success in many domains is the ability to cost-effectively develop and certify software for critical systems (e.g. pacemakers, health monitoring equipment, core banking applications, financial reporting, nuclear reactors, rail automation and active safety in vehicles etc.). Software errors in each of these domains continue to lead to catastrophic system failures, sometimes resulting in loss of life. A recent report by the U.S. National Academy of Sciences [1], concludes that "new techniques and methods will be required in order to build future software systems to the level of dependability that will be required... In the future, more pervasive deployment of software...could lead to more catastrophic failures unless improvements are made." Thus, society is increasingly demanding that software used in critical systems must meet minimum safety, security and reliability standards. Manufacturers of these systems are in the unenviable position of not having consistent and effective guidelines as to what constitutes acceptable evidence of software quality, and how to achieve it. This drives up the cost of producing these systems without producing a commensurate improvement in dependability.

Multiple trends and activities (a) point to the changing nature of development of certified systems and (b) indicate the need for community-wide efforts to assess and form a vision of the future for development of certified systems.

New and Evolving Standards:

To adapt to the significant changes in the role of software in dependable systems and to improve current industrial practice in software engineering, international standards like the IEC 61508 are currently under revision. DO-178C governing certification of software in commercial aircraft has recently been revised to accomodate the use of software technologies such as formal methods and model-based development processes. In several other software-intensive domains new domain-specific standards are being developed.

Process- vs. Product-oriented Certification:

In practice, current certification of software-intensive systems is primarily process based. A reliance on process oriented standards has established a certification practice that is dominated by assessing process-related documents and marking off checklists that are derived from the recommendation annexes of the standards or so-called "approved practice in use". Thorough evaluation of the product itself or the adequacy, coverage and maturity of design and quality assurance methods are sometimes neglected because there is currently no fundamental agreement on software engineering principles and product qualities to achieve demonstrably dependable software. An alternative to process-oriented certification regimes is "safety and assurance cases" [7]. In Europe, and particularly in the UK, assurance cases have been adopted as a product centric alternative approach to certification and are widely used in practice already. Recently the U.S. FDA has issued guidance documents recommending the use of assurance cases in submissions for approval of infusion pumps. However, while assurance cases offer some product oriented focus to certification, the lack of standardization of safety and assurance case arguments has its own pitfalls [8].

Advances in Formal Methods:

In academia, research on formal methods has made substantial progress with respect to scalability and coverage recently, e.g. in tool-supported model-based design and code generation, but also in the area of software model checking or timing analysis [2]. Thus, formally assuring safety requirements has become feasible at least on the level of components. Nevertheless, research usually focuses on specific techniques, thereby often neglecting the cross-cutting nature of dependability and the need of providing traceable evidence.

Software Development Trends:

Two trends relevant in industrial software development for critical systems are the success of model-based design environments that support automated code generation and the need to integrate pre-developed or Commercial Off The Shelf (COTS) software components: (1) Model based tools facilitate rapid prototyping and validation and verification in earlier design phases than traditional processes, but with a price of higher effort in the design phases performed by well-trained and experienced personnel. Software quality will only benefit from these approaches, if certification procedures are adapted towards a cost-effective assessment on the level of models wherever it is adequate. For instance, if model based tools are supported by V & V tools that perform some verification at design time, how does this affect certification standards that require independent design and V & V teams? (2) Evidence based upon prior usage and operating history are typically key components in making decisions in industry about the "fitness for use" of a pre-developed software application or component. However, platform-specific and environmental constraints on the usage are sometimes not specified in detail which has lead to catastrophic failures in the past.

Community-building Activities:

Various community-building organizations are being formed drive research, education, and cross-domain coordination in the area of software certification. For instance, the Software Certification Consortium (SCC) was formed in 2007 as a North American initiative to promote product based software certification. Its members are drawn from regulators, industry and academia. SCC has been successful in highlighting shortcomings in current certification regimes and in providing challenge problems and example certification artifacts to the broader community.

Seminar Topics and Goals

The Dagstuhl Seminar 13051 Software Certification: Methods and Tools brought together experts for the purpose of assessing the current state of practice, identifying challenges, promising techniques/methods, and for creating a road map for future research, education, and standards development in the area of certification of software and systems.

The seminar addressed the following topics:

  • Identification of the challenges, regulatory bodies, primary certification standards, typical development and certification processes in variety of safety-critical domains including avionics, automotive, medical systems, and rail, as well as cross-cutting aspects of security certification.
  • Developing a rational basis for the primary activities in certification. This included work on the interrelation between i) how we develop software in a way that facilitates certification; and, ii) how we collect and use evidence about software products to evaluate whether they should or should not be certified for use, and iii) cost-benefits issues in certification.
  • Pros and cons of assurance-cases in regulatory regimes, assessing the confidence given by assurance cases, new techniques for presenting assurance case arguments, tools for managing the collection of evidence and organization of arguments for assurance cases, and the relationship between assurance cases and software certification standards such as DO-178C.
  • The use of tools and open source infrastructure in certification, along with new approaches and guidelines for qualifying tools for use in development of certified systems.
  • The latest advances in relevant formal methods for software verification, and integrating formal methtod with other quality assurance techniques such as testing in the context of certified system development.
  • The increasing use of "systems of systems" in safety-critical domains, and the need for new approaches supporting compositional certification and reuse of components in the context of certified systems.
  • The structure, nature, use, of current certification standards, current business models and organizational principles for developing standards, and how these aspects might be evolved to better address the needs of the community.
  • Strategies for managing the complexity of software intensive systems, including model based development, refinement-based methodologies, and generative techniques.
  • Challenges problems, infrastructure, and pedagogical resources to support research and education for both academia and industry in the area of certified sytem development.

Seminar Participants and Activities

41 researchers participated in the "Software Certification" Seminar, 21 academic researchers, 10 are affiliated to research institutes and 10 experts from industries proving the strategic relevance of the subject to both, research and practice. With about 40% the portion of North American participants was remarkable high.

The seminar started with an introductory session on Monday morning at which the organizers recapitulated the outline, the objectives, and goals of the seminar. Each participant shortly introduced him/herself, his/her scientific background and personal goals for the seminar week. Then senior experts gave an overview on software certification in different domains, namely the avionic, nuclear, medical devices, automotive, and the rail domain. Monday afternoon ended with a discussion on the major differences and similarities between software assessment in the domains and cross-domain challenges. From Tuesday to Thursday experts presented their work. Panel discussions, challenge problem advertisements as well as working group sessions took place in the afternoons and evenings. A wide range of topics was covered including assurance cases and the fundamentals of how to achieve evidence, tool support to software assessment in the certification process, experience reports and new methodologies for the medical device domain, model based design methods appropriate to certification, issues in cloud security and security certification, tools and methods for static analysis, formal verification and testing. On Thursday evening we had a fruitful discussion with the participants of the Dagstuhl seminar on "Multicore Enablement for Embedded and Cyber-Physical Systems" organized by Andreas Herkersdorf, Michael Hinchey, and Michael Paulitsch that was held in parallel. Among others the following questions were discussed: What are the requests on predictability that have to be satisfied by multicore architectures to be well suited for dependable systems? What are the compelling cyberphysical dependable applications that need multicore architectures? What mechanisms known from dependable software development may be transferred to multicore architecture design and vice versa? Friday was dedicated to working groups as well as outlining and scheduling post seminar proceedings in which we plan to summarize the state of the art in software certification and the results of the seminar. The areas identified by the plenum to be most relevant for further progress on software certification are:

  • Fundamentals on confidence and evidence
  • Compositional certification
  • Education on dependable systems and certification
  • Tool qualification
  • Security
  • Methods for the development of certifiable software and methods supporting certification


  1. D. Jackson, M. Thomas, L.Millett. "Software for Dependable Systems: Sufficient Evidence?" Committee on Certifiably Dependable Software Systems, National Research Council. National Academies Press. 2007.
  2. M. Huhn, H. Hungar. UML for software safety and certication. Model-based development of safety-critical software-intensive systems. In H. Giese, G. Karsai, E. Lee, B. Rumpe, and B. Schätz: Model-Based Engineering of Real-time Embedded Systems, LNCS 6100, Springer, p. 203-240. 2010.
  3. M. Huhn, A. Zechner. Analysing Dependability Case Arguments Using Quality Models. In B. Buth, G. Rabe, and T. Seyfarth (eds): 28th Intern. Conference on Computer Safety, Reliability, and Security, (SAFECOMP): LNCS 5775, Springer, p. 118-131, 2009.
  4. A. Wassyng, T. Maibaum, M. Lawford, On Software Certification: We Need Product-Focused Approaches. C. Choppy and O. Sokolsky (Eds.): Monterey Workshop 2008, LNCS Vol. 6028, Springer, 2010, 250-274.
  5. J. Hatcliff, M. Heimdahl, M. Lawford, T. Maibaum, A. Wassyng, F. Wurden. A Software Certification Consortium and its Top 9 Hurdles. In Proceedings of the First Workshop on Certification of Safety-Critical Software Controlled Systems (SafeCert 2008), Electronic Notes in Theoretical Computer Science, Vol. 238, No. 4, pp. 11-17, 2009.
  6. FDA, "FDA Launches Initiative to Reduce Infusion Pump Risks", News Release, April 23, 2010 (see:
  7. R. Bloomfield and P. Bishop. Safety and assurance cases: Past, present and possible future - an Adelard perspective. In Dale, C., Anderson, T., eds.: Making Systems Safer, Proceedings of the Eighteenth Safety-Critical Systems Symposium, Bristol, UK (February 2010) 51-67.
  8. A. Wassyng, T. Maibaum, M. Lawford and H. Behr. Is there a case against safety cases?. Submitted to post-proceedings volume of Monterey 2010 Workshop, to be published in LNCS.
  Creative Commons BY 3.0 Unported license
  Darren Cofer, John Hatcliff, Michaela Huhn, and Mark Lawford


  • Dependable Systems
  • Formal Methods


  • Dependable systems
  • Safety
  • Security
  • Certification
  • Formal methods
  • Quality assurance
  • Verification
  • Tools


In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.


Download overview leaflet (PDF).


Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.

NSF young researcher support