SHF: Medium: Assurance Based Development: A Rational Approach To Creating High Assurance Software

本研究的目的是为关键系统创建一种软件开发方法，在这些系统中，高水平的保证对于防止故障产生严重后果是必不可少的。正在开发的方法，基于保证的开发（ABD），是基于贯穿整个开发过程的两个严格的论点。适应性论证表明系统具有满足所有涉众所需的功能性、非功能性（包括法律和道德）和可靠性属性，而成功论证表明开发活动将如何在时间和预算限制内产生令人满意的系统。由于这些参数捕获了所有涉众的关注点，因此它们在任何给定时间的状态都揭示了开发人员所承担的责任。选择满足这些义务的开发活动有助于及早发现和避免潜在的保证困难。选择还允许开发人员部署昂贵的技术，例如形式验证，仅在保证需要它的组件上。ABD的评估和评估正在通过一个原型人工心脏泵和一个安全关键应用的案例研究进行。

The objective of this research is to create an approach to software development for critical systems where a high level of assurance is essential to prevent failures from having serious consequences. The approach being developed, Assurance Based Development (ABD), is based on two rigorous arguments that evolve throughout development. A fitness argument shows that the system has the functional, non-functional (include legal and ethical) and dependability properties necessary to satisfy all stakeholders, and a success argument shows how the development activities will yield a satisfactory system within time and budget constraints. Because these arguments capture the concerns of all stakeholders, their state at any given time reveals the obligations incident on the developers. Choosing development activities to meet these obligations facilitates early detection and avoidance of potential assurance difficulties. Choice also allows the developer to deploy expensive technology, such as formal verification, only on components whose assurance needs demand it.Evaluation and assessment of ABD is being conducted using case studies of a prototype artificial heart pump and a security-critical application.