- Susanne Bach-Bernhard (for administrative matters)
Dagstuhl Seminar Wiki
- Dagstuhl Seminar Wiki (Use personal credentials as created in DOOR to log in)
Software certification, also known as, "licensing", "device approval", etc., has historically been based upon indirect evidence of software quality, namely the process used to produce the software. Academics, regulators, and industry are increasingly viewing process oriented certification as inadequate in light of well documented software intensive system failures. This seminar will examine the current state of the art in methods and tools that can be used in product-focused certification of software intensive systems, working to identify gaps in the current methods and supporting tool infrastructure that need to be filled to facilitate cost effective certification of software intensive systems based upon direct evidence. An important theme will be how tools to produce product focused evidence for certification can be integrated into the forward development process in a way that improves developer productivity rather than becoming an additional burden.
The seminar will address the relationship between how software is developed and, how we collect and use evidence about software to certify it is "fit for use". This includes the pros and cons of the recent trend towards the use of assurance-cases in regulatory regimes. The relationship between assurance-cases and software standards will be a major focus of the seminar. A defining factor in the degree of dependability that can be achieved is the complexity of the system. In order to facilitate software certification we will investigate ways in which we system complexity, including human computer interfaces.
The seminar organizers hope to achieve the following goals:
- Identification and development of industry relevant challenge problems for certification researchers
- Identification of key issues for regulators evaluating software intensive systems
- Determine methods to remove uncertainty currently experienced by industry in the typical certification process
- Determine promising academic research on methods, metrics and processes for certification of critical software, including analytic tools, and human computer interfaces.
- Provide a comparison on the basis of a common case study on the methods and tools ready for industrial use in the certification process.
- Investigate product-focused certification processes and the role of tools
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 , 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" . 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 .
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 . 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.
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
- Methods for the development of certifiable software and methods supporting certification
- 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.
- 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.
- 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.
- 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.
- 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.
- FDA, "FDA Launches Initiative to Reduce Infusion Pump Risks", News Release, April 23, 2010 (see: http://www.fda.gov/NewsEvents/Newsroom/PressAnnouncements/ucm209042.htm)
- 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.
- 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.
- Dominique Blouin (Université de Bretagne Sud, FR) [dblp]
- Darren Cofer (Rockwell Collins - Cedar Rapids, US) [dblp]
- Cyrille Comar (AdaCore - Paris, FR) [dblp]
- Mirko Conrad (The MathWorks GmbH - Ismaning, DE) [dblp]
- John S. Fitzgerald (University of Newcastle, GB) [dblp]
- Kim R. Fowler (Kansas State University, US) [dblp]
- Hubert Garavel (INRIA - Grenoble, FR) [dblp]
- Janusz Górski (Gdansk University of Technology, PL) [dblp]
- Arie Gurfinkel (Carnegie Mellon University - Pittsburgh, US) [dblp]
- John Hatcliff (Kansas State University, US) [dblp]
- Mats P. E. Heimdahl (University of Minnesota - Minneapolis, US) [dblp]
- Constance L. Heitmeyer (Naval Research - Washington, US) [dblp]
- Michael Holloway (NASA Langley ASDC - Hampton, US) [dblp]
- Jozef Hooman (Radboud University Nijmegen, NL) [dblp]
- Jérôme Hugues (ISAE - Toulouse, FR) [dblp]
- Michaela Huhn (TU Clausthal, DE) [dblp]
- Hardi Hungar (DLR - Braunschweig, DE) [dblp]
- Peter Karpati (Institute for Energy Technology - Halden, NO) [dblp]
- Daniel Kästner (AbsInt - Saarbrücken, DE) [dblp]
- Vikash Katta (Institute for Energy Technology - Halden, NO) [dblp]
- Tim Kelly (University of York, GB) [dblp]
- Andrew King (University of Pennsylvania - Philadelphia, US) [dblp]
- John C. Knight (University of Virginia, US) [dblp]
- Brian Larson (Multitude Corp., US) [dblp]
- Mark Lawford (McMaster University - Hamilton, CA) [dblp]
- Dominik Mader (Berner & Mattner Systemtechnik - Berlin, DE) [dblp]
- Tom S. Maibaum (McMaster University - Hamilton, CA) [dblp]
- John McDermid (University of York, GB) [dblp]
- Dominique Méry (LORIA - Nancy, FR) [dblp]
- Frank Ortmeier (Universität Magdeburg, DE) [dblp]
- Richard F. Paige (University of York, GB) [dblp]
- Andras Pataricza (Budapest Univ. of Technology & Economics, HU) [dblp]
- Jan Philipps (Validas AG - München, DE) [dblp]
- Robby (Kansas State University, US) [dblp]
- Julia Rubin (IBM - Haifa, IL) [dblp]
- John Rushby (SRI - Menlo Park, US) [dblp]
- Bernhard Schätz (fortiss GmbH - München, DE) [dblp]
- David von Oheimb (Siemens AG - München, DE) [dblp]
- Alan Wassyng (McMaster University - Hamilton, CA) [dblp]
- Jens Holger Weber (University of Victoria, CA) [dblp]
- Virginie Wiels (ONERA - Toulouse, FR) [dblp]
- dependable systems
- formal methods
- dependable systems
- formal methods
- quality assurance