广告
前沿 | 超越SOTIF：黑天鹅和形式化方法
2021-11-18 09:28:03· 来源：轩辕实验室
本文来自实验室符永乐的研究成果和学习笔记Beyond SOTIF: Black Swans and Formal Methods（题外）「黑天鹅事件」是指满足以下三个特点的事件：第一，它具有意外
本文来自实验室符永乐的研究成果和学习笔记
Beyond SOTIF: Black Swans and Formal Methods
（题外）”「黑天鹅事件」“是指满足以下三个特点的事件：
第一，它具有意外性。
第二，它产生重大影响。
第三，虽然它具有意外性，但人的本性促使我们在事后为它的发生编造理由，并且或多或少认为它是可解释和可预测的。
「摘要」：iso26262标准解决了系统故障和安全减轻这些故障的需要。然而，该标准只是隐含了预期功能的安全性。人们应该承认，一个没有故障的系统，在指定的设计边界内运行应该是安全的。然而，新的ISO/PAS 21448预期功能安全标准(SOTIF)仅明确地解决了与产品设计相关的非预期功能，据称在没有任何系统、元素或组件故障的情况下。这是怎么发生的?是什么保证当代复杂的计算机控制系统在正常情况下总是表现良好，而不会表现出任何可能对用户造成潜在危险的意外和偏差行为?怎样才能解决这个难题呢?本文探讨了「依赖于复杂子系统来产生所需功能的复杂系统中的实际故障」。我们质疑ISO 26262和ISO 21488标准目前在其指导下已经足够解决这个谜。
第一章 介绍
1.随着汽车领域自动化水平的提高（根据SAE J3016），该行业面临着安全保证方面的独特挑战。「车内系统」在整体道路安全中扮演着越来越重要的角色，因为驾驶责任从驾驶员转移到了这些系统，并允许系统决定操作和最终战术级别。
汽车自动化等级划分：
2.由于多种因素，汽车领域的安全挑战是独特的（与航空电子和铁路等其他行业相比）。
「首先」，与其他行业的系统相比，汽车系统的复杂性要高得多。
「其次」，汽车系统运行的环境是不受约束的，包括各种类型的不确定性，这些不确定性导致了对指定运行域的挑战。
「第三」，汽车行业的供应链有许多参与者，而新技术的引入为新来者打开了大门，而新来者并非传统汽车市场的一部分。换句话说，汽车系统的设计分布在庞大而复杂的供应链中；意识到可能的安全问题并负责安全责任并非易事。
「最后」，这一行业的大众市场意味着，与其他交通工具相比，公众对汽车的接触要多得多；因此，潜在的系统安全问题将对社会产生重大影响。
3.确保系统的正确运行被称为“「功能安全」”。自2011年以来，ISO 26262标准（及其后第二次修订版）确立了汽车功能安全的最新水平。本标准给出了在车辆级别识别危险、量化与汽车安全完整性级别（ASIL）相关的风险以及确定缓解或预防这些危险的高级别安全目标的指南和方法。它提供了关于需求层次结构和各种设计、分析和验证方法的建议。先前的研究已经解决了本标准范围内功能安全的系统体系问题。
4.ISO 26262的范围讨论了因项目故障导致的“项目”故障行为而产生的危害。但是，由于车辆的标称行为而可能发生的危险不在本规范的范围内。对缓解或预防故障的关注对于传统汽车系统来说已经足够了，因为传统汽车系统的标称功能具有明确性和确定性。另一方面，对于创新系统，例如自动驾驶应用程序，存在用例和操作领域的不确定性。传感器的局限性和功能不足，再加上关键操作情况，可能导致危险（超出ISO 26262的范围）。这些危险可能是由于车辆内的一组触发条件或驾驶场景的环境状况造成的。在系统开发阶段，这些危险可能“已知”或“未知”。
5.ISO/PAS 21448标准关于预期功能的安全性(SOTIF)解决了上述危害。本文研究了ISO/PAS 21448在涉及系统集成的复杂系统时的基本公理。「由于当前系统过于复杂，关于需求、规格说明、设计实现和操作环境的交互的知识变得不完整。在系统知识不完整、风险管理流程不规范的情况下，异常或非预期的行为可能表现为“黑天鹅”事件」。
6.我们在这篇论文中的贡献是探索黑天鹅事件及其来源，以及作为遏制它们的一种手段的正式方法的检查。系统的安全性和复杂性是对立的。随着复杂性的增加，追踪难以捉摸的黑天鹅事件必须成为系统集成商的当务之急。「黑天鹅」的发现需要一个专门的设计和验证过程，以增加对系统功能安全和SOTIF相关问题安全性的信任。
7.本文的其余部分组织如下：
在第二章中，描述了ISO/PAS 21448的当前范围和内容。
在第三章中，简要概述了形式化方法。
在第四章中，定义了“意外功能”，并提供了一些示例。
在第五章讨论了处理非预期功能的形式化方法的适用性和局限性。
最后，第六章总结本文。
（第一章 主要总结了ISO 21448和ISO26262两个标准的内容和范围，接下来分别对两个标准的内容进行探讨）
第二章 ISO/PAS 21448 SOTIF
1.ISO/PAS 21448标准规定了道路车辆高度自动化驾驶应用的预期功能（SOTIF）的安全性。本标准旨在为需要复杂态势感知的安全关键系统的高级开发提供指南。
2.总的来说，本标准从两个主要角度提供了指南：「从驾驶员的角度」，它提供了更系统的方法（与ISO 26262相比）来分析合理可预见的误用及其潜在的安全风险。，它着重于由于车内系统的标称性能（限制）而可能发生的危险。它特别考虑了「两种」类型的系统限制：感知环境的能力（缺陷），包括传感器融合等相关主题，以及控制算法功能的（不）充分性，包括对不同环境情况的反应。这些限制，再加上作为触发事件的敌方环境条件，可能组合成关键场景，并最终造成危险。我们展示了系统透视图的概述，并将其与图1中ISO 26262的范围进行了比较。
第三章 形式方法
1.形式化方法领域包括一系列技术，用于以严格的数学方法描述、设计和分析系统行为。与大多数其他软件工程方法相比，形式化方法侧重于从数学上证明所设计的软件满足其所需的功能，并在所有情况下遵守所有可能执行的所有安全要求。
2.形式化方法提倡对系统进行建模和评估的「三步方法」。「第一步」是研究中系统的正式规范：设计师或工程师通过描述系统的所有相关行为，使用正式建模语言定义系统。描述通常可以看作是一个状态机。这些形式规范是用自然语言或纯文本编写系统规范的替代方法。以这种方式描述整个系统行为的一部分并不少见，例如内部通信协议、高度安全关键组件的控制或其作为服务提供的接口。
3.在「第二步」中，工程师写下对行为的要求。这些要求可以是安全性质的（机器不能启动两次，中间不能正确停止），可以描述最终行为（制动器控制器必须在制动器按下时始终接收信号），或者是更复杂的性质（系统将在请求时报告自上次检查以来发动机中发生的所有错误）。
4.编写这样的需求至关重要的一个基本遵循原则是，从人的角度来说，不可能写出一个能够很好地处理所有可能情况的模型——更不用说软件了。通过检查软件是否始终符合明确表示的要求，引入了一种保护措施，以防止通常不可避免的疏忽。原则上，对实际软件进行检查是可能的，但是现代编程语言是如此的通用，语义复杂，并且包含了如此多的不相关的行为细节，以至于对成熟软件的检查需求是站不住脚的。
5.在形式化方法中，对所有可能的运行都用数学的严格性检查需求，以确保系统行为总是按照需求运行。当系统行为中的状态数量太大时，就会遇到一个挑战，那些建立系统模型的人必须积极地以这样一种方式设计系统，即状态空间足够小，以启用验证[14]。
6.请注意，使用测试时，系统的许多可能运行都没有包括在内。测试覆盖率通常代表语句覆盖率，这意味着变量值的许多特定组合永远不会被处理，因为这被认为是不可能的。尽管测试是一种比验证弱得多的技术，但放弃它是一个坏主意，因为测试可能会覆盖模型或需求中未捕获或未正确捕获的方面。从不同的角度检查和分析软件是获得高质量的必要条件。
7.最后，一旦指定并验证了模型，就可以通过将规范转换为常规编程代码来实现。这可以自动完成，但手动转换也是一个不错的选择。将模型转换为软件相对容易，并且可以由熟练工人以快速可靠的方式完成。在这样的转换中引入问题是可能的，但一般来说，它们远没有建模和验证可以避免的错误复杂。
8.尽管在模型、需求及其验证方面花费了额外的努力，但形式化方法的使用总体上更为有效，因为在设计实现之前发现可用性缺陷可以节省时间。形式化方法可以防止在开发的后期出现代价高昂的错误。使用形式化方法和经典设计方法对类似项目进行仔细分析后发现，形式化方法所需的工作量最多可减少三倍，同时将错误减少到10倍，通常只留下浅显的软件错误供测试人员发现。
9.软件建模的基本概念是状态机。状态机具有状态以及这些状态之间的转换。状态表示软件在某些静态情况下的状态，转换表示计算或交互如何导致状态更改。转换和状态具有指示其功能的标签。例如，一个转换可以用“开”来标记，表示机器打开时进行转换。
10.不幸的是，系统太复杂了，不能直接由状态机建模。因此，已经开发出了允许表达状态机的形式。在20世纪80年代，过程代数被设计用来模拟系统行为。最值得注意的是「通信过程演算(CCS)」，「通信进程代数(ACP)「和」通信顺序进程(CSP)」。另一种更适合于数据流应用的形式是Petri网络。
11.这些基本形式已通过数据、时间、有时甚至概率来扩展，以描述更先进的系统。对于Petri网，人们通常会进入有色Petri网领域，而在过程代数中，人们会看到诸如LOTOS-NT、FDR或mCRL2等语言[16]，所有这些语言都带有大量的工具集用于验证。
12.要对需求建模，需要使用逻辑。典型地，人们会使用模态逻辑，即命题逻辑或带有模态的谓词逻辑的扩展。这些模式通常表示某些行为可以或不可以发生，以及如果发生了，随后应该发生什么。典型逻辑有CTL逻辑、LTL逻辑、Hennessy-Milner逻辑和模态黏液逻辑。如果用数据和时间扩展这些逻辑，它们就会变得非常具有表现力。最具表现力的逻辑是时间和数据的模态微积分。
13.一个典型且可能令人深省的发现是，如果要对状态机进行建模，使用哪种形式主义几乎无关紧要。当行为以一种形式建模时，它可以很容易地转化为另一种形式。但通常情况下，将自然语言中的非正式规范转换为模型既困难又耗时，因为这些规范往往不完整、不一致且模棱两可。关于需求规范，仍有一场争论在进行，LTL/CTL被认为更直观，而模态微积分更具表现力，但学习曲线更陡峭。
第四章 非预期功能
1.如前所述，SOTIF危险不要求任何组件或元件（硬件或软件）存在缺陷。元素之间关系的非预期属性足以产生异常的未知安全或不安全行为，这可能超出ISO/PAS 21448中当前处理的已确认触发事件。这些相互作用的指数组合性质将压倒任何预测和缓解意外系统行为的最佳努力。
2.此外，车内系统已经被视为系统中的系统，并且变得非常复杂。因此，智能构思和管理复杂系统交互的能力现在已经被构建这些系统的能力所超越。
3.我们建议通过两种渠道引入任何非预期功能/行为：
「第一种」是预期功能意外暴露于设计领域之外的场景/操作情况。意外触发或触发源可能是系统元素交互的产物。
「第二种」类型是由于未知依赖关系、不完全干扰或导致非预期功能的非预期紧急行为而导致的未发现的共存问题。
（第一种是系统内部可能会出现的危险因素，第二种是环境方面可能导致的危险因素）
4.紧急行为是无意中嵌入系统并在特定条件下或通过一系列状态转换在意外时刻浮出水面的行为。紧急行为可以有不同的解释：首先，紧急行为可以是系统在意外事件或事件序列之后出现的未定义行为。「例如」，假设处于主动模式的巡航控制系统监控制动踏板，以便在踩下踏板时可以停用。如果制动踏板在按下和释放时都提供触发信号，则处于活动模式的控制器不会期望制动踏板释放触发器，并可能导致未定义的行为。这种情况可能是用户在踩下制动踏板时激活巡航控制系统的结果。其次，紧急行为可能是组合系统的结果，其中任何一个组件中都不存在意外行为，但它们的交互结果会产生意外状态。「例如」，1995年阿丽亚娜5号导弹的坠毁，耗资5亿美元，是将旧的阿丽亚娜4号软件与更新的组件相结合的结果，这些组件对惯性参考系统[20]的水平偏差有不同的定义。意外的过载事件导致控制系统崩溃。另一个更常见的例子是通信系统之间的竞争条件。控制系统需要能够处理所有可能的事件组合。
5.在图2中，我们展示了一个框架来捕获这些概念与ISO/PAS 21448和ISO 26262中所涵盖项目之间的关系。我们使用三个抽象级别：系统、车辆和环境。从物理架构的角度来看，在这些抽象级别中，我们分别拥有系统、车辆和操作域。此外，从逻辑架构的角度来看，系统具有功能，车辆显示涉及系统功能的行为，操作域捕获场景（包括各种车辆（或道路用户）行为）。在逻辑的角度来看，我们考虑一个隐藏层捕捉非预期的功能，紧急行为，以及未知的场景。在此框架中，我们捕获了系统故障、车辆故障行为和关键场景的功能安全问题。在本框架中，故障行为（如ISO 26262所述）和关键场景都被视为危险。我们使用箭头显示这些概念之间的因果关系，并区分ISO 26262和ISO/PAS 21448的范围。
第五章 讨论
1.形式化方法（formal method）已经存在了一段时间，但尚未得到广泛使用。一般来说，形式化方法在工程界具有负面的含义，通常被视为教育玩具。以下是与形式化方法相关的典型问题列表：
（1）可访问性—形式方法本质上是数学方法，需要深厚的数学专业知识来应用它们。
（2）可拓展性—由于状态空间爆炸的问题，形式化方法对它们能够处理的问题的大小有限制。
（3）适用性—形式化方法是领域特定语言（DSL），仅在孤立的领域中可用。
（4）探索—理解形式主义很有挑战性，因此很难想象基于形式主义的系统将如何工作。
（5）转换—形式化模型必须转换为可针对目标硬件编译的代码。一般来说，数学模型不能自动转换。
（6）学术性——尽管它们在学术界已经存在多年，但在行业环境中还没有大规模使用（可能是因为上述原因）。
2.考虑到所有可能的技术，我们只能说形式化方法的潜在好处。因此，我们将这些定义为示例，并不打算提供详尽的列表：
（1）完整性：一般来说，形式化方法强制执行明确的规范。规范中的漏洞被检测并报告为完整性问题。
（2）合规性，功能正确性：如果规范和实现被正式定义，那么它们之间的合规性可以通过数学证明。
（3）确定性：可以验证形式化描述是否完全是确定性的
（4）死锁、活锁、死代码：这些是状态密集型系统中的典型情况，可以通过正式方法轻松检测到，或者换句话说，可以证明它们的缺失。
第六章 结论
ISO/PAS 21448 SOTIF即将完成，是提高（自动）车辆安全性的重要一步。然而，我们声称这不是感到自满和退缩的理由，因为在我们看来，仍然有一些领域没有得到很好的覆盖。我们通过使用形式化方法查看隐藏的行为，获得了一些关于管理系统的复杂性和增加信任的建议。我们提出了一个框架来捕捉设计和功能安全的基本概念之间的关系。我们没有讨论正式方法的操作细节，但参考了有关该主题的各种来源。这些建议应视为对ISO/PAS 21448 SOTIF的补充。我们认为，随着自动驾驶的发展，随着行业的发展，将出现更多的标准和同质数据库，涵盖当前关于未知场景和功能不足的担忧。因此，设计重点将逐渐转向本文所述的紧急行为。
- 下一篇：典型混动构型方案对比
- 上一篇：国汽智控发布智能汽车基础脑iVBB2.0
广告
最新资讯
-
广汽研究院祁宏钟：汽车加速出口，内燃机也
2024-04-30 16:39
-
中国保险汽车安全指数2024年第一批测评车型
2024-04-30 16:37
-
车门碰撞解锁，无需“遥遥领先”
2024-04-30 12:50
-
“并联”、“串联”和“混联”哪种混动汽车
2024-04-30 12:46
-
直播｜Keysight：软件定义车辆的测试挑战和
2024-04-30 12:34
广告
广告
