Search for: All records

Modern software systems are deployed in a highly dynamic, uncertain environment. Ideally, a system that is robust should be capable of establishing its most critical requirements even in the presence of possible deviations in the environment. We propose a technique called behavioral robustification, which involves systematically and rigorously improving the robustness of a design against potential deviations. Given behavioral models of a system and its environment, along with a set of user-specified deviations, our robustification method produces a redesign that is capable of satisfying a desired property even when the environment exhibits those deviations. In particular, we describe how the robustification problem can be formulated as a multi-objective optimization problem, where the goal is to restrict the deviating environment from causing a violation of a desired property, while maximizing the amount of existing functionality and minimizing the cost of changes to the original design. We demonstrate the effectiveness of our approach on case studies involving the robustness of an electronic voting machine and safety-critical interfaces. 

As software is rapidly being embedded into major parts of our society, ranging from medical devices and self-driving vehicles to critical infrastructures, potential risks of software failures are also growing at an alarming pace. Existing certification processes, however, suffer from a lack of rigor and automation, and often incur a significant amount of manual effort on both system developers and certifiers. To address this issue, we propose a substantially automated, cost-effective certification method, backed with a novel analysis synthesis technique to automatically generate application-specific analysis tools that are custom-tailored to producing the necessary evidence. The outcome of this research promises to not only assist software developers in producing safer and more reliable software, but also benefit industrial certification agencies by significantly reducing the manual effort of certifiers. Early validation flows from experience applying this approach in constructing an assurance case for a surgical robot system in collaboration with the Center for the Advanced Surgical Technology.