| Assurance Based Development (ABD) is an approach to the synergistic construction of critical software systems and their assurance arguments. We require assurance of the adequacy of such systems before they are deployed. To that end, developers create hazard assessments, threat models, test results, design analyses, etc. An assurance argument provides the needed explanation of this evidence. In some domains, including several in the United Kingdom, regulations require the preparation of an assurance argument.;ABD is concerned with all stakeholder goals, not solely the software's contribution to system safety. To be fit for use, software must meet an acceptable balance of stakeholder goals, including safety, security, and functionality goals. In ABD, a fitness argument explains how the available evidence supports the conclusion that the software is fit for use.;Stakeholder goals are not limited to software properties: cost and schedule must also be addressed. ABD accommodates goals about the development effort itself in a separate success argument. The success argument documents developers' rationale for believing that the development effort under way will result in a system that is fit for use on time and within budget.;In ABD, the need to provide assurance drives a unique process synthesis mechanism that results in a detailed process for building both software and evidence. At any time, the unsupported portions of the fitness and success arguments represent assurance obligations to be satisfied. In each process synthesis round, the developer chooses to perform a development step that helps to address an obligation. The ABD arguments simultaneously prompt choices and provide a basis for evaluating those choices.;ABD has been evaluated through case studies involving two specimen systems. The University of Virginia LifeFlow is a prototype artificial heart pump. Using ABD, my colleagues and I implemented control software for the pump's magnetic bearings in SPARK Ada and subjected this implementation to a full formal verification. The Tokeneer enclave protection system is a challenge problem inspired by existing National Security Agency systems. Using ABD, I implemented a portion of the Tokeneer software and created an argument demonstrating compliance with Tokeneer's Common Criteria security target. |
