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.