Assuring Complex Software Systems

点击翻译按钮获取中文摘要

The complexity of many safety-critical systems has recently surged in an unprecedented manner, mainly due to software-driven innovations. To address safety concerns, industry-specific standards that guide development of such systems have been developed. For example, ISO 26262 is the automotive functional safety standard which mandates the execution of certain activities in order to build safe vehicles, and combining the outcomes of these activities into an Assurance Case (AC). A safety AC is a structured argument used to justify that a system is safe enough to use in its intended environment. The argument gets decomposed until it is possible to collect evidence that a (sub)goal is met. Evidence can be in the form of verification results, test cases, expert opinions, etc. Building safety arguments for traditional software systems is difficult -- they are lengthy and expensive to maintain, especially as software undergoes change. Safety is also notoriously non-compositional -- each subsystem might be safe but together they may create unsafe behaviors. It is also easy to miss cases, which in the simplest case would mean developing an argument for when a condition is true but missing arguing for a false condition.  Also, many machine learning (ML)-based systems are becoming safety-critical, e.g., recent Tesla self-driving cars misclassified emergency vehicles and caused multiple crashes. ML-based systems typically do not have precisely specified and machine-verifiable requirements. While some safety requirements can be stated clearly: "the system should detect all pedestrians at a crossing", these requirements are for the entire system, making them too high-level for safety analysis of individual components. Thus, systems with ML components (MLCs) add a significant layer of complexity for safety assurance. I believe that safety assurance should be an integral part of building safe and reliable software systems, but this process needs support from advanced software engineering and software analysis. Building on my background in formal methods, software engineering, program analysis, safety and machine learning, the goal of my research program is to enable scalable user-friendly support for developing, assuring and maintaining complex software systems with safety concerns.  The work is proposed to commence along three synergetic and interconnected thrusts:   Thrust 1:  Development of principled, tool-supported methodologies for creating, understanding, validating, debugging and repairing assurance arguments.   Thrust 2:  Development of techniques to reuse and improve of safety evidence.   Thrust 3:  Development of methods for assuring safety of systems with MLCs. The proposed research program aims to develop and combine scientific and engineering foundations across different disciplines, tool building and extensive experimentation across the three thrusts to support the development of safer software systems, ultimately saving human lives.