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

这项研究的目标是为关键系统创建一种软件开发方法，在这些系统中，高级别的保证对于防止故障产生严重后果至关重要。正在开发的方法，基于保证的开发(ABD)，基于在整个开发过程中演变的两个严格的论点。合适性论证表明，系统具有满足所有利益相关者所需的功能性、非功能性(包括法律和伦理)和可靠性属性，而成功论证表明，开发活动将如何在时间和预算限制内产生令人满意的系统。因为这些争论抓住了所有利益相关者的关注点，他们在任何给定时间的状态揭示了开发人员的义务事件。选择发展活动来履行这些义务有助于及早发现和避免潜在的保证困难。CHOICE还允许开发人员仅在保证需要的组件上部署昂贵的技术，如正式验证。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.