Carnegie Mellon University
Browse

Behavioral Robustness of Software System Designs

Download (4.62 MB)
thesis
posted on 2025-03-18, 21:25 authored by Changjian ZhangChangjian Zhang

Software systems are designed and implemented with assumptions about the environment. However, once a system is deployed, the actual environment may deviate from its expected behavior, potentially leading to violations of desired properties. Ideally, a system should be robust to continue establishing its most critical requirements even in the presence of possible deviations in the environment. To enable systematic design of robust systems against environmental deviations, this work proposes a rigorous behavioral notion of robustness for software systems. Then, it presents a technique called behavioral robustification, which involves two tactics to systematically and rigorously improve the robustness of a system design against potential deviations.

Specifically, the robustness of a system is defined as the largest set of deviating environmental behaviors under which the system is capable of guaranteeing a desired property. Then, we present an approach to compute robustness based on this definition. On the other hand, the system is not robust against an en vironment when the environment exhibits deviations causing a violation of the desired property. The robustification method finds a redesign that is capable of satisfying the property under such a deviated environment. In particular, two tactics, namely robustification-by-control and robustification-by-specification weakening, are introduced. The robustification-by-control tactic formulates the robustification problem as a multi-objective optimization problem with the goal of guaranteeing the desired property while maximally preserving the existing functionality and minimizing the cost of changes to the original design. Then, the specification-weakening tactic is used alongside the control tactic, which allows weakening the property to generate more feasible redesigns that retain more functionality or have a lower cost.

The proposed robustness computation and robustification method are implemented in a tool named Fortis. The applicability and efficiency of these approaches are evaluated through experimental results across five case studies, including a radiation therapy machine, an electronic voting machine, network protocols, a transportation fare system, and an infusion pump machine.

Funding

CAREER: Towards a Rigorous Methodology for Engineering Robust Software Systems

Directorate for Computer & Information Science & Engineering

Find out more...

Collaborative Research: FMitF: Track I: Designing Safe and Robust Human-machine Interactions with Fuzzy Mental Models

Directorate for Computer & Information Science & Engineering

Find out more...

FMitF: Collaborative Research: Track I: Preventing Human Errors in Cyber-human Systems with Formal Approaches to Human Reliability Rating and Model Repair

Directorate for Computer & Information Science & Engineering

Find out more...

SaTC: CORE: Medium: Collaborative: Bridging the Gap between Protocol Design and Implementation through Automated Mapping

Directorate for Computer & Information Science & Engineering

Find out more...

History

Date

2024-12-20

Degree Type

  • Dissertation

Department

  • Software and Societal Systems (S3D)

Degree Name

  • Doctor of Philosophy (PhD)

Advisor(s)

David Garlan Eunsuk Kang