Assuring Complex Software Systems

许多安全关键系统的复杂性最近以前所未有的方式激增，这主要是由于软件驱动的创新。为了解决安全问题，已经制定了指导此类系统开发的行业特定标准。例如，ISO 26262是汽车功能安全标准，它要求执行某些活动以构建安全的车辆，并将这些活动的结果结合到保证案例（AC）中。安全AC是一种结构化的论证，用于证明系统在其预期环境中足够安全。这个论证被分解，直到有可能收集到一个（子）目标被满足的证据。证据可以是验证结果、测试用例、专家意见等形式。为传统软件系统构建安全论证是困难的——维护它们既耗时又昂贵，尤其是在软件经历变化的时候。安全性也是出了名的非组合性——每个子系统可能是安全的，但它们一起可能会产生不安全的行为。我们也很容易忽略一些情况，在最简单的情况下，这意味着我们提出了一个关于什么时候一个条件为真的论证，而忽略了对一个条件为假的论证。此外，许多基于机器学习（ML）的系统正变得对安全至关重要，例如，最近的特斯拉（Tesla）自动驾驶汽车错误地对紧急车辆进行了分类，并造成了多起撞车事故。基于机器学习的系统通常没有精确指定和机器可验证的需求。虽然有些安全要求可以明确说明：“系统应该检测到十字路口的所有行人”，但这些要求是针对整个系统的，对于单个组件的安全分析来说，这些要求太高了。因此，具有ML组件（mlc）的系统为安全保证增加了一个重要的复杂性层。我相信安全保证应该是构建安全可靠的软件系统的一个组成部分，但是这个过程需要高级软件工程和软件分析的支持。基于我在形式化方法、软件工程、程序分析、安全和机器学习方面的背景，我的研究计划的目标是为开发、确保和维护具有安全问题的复杂软件系统提供可扩展的用户友好支持。建议沿着三个协同和相互关联的重点开展工作：重点1：开发原则性的、工具支持的方法，用于创建、理解、验证、调试和修复保证论证。重点2：发展安全证据再利用和改进技术。主旨3：发展确保mlc系统安全的方法。拟议的研究计划旨在开发和结合跨不同学科的科学和工程基础、工具构建和跨三个重点的广泛实验，以支持更安全软件系统的开发，最终拯救人类生命。

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.