Assuring Complex Software Systems

确保复杂的软件系统

• 批准号: RGPIN-2022-03075
• 负责人: Chechik, Marsha
• 金额: $ 3.5万
• 依托单位: University of Toronto
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2022
• 资助国家: 加拿大
• 起止时间: 2022-01-01 至 2023-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=750022
• 关键词: 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.

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