CAREER: Towards a Rigorous Methodology for Engineering Robust Software Systems

现代软件系统部署在一个高度动态、不断发展的环境中，有时可能会偏离其预期行为。例如，与放射治疗机交互的治疗师可能无意中以不正确的顺序执行一系列关键操作；通信网络可能经历中断并无法及时传递消息；或者网络上的恶意行为者可能随着时间的推移而演变并获得更广泛的利用。理想情况下，一个健壮的系统将确保即使在环境可能出现偏差的情况下，也能满足其最关键的要求。该项目旨在通过将健壮性提升为一流的质量属性来系统化健壮软件的开发，该属性可以明确地分析并设计成系统。为此，该项目将为软件健壮性奠定严格的基础，并开发一套基本的分析和设计技术，以支持工程健壮系统的方法学。这项研究的结果将被纳入卡内基梅隆大学的软件工程和形式化方法课程。这个项目将研究(1)软件系统健壮性的形式化概念和(2)支持开发健壮系统的活动的规范和验证技术。特别是，该项目将开发技术，将系统的健壮性作为显性属性进行形式推理，以回答以下问题：系统对环境中可能的偏差的健壮性有多强？哪些偏差会导致系统违反关键要求？给出一对可供选择的设计，它们中的哪一个在什么偏差下更健壮？此外，给出一个不能容忍某些偏差的系统模型，该项目将开发使系统健壮的技术，方法是自动将现有设计转换为对这些偏差具有健壮性的设计。最后，该项目将展示健壮性在多个领域的适用性和实用性，特别是通过提议的技术的两个创新应用：(1)安全协议的健壮性测试和(2)安全关键接口的健壮性。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Modern software systems are deployed in a highly dynamic, evolving environment that may occasionally deviate from its expected behavior. For example, a therapist interacting with a radiation therapy machine may inadvertently perform a sequence of critical actions in an incorrect order; a communication network may experience a disruption and fail to deliver messages in time; or a malicious actor on the web may evolve and obtain a wider range of exploits over time. Ideally, a system that is robust would ensure that its most critical requirements are satisfied even under possible deviations in the environment. This project aims to systematize the development of robust software by elevating robustness as a first-class quality attribute that can be explicitly analyzed for and designed into a system. To this end, the project will lay a rigorous foundation for software robustness and develop a set of fundamental analysis and design techniques to support methodologies for engineering robust systems. The results of this research will be incorporated into software engineering and formal method classes at Carnegie Mellon University.This project will investigate (1) a formal notion of robustness for software systems and (2) specification and verification techniques to support activities for developing robust systems. In particular, the project will develop techniques for formally reasoning about the robustness of a system as an explicit property, to answer questions such as: How robust is the system against possible deviations in the environment? What deviations could result in the system violating a critical requirement? Given a pair of alternative designs, which one of them is more robust under what deviations? In addition, given a model of a system that is incapable of tolerating certain deviations, the project will develop techniques for robustifying the system, by automatically transforming the existing design into one that is robust against those deviations. Finally, the project will demonstrate the applicability and utility of robustness across multiple domains, in particular through two innovative applications of the proposed techniques: (1) robustness testing of security protocols and (2) robustification of a safety-critical interface.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.