CAREER: Towards a Rigorous Methodology for Engineering Robust Software Systems

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.