Goals of the Workshop
Software is currently used to control medical devices, automobiles, aircraft, manufacturing plants, nuclear generating stations, space exploration systems, elevators, electric motors, automated trains, banking transactions, telecommunications devices and a growing number of devices in industry and in our homes. Software is also mission critical for many organisations, even if the software does not "control" what happens. Clearly, many of these systems have the potential to cause physical harm if they malfunction. Even if they do not cause physical harm, their malfunctions are capable of causing financial and political chaos. Currently there is no consistent regulation of software, and society is starting to demand 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 any clear guidelines as to what may be regarded as acceptable standards in these situations. Even where the systems are not mission critical, software producers and their customers are becoming interested in methods for assuring quality that may result in software supplied with guarantees.
The purpose of the workshop is to discuss issues related to software certification. We have three invited talks from engaging and over- qualified speakers! We also have four excellent contributed papers from software researchers. Finally, instead of a panel discussion, we have asked our experts to lock horns in a debate - concluding with audience participation.
Tentative Program
| SATURDAY 26 AUG (09:00-17:00) | SUNDAY 27 AUG (09:00-13:00) |
| Invited talk: Rance Cleaveland Does Certification = Verification? Formal Methods And Software Certification |
Examining Certification and Access Control Conflicts Using Deontic Logic - Smith et al |
| Invited talk: Glenn Archinoff Real-Time Software Certification in the Nuclear Power Industry |
A Report of the Current Situation on Software Certification in Japan - Mizuguchi et al |
| Invited talk: Dave Parnas Certification of Software: What, How, and How Confidently |
DEBATE |
Basic Concepts of Software Certification - Fusani et al |
|
| A Maturity Model for Software Product Certification - Heck |
Invited Talks
| David Parnas - McMaster University; University of Limerick | |
| Certification of Software: What, How, and How Confidently |
Where other products have a warranty, software carries a disclaimer. In spite of the widespread use of software in all aspects of our lives, there are still computer experts who are afraid to trust software for such simple tasks as counting votes. One of the signs of a maturing discipline will be software that comes with a document certifying that it is fit for its intended use. This talk deals with some simple questions about certification. - What exactly can we certify in the certificate? - How can we be confident that the certificate is accurate? - How can we measure our confidence? - What can the designers do to increase our confidence? - What can the designers do to decrease the expected damage if we are wrong? |
Rance Cleaveland - University of Maryland; Fraunhofer Center; Reactive Systems |
|
| Does Certification = Verification? Formal Methods And Software Certification |
The growing importance of software in safety-critical systems has led governmental agencies and standards bodies to devise regulations and guidelines on the development and deployment of such software. The underlying motivation for these forms of guidance may be summarized as follows: "Is the software sufficiently likely to behave correctly?" The resulting certification standards have tended, however, to focus on documentable proxies for absolute software correctness, such as development and V&V processes. Formal methods is also devoted to the question of software correctness, although they are not mentioned in typical certification standards. This talk is devoted to exploring why this is the case and to suggesting roles that formal methods might usefully play in certification regimes. |
Glenn Archinoff - Candesco Corporation |
|
| Real-Time Software Certification in the Nuclear Power Industry |
Computer control has been a significant part of the Canadian nuclear power industry since its inception. The Pickering A nuclear power plant just east of Toronto began operation in the early 1970's, and uses a dual redundant computer system to control major functions such as bulk reactor power and the spatial power distribution. More recent nuclear plants have taken advantage of advances in computer hardware and software technology, and use computers in both control and safety functions. The Canadian nuclear industry has been a leader in developing and applying methods to ensure the correctness of software used in applications that require ultra-high confidence in computer systems. This presentation summarizes the development of these methods and how they are deployed in current designs. The presentation describes the process used to categorize the safety significance of software based on its required functions relative to the overall safety of the plant, discusses methods used to qualify embedded software in systems or components supplied by third parties, and describes methods used to certify software developed for safety-critical applications. The presentation also covers regulatory oversight and approval of computer-based, real-time control and safety systems in the Canadian nuclear power industry. |
Contributed Papers
| Mario Fusani, Fabrizio Fabbrini and Giuseppe Lami - National Research Council, Italy | |
| Basic Concepts of Software Certification | This paper examines the subject of software certification together with various related issues through a question/answer paradigm. The general concepts of certification and certification schemes, developed over twenty years of working with the Evaluation Center, are firstly introduced, and then certification problems to do with software technology (products, processes) are commented on. The paper aims to assure the reader that certification schemes can be applied to software, provided their current limitations and expected results are clearly understood. |
Petra Heck - Laboratory for Quality Software, The Netherlands |
|
| A Maturity Model for Software Product Certification | In this paper we describe a framework for assessment of software maturity, called the Software Product Maturity Model. This Maturity Model expresses that the confidence in the absence of faults in a software product increases when formal methods are used for verification of the software product. Maturity is the capability of the software product to avoid failure as a result of faults in the software. From the definition it follows that a software product without faults is the best guarantee for maturity. The absence of faults we call correctness. In our maturity model we cater for an objective evaluation of the correctness of the product. Establishing that faults are absent is also the main topic in certification of (critical) systems, which means our model can be of use in this field. We do not only consider the maturity of the final software product (the source code or working system), but also of intermediate deliverables like requirements and detailed design. In the spirit of the well-known CMMI models we define Product Areas (main product deliverables), Goals per area and Properties per goal. The scores on these properties indicate the Maturity Level of the product or product area. Our Maturity Model is unique in its focus on the product in all its phases and on correctness. It establishes a standard to perform software certification that also includes e.g. expert reviews and formal verification if necessary. It uniformly establishes what to check and how to check it. The checks are not new, but there is no place yet were they all have been put together into one model. |
Daichi Mizuguchi and Satoshi Matsuoka - AIST (CVS), Japan |
|
| A Report of Current Situation on Software Certification in Japan | In Japan, the concern about software certfication is increasing mainly in the following three industrial fields: the safety control equipment industry, the automotive industry, and the measuring instrument industry. In this paper, we report about the current situation of the three industries on software certification. We also report about our activities for software certification in CVS-AIST. |
Melanie Smith, Manasi Kelkar and R. F. Gamble - University of Tulsa, U.S.A. |
|
| Examining Security Certification and Access Control Conflicts Using Deontic Logic | Component-based software has become a mainstream practice as organizations attempt to streamline application development tasks. These applications invariably contain third-party Commercial-off-the-Shelf (COTS) systems with black box functionality. When integrated applications require security certification, COTS components-even if individually certified-may introduce vulnerabilities into the system if their security mechanisms are poorly combined. One cause of improper integration can be found in the access control mappings across COTS component domains. Missing, conflicting, and ambiguous mappings can lead to non-compliance with security certification criteria. In this paper, we discuss certification criteria applicable to COTS integration and their interpretations to access control across domains. Highlighting common conflicts using deontic logic, we indicate how resolution strategies to those conflicts can comply with certification criteria. |
Program Committee
| Stefania Gnesi – Co-Chair | ISTI-CNR, Italy |
| Tom Maibaum – Co-Chair | McMaster University, Canada |
| Rance Cleaveland | University of Maryland, USA |
| Alessandro Fantechi | University of Florence, Italy |
| Jan Friso Groote | Eindhoven University of Technology, The Netherlands |
| Connie Heitmeyer | Naval Research Laboratory, USA |
| Paola Inverardi | University of L'Aquila, Italy |
| S. Purushothaman Iyer | North Carolina State University, USA |
| Yoshiki Kinoshita | CVS-AIST, Japan |
| Dino Mandrioli | Politecnico di Milano, Italy |
| Jonathan Ostroff | York University, Canada |
| Shankar | SRI International, USA |
| David von Oheimb | Siemens AG, Germany |
Organising Committee
| Alan Wassyng |
| Wolfram Kahl |
| Mark Lawford |
| Jeff Zucker |
| (all at McMaster University, Canada) |