正确性验证系统、方法、装置和程序与流程

1.本公开涉及正确性验证系统、方法、装置和程序。


背景技术：

2.纯软件、嵌入式系统和网络中的正确性验证一般是耗时间的工作。随着软件程序和嵌入式系统变得越发复杂，这些复杂的系统的正确性验证急剧地变得更加困难，特别是在发生非预期的行为的边缘情况(edge case)或边角情况(corner case)下如此。进一步地，存在对更高级别的约束和正确性进行编码的语言和编程环境，但这些通常是非常地特定于领域(domain)的，需要用该领域特有的方法处理。


技术实现要素：

3.根据实施方式，提供用于决定系统的构成要素中的特性的正确性的方法。
4.方法由电子装置执行，并且包含：
5.设定系统的构成要素的已知特性；
6.动态地决定系统的构成要素的未知特性，其中，动态地决定包含：对动作定义为了正确地执行动作而必须满足的一个以上的前提条件，对动作定义在正确地执行动作之后必须满足的一个以上的后置条件，以及通过测试来识别系统的构成要素的未知特性的界限；
7.验证系统的构成要素的已知特性和系统的构成要素的未知特性；以及
8.为了反映系统的构成要素的已知特性和系统的构成要素的未知特性，更新接口定义语言(idl)程序代码。
9.根据公开的一个方式，提供存储命令的非暂时性计算机可读取介质。
10.非暂时性计算机可读取介质包含一个以上的命令，该一个以上的命令在由装置的一个以上的处理器执行时预测单词的含义，使一个以上的处理器进行：
11.设定系统的构成要素的已知特性；
12.动态地决定系统的构成要素的未知特性，其中，动态地决定包含：对动作定义为了正确地执行动作而必须满足的一个以上的前提条件，对动作定义在正确地执行动作之后必须满足的一个以上的后置条件，以及通过测试来识别系统的构成要素的未知特性的界限；
13.验证系统的构成要素的已知特性和系统的构成要素的未知特性；以及
14.为了反映系统的构成要素的已知特性和系统的构成要素的未知特性，更新接口定义语言(idl)程序代码。
15.根据公开的其他方式，提供用于决定系统的构成要素中的特性的正确性的装置。
16.装置包含：存储器，被构成为存储命令；以及一个以上的处理器，该一个以上的处理器被构成为执行命令，所述命令进行：
17.设定系统的构成要素的已知特性；
18.动态地决定系统的构成要素的未知特性，其中，动态地决定包含：对动作定义为了正确地执行动作而必须满足的一个以上的前提条件，对动作定义在正确地执行动作之后必
须满足的一个以上的后置条件，以及通过测试来识别系统的构成要素的未知特性的界限；
19.验证系统的构成要素的已知特性和系统的构成要素的未知特性；以及
20.为了反映系统的构成要素的已知特性和系统的构成要素的未知特性，更新接口定义语言(idl)程序代码。
附图说明
21.下面参照附图来记述公开的作为例子的实施方式的特征、优点和重要性，在附图中，相似的符号示出相似的要素。
22.图1是实施方式的用于决定系统的构成要素中的特性的正确性的作为例子的过程的流程图的图。
23.图2是实施方式的能够实现在此记述的系统和/或方法的作为例子的环境的图。
24.图3是实施方式的图2的一个以上的装置的作为例子的构成要素的图。
25.图4是实施方式的用于决定系统的构成要素中的特性的正确性的作为例子的过程的流程图。
具体实施方式
26.本公开的实施方式可以涉及验证软件、固件或硬件的正确性。程序一般在程序代码级别指定其含义规则，但是往往过度地约束解决方案，使验证变得非常复杂。因此，即使程序代码或硬件设计以所实现的方式工作，也难以确认程序代码或硬件以所意图的方式工作。这对于如高可用性、安全、功能的安全性、隐私、资源利用等那样的要求验证所有构成要素的领域尤其如此。若干语言和编程环境对更高级别的约束进行编码，以便验证正确性，但其往往是非常地特定于领域的，且并非总是合适的应用领域。
27.本公开的实施方式涉及用能够编码到系统中的正确性、协定、约束和界限信息来增强在这些领域中被良好地接受的现有的编程语言和范例。例如，使用接口定义语言，能够将正确性、协定、约束和界限信息编码到系统中，以便在使用系统时验证系统的这些特性被维持。
28.根据本公开的实施方式，验证系统的特性或系统的构成要素的特性被维持可以包含：验证这些特性在系统的动作范围中维持。动作范围可以是对系统带来影响的因素的记述。根据若干实施方式，动作范围可以是系统的结构化的定义、正式的规范(specification)或者能够在测试或保证系统或系统的形态时使用的对于系统的状态空间的记述。例如，在自主车辆的状况下，动作范围可以包含自主车辆在行驶中可能遭遇的所有的环境和其他因素的记述。
29.与车辆、机器人工程学和其他安全性有关的装置典型地包含一个以上的电子运算单元(ecu)以及这些ecu间的一个以上的通信机构。这些装置中的若干装置对于安全性可能是重要的，并且为了确保功能的安全性，可能必须遵循保证基准，或者必须证明合适的动作界限。本公开的实施方式旨在实现对于与功能的安全性、安全、隐私、资源利用、能源利用等关联起来的特性的正确性验证器。例如，正确性验证器能够确认如最坏情况的执行时间、最坏情况的时间表设定、对于分布式系统中的资源的竞争、误差传播、最坏情况的网络使用、确保安全性和保证基准不矛盾的实现方式等这样的特性。作为例子，正确性验证器为了确
保自主车辆在功能上是安全的，可以确认特性，并且可以识别与实现对于自主车辆的汽车安全水准(asil)的代码有关的界限。
30.根据实施方式，可以通过约束、协定或条件将构成要素的这些重要特性编码到idl层。idl被设计为与编程语言无关，也就是说，idl被设计为能够从一种编程语言中的程序向其他编程语言中的其他程序进行通信，因此将约束、协定或条件编码到idl能够使系统的构成要素具有更高的可移动性。附加地，将约束、协定或条件编码到idl能够更容易地在其他平台中再次使用系统的构成要素，能够更容易地通过如基于无线的更新等方法来更新构成要素。
31.除了提高的可移动性，因为将约束、契约或条件编码到idl，所以还能够提高系统的构成要素的可构成性。根据实施方式，不同的构成要素能够知道且能够验证构成要素的特性的输入和输出的界限，因此能够进行组合、重新实现或废弃。
32.提高的可移动性和可构成性的这些好处可以不仅限制于软件构成要素。本公开的实施方式的正确性验证器也可以在硬件以及仿真中应用。在仿真可能“错误多”时或者在仿真可能具有与实际的硬件不同的设计时，可以为了识别系统的构成要素的行为在两者之间相异的状况、状态或条件而使用正确性验证器。因此，除了提高的可移动性和可构成性，本公开的实施方式还能够提供系统的构成要素的特性的行为不同的状况、状态或条件的识别显示。然后，可以将该识别的差异用于重新设计仿真或实际的硬件，以便提高系统整体的性能。该识别的差异还可以用于通过识别哪些硬件设计特性或功能对于特定的软件的目的是有用的或有害的来对硬件和软件进行共同设计。
33.例如，本公开的实施方式可以用于识别自主车辆的构成要素的特性在仿真和实际的车辆中的行为不同的状况、状态或条件。该差异可以用于测试硬件以及识别硬件在各式各样的特定情况中是否能够以所预期的方式工作，使硬件的测试高速化，缩减确认硬件构成要素的正确性所需的时间。该差异还可以用于决定实际的自主车辆的哪些构成要素(ecu、传感器、传感器的设置和校正等)或自主车辆的软件的哪些构成要素一起工作或者需要重新设计。
34.因此，本公开的实施方式提供对于多个重要特性的正确性验证器。在实际的硬件中以及在仿真中测试的重要特性使得能够进行提高系统的软件和硬件构成要素两者的更高速的设计以及设计系统的软件和硬件构成要素有关的人工劳力和成本的缩减。进一步地，在idl中对这些特性进行编码，提高系统的构成要素的可移动性和可构成性，有效地提高系统的构成要素的效率。
35.图1是在此记述的实施方式的概要的图。如图1中所示，过程100能够决定系统的构成要素中的特性的正确性。
36.如图1中所示，在动作110中，可以设定系统的构成要素的已知特性。系统的构成要素的已知特性可以包含期望系统的构成要素维持或验证的特性。系统的构成要素的已知特性可以基于系统的规范来设定。系统的规范可以是假定系统执行的或不许执行的内容的正式或非正式的记述。在正式的规范中，系统的构成要素的特性可以使用如句法或领域特定的含义规则等特定的结构来表达。该正式的结构可以用于推测关于系统的构成要素的特性的信息和系统的构成要素的特性间的关系。在实施方式中，可以将特定的语言用于规范的记述，语言不限制于下述，但是可以包含抽象状态机(asm)、java建模语言(jml)、对于应用
公共lisp(acl2)的运算逻辑等。作为例子，在车辆或自主车辆的情况下，制动构成要素的已知特性可以是所发出的制动命令可具有最大20毫秒的等待时间。该已知特性可以基于正式的规范设定，可以从法律或保证基准取得或提取。
37.然而，在若干实施方式中，在正式的规范的基础上，或者在没有正式的规范的情况下，根据本公开的实施方式，系统的构成要素的已知特性的设定可以包含：解析系统的设计，解析系统的构成，或者通过基于程序的导出而解析系统的代码。在若干实施方式中，设定系统的构成要素的已知特性可以包含：解析程序代码(例如，如面向对象的编程语言等高级语言，如汇编级语言等低级语言，或者二进制代码)。程序代码可以使用静态程序解析或者可以使用动态程序解析进行解析，可以手动或自动地进行解析。在若干实施方式中，解析程序代码可以包含：实时地，或者在仿真中部分地执行程序。在若干实施方式中，解析系统或系统的构成要素的设计可以包含：解析基于模型的规范。作为例子，可以包含基于解析系统状态模型而设定的构成要素的特性。在若干实施方式中，系统的构成要素的已知特性的设定可以包含：从系统的模型识别已知特性。本公开的实施方式不旨在是限制性的。为了解析系统的设计，为了解析系统的构成，或者为了通过基于用于设定系统的构成要素的已知特性的程序的导出而解析系统的代码，可以使用最先近技术方法的任意的已知方法状态。
38.系统的构成要素的已知特性可以与功能的安全性、安全、隐私、能源利用和资源利用中的至少一个关联起来。例如，已知特性可以基于与功能的安全性、隐私、安全、资源利用、误差传播、内部和外部传感器或系统内的通信关联起来的工业保证基准。
39.在动作120中，可以动态地决定系统的构成要素的未知特性。系统的构成要素的未知特性可以是无法预测的特性、其界限未知的特性、或者其性质能够从一个以上的源推测的特性。例如，系统的构成要素的未知特性可以包含无法在正式的规范中显式地指定且可能需要根据程序代码的部分性的执行来推测的系统的构成要素的特性。
40.系统的构成要素的未知特性可以与功能的安全性、安全、隐私、能源和资源利用中的至少一个关联起来。例如，未知特性可以基于与功能的安全性、隐私、安全、资源利用、误差传播、内部和外部传感器、或系统内的通信关联起来的无法预测的事件或故障。
41.根据若干实施方式，动态地决定系统的构成要素的未知特性可以包含对动作定义一个以上的前提条件，为了正确地执行动作，可以满足一个以上的前提条件。前提条件可以包含在动作的执行之前必须为真或者对于动作的执行必须为真的条件、断言(表明)或系统状态。动作可以是与系统的构成要素的特性关联起来的功能或子部分的执行。作为例子，为了引起自主或自动的车辆车道变更动作，必须为真的前提条件可以包含“方向转换信号必须开启”。
42.根据若干实施方式，动态地决定系统的构成要素的未知特性可以包含对动作定义一个以上的后置条件，可以在正确地执行动作之后满足一个以上的后置条件。后置条件可以包含在动作的正确执行之后必须为真或者为了示出动作的正确执行而必须为真的条件、断言或系统状态。作为例子，在自主或自动车辆的正确的自动的车道变更动作之后，必须为真的后置条件可以包含“如果不进行其他的当前的车道变更，则方向转换信号必须关闭”。
43.根据若干实施方式，动态地决定系统的构成要素的未知特性可以包含：通过测试来识别系统的构成要素的未知特性的界限。识别系统的构成要素的未知特性的界限使得能够理解未知特性和与其关联起来的值以及系统状态。为了识别虽然可能几乎不发生但是可
能使系统的构成要素异常地动作的边角情况或边缘情况，界限的该识别可能是不可缺少的。如前所述，在虽然边缘情况或边角情况的发生极为罕见、但是在发生了时可能具有重大的影响的安全性重要的系统中，可以使用复杂的系统。
44.根据系统的实施方式，识别或证明系统的构成要素的未知特性的界限可以静态地或动态地执行。系统的构成要素的未知特性的界限可以使用数学性的证明或工具来静态地识别或证明。然而，用于动态地决定界限的一种方法可以基于静态证明为何、如何以及在哪儿失败或者无法决定。系统的构成要素的若干特性在理论上可能是不受约束的，但是在实际地执行、测试或应用时，可能出现能够支援识别特性的实际上的界限的实际上的限制。根据公开的实施方式，可以基于系统的构成要素的未知特性的所识别的界限来生成一个以上的测试计划或测试程序。所生成的测试计划或测试程序可以用于动态地测试所有的已知或未知特性，或者可以用于静态地测试为了合理地确保系统的构成要素的已知或未知特性能够在系统的动作范围中维持而所充分的情况。在若干实施方式中，为了测试系统的构成要素的特定的特性的性能，可以进一步改良所生成的测试计划或测试程序。
45.在若干实施方式中，通过测试来识别系统的构成要素的未知特性的界限可以包含用仿真的(进行了模拟试验(仿真)的)系统进行测试。在若干实施方式中，通过测试来识别系统的构成要素的未知特性的界限可以包含测试硬件构成要素。在若干实施方式中，通过测试来识别系统的构成要素的未知特性的界限可以包含用仿真的系统进行测试，并且可以包含测试硬件构成要素。
46.如上所述，根据本公开的实施方式，测试能够在硬件上和在仿真中执行。在仿真可能“错误多”时或者在仿真可能具有与实际的硬件不同的设计时，为了识别系统的构成要素的行为在两者之间相异的状况、状态或条件而使用利用仿真和硬件两者的测试。其还能够支援发现由于关于系统的构成要素或系统整体的不正确的假定而导致的不正确的解决方案或界限。因此，本公开的实施方式能够提供系统的构成要素的已知或未知特性的行为不同的状况、状态或条件的识别。然后，该识别的差异能够用于提高系统整体的性能，用于重新设计仿真或实际的硬件。该识别的差异还可以用于通过识别哪些硬件设计特性或功能可能对于特定的软件的目的是有用的或有害的来对硬件和软件进行共同设计。
47.在动作130中，可以验证系统的构成要素的已知特性和系统的构成要素的未知特性。
48.在若干实施方式中，验证可以基于决定是否能够将系统的构成要素的已知特性和系统的构成要素的未知特性在系统的动作范围内维持。决定能够将系统的构成要素的已知特性和系统的构成要素的未知特性在系统的动作范围内维持可以包含：决定系统的构成要素或系统整体以所预期的方式工作。为了决定系统的构成要素或系统整体是否以所预期的方式工作，可以使用系统的构成要素或系统整体的所预期的行为的列表。在若干实施方式中，系统的构成要素或系统整体的所预期的行为的列表可以手动书写。在若干实施方式中，可以对系统的构成要素或系统整体的所预期的行为的列表进行编码。作为例子，通过约束、协定和条件，使用编程语言对所预期的行为进行编码。在若干实施方式中，所预期的行为可以基于工业保证基准或法律。根据实施方式，系统的构成要素或系统整体的所预期的行为的列表可以是正式或非正式的规范的形式。在系统的构成要素或系统整体的所预期的行为的列表可以是如工业基准或程序代码等那样的非正式的规范的形式的实施方式中，为了生
成列表而可以使用如机器学习、自然语言处理或自动程序解析等那样的任意的合适的技术。
49.在若干实施方式中，验证系统的构成要素的已知特性和系统的构成要素的未知特性可以使用布尔可满足性求解器(boolean satisfiability solver)来执行。作为例子，验证系统的构成要素的已知特性和系统的构成要素的未知特性可以使用戴维斯-普特南-洛吉曼-洛夫兰德(davis-putman-logemann-loveland，dpll)求解器、冲突驱动子句学习(cdcl)求解器、并行sat求解器等sat求解器来执行。在若干实施方式中，验证系统的构成要素的已知特性和系统的构成要素的未知特性可以使用一阶验证引擎(first-order verification engine)来执行。例如，验证系统的构成要素的已知特性和系统的构成要素的未知特性可以使用可满足性模理论(smt)求解器来执行。
50.在若干实施方式中，验证系统的构成要素的已知特性和系统的构成要素的未知特性可以基于正确性的模糊含义或近似性的含义来执行。作为例子，正确性的模糊含义可以在系统的构成要素的已知或未知特性可能是无限的或者测试系统的构成要素的所有的已知或未知特性可能太过于使用资源的若干实施方式中使用。例如，自主车辆中的用于对道路上的交通标识的图像进行分类的已机器学习的模型可以在样本数据集中以试行的特殊比例而模型识别到特殊特性并维持这些特性的情况下验证为正确。合并正确性的该模糊含义可以支援验证使用很多资源的若干特性。这可以通过使用更少的资源来验证特性从而使系统中的资源的使用最优化。
51.根据若干实施方式，验证系统的构成要素的已知特性和系统的构成要素的未知特性可以包含：决定与系统的构成要素的已知特性或系统的构成要素的未知特性关联起来的最坏情况的执行时间。在若干实施方式中，验证系统的构成要素的已知特性和系统的构成要素的未知特性可以包含：决定与系统的构成要素的已知特性或系统的构成要素的未知特性关联起来的最坏情况的误差传播。在若干实施方式中，验证系统的构成要素的已知特性和系统的构成要素的未知特性可以包含：决定与系统的构成要素的已知特性或系统的构成要素的未知特性关联起来的最坏情况的时间表设定。在若干实施方式中，验证系统的构成要素的已知特性和系统的构成要素的未知特性可以包含：决定与系统的构成要素的已知特性或系统的构成要素的未知特性关联起来的最坏情况的网络使用。
52.在动作140中，可以更新用于反映系统的构成要素的已知特性和系统的构成要素的未知特性的接口定义语言(idl)程序代码(interface definition language(idl)program code)。在若干实施方式中，idl程序代码可以基于系统的构成要素的已知特性和系统的构成要素的未知特性的验证结果来自动地更新。在若干实施方式中，idl程序代码可以基于系统的构成要素的已知特性和系统的构成要素的未知特性的验证结果来手动地更新。
53.图1示出过程100的作为例子的块，但是在若干实现方式中，过程100可以包含图1中示出的块以外的追加性的块、比这些更少的块、与这些不同的块或者以与这些不同的方式配置的块。在实施方式中，过程100的作为例子的块的一个以上的块可以以任意的顺序或任意的数量组合或配置。在实施方式中，过程100的2个以上的块可以并行地执行。
54.图2是可以实现在此记述的系统和/或方法的、作为例子的环境200的图。如图2中所示，环境200可以包含用户装置210、平台220和网络230。环境200的装置可以经由有线连
2可以是系统虚拟机或过程虚拟机的任意一个。系统虚拟机可以提供支持完全的操作系统(“os”)的执行的完全系统平台。过程虚拟机可以执行单个程序，可以支持单个过程。在若干实现方式中，虚拟机224-2可以代替用户(例如，用户装置210)执行，可以管理如数据管理、同步或长时间的数据转送等那样的云运算环境222的基础架构。
63.虚拟化存储装置224-3包含有在存储系统内或在运算资源224的装置内使用虚拟化技术的一个以上的存储系统和/或一个以上的装置。在若干实现方式中，在存储系统的情况下，虚拟化的类型可以包含块虚拟化和文件虚拟化。块虚拟化可以指从物理存储装置到逻辑存储装置的抽象化(或分离)，使得能够与物理存储装置或异种的结构无关地访问存储系统。分离使得存储系统的管理者能够在如何管理对于最终用户的存储方面具有灵活性。文件虚拟化可以消除按文件级别访问的数据与文件在物理上所存储的位置之间的依赖性。这使得能够将存储装置的使用、服务器的合并和/或非分割文件转移的执行最优化。
64.管理程序224-4可以提供使多个操作系统(例如，“来宾操作系统”)能够在如运算资源224等那样的主计算机上同时执行的硬件虚拟化技术。管理程序224-4可以向来宾操作系统呈现虚拟动作平台，并且可以管理来宾操作系统的执行。各式各样的操作系统的多个实例可以共享虚拟化硬件资源。
65.网络230包含有一个以上的有线和/或无线网络。例如，网络230可以包含蜂窝网络(例如，第5代(5g)网络、长期演进(lte)网络、第3代(3g)网络、码分多址连接(cdma)网络等)、公共陆地移动通信网络(plmn)、局域网络(lan)、广域网络(wan)、城域网络(man)、电话网络(例如，公共交换电话网(pstn))、私有网络、自组织网络、内部网、互联网、基于光纤的网络等和/或这些或其他类型的网络的组合。
66.图2中所示的装置和网络的数目和配置是作为例子提供的。实际上，可以有在图2中所示的装置和/或网络以外的追加性的装置和/或网络、比这些更少的装置和/或网络、与这些不同的装置和/或网络、或者以与这些不同的方式配置的装置和/或网络。进一步地，图2中所示的2个以上的装置可以在单个装置内实现，或者，图2中所示的单个装置可以实现为多个分散的装置。附加地，或者代替地，环境200的装置的设置(例如，一个以上的装置)可以执行被记述为通过环境200的装置的其他设置执行的一个以上的功能。
67.图3是装置300的作为例子的构成要素的图。装置300可以对应于用户装置210和/或平台220。如图3中所示，装置300可以包含总线310、处理器320、存储器330、存储构成要素340、输入构成要素350、输出构成要素360和通信接口370。
68.总线310包含有使得能够在装置300的构成要素间进行通信的构成要素。处理器320以硬件、固件、或者硬件和软件的组合来实现。处理器320是中央运算处理装置(cpu)、电子控制单元(ecu)、图形处理单元(gpu)、加速处理单元(apu)、微处理器、微控制器、数字信号处理器(dsp)、现场可编程门阵列(fpga)、专用集成电路(asic)或者其他类型的处理构成要素。在若干实现方式中，处理器320包含有为了执行功能而可编程的一个以上的处理器。
69.存储器330包含有随机存取存储器(ram)、只读存储器(rom)和/或存储用于处理器320使用的信息和/或命令的其他类型的动态或静态存储装置(例如，闪速存储器、磁存储器和/或光存储器)。
70.存储构成要素340存储有与装置300的动作和使用有关的信息和/或软件。例如，存储构成要素340可以与对应的驱动器一起包含硬盘(例如，磁盘、光盘、光磁盘和/或固态
盘)、压缩盘(cd)、数字通用盘(dvd)、软盘、磁带盒、磁带和/或其他类型的非暂时性计算机可读取介质。输入构成要素350包含有使装置300能够以如经由用户输入(例如，触摸屏显示器、键盘、小键盘、鼠标、按钮、开关和/或麦克风)等方式接收信息的构成要素。追加地，或者代替地，输入构成要素350可以包含用于感知信息的传感器(例如，全球定位系统(gps)构成要素、加速度计、陀螺仪和/或致动器)。输出构成要素360包含有提供来自装置300的输出信息的构成要素(例如，显示器、扬声器和/或一个以上的发光二极管(led))。
71.通信接口370包含有使装置300能够如以经由有线连接、无线连接、或者有线连接和无线连接的组合等方式与其他装置通信的与收发机相似的构成要素(例如，收发机和/或单独的接收机和发送机)。通信接口370可以使装置300能够从其他装置接收信息和/或向其他装置提供信息。例如，通信接口370可以包含以太网接口、光接口、同轴接口、红外线接口、射频(rf)接口、通用串行总线(usb)接口、wi-fi接口、蜂窝网络接口等。
72.装置300可以执行在此记述的一个以上的过程。装置300可以响应于处理器320执行由如存储器330和/或存储构成要素340等那样的非暂时性计算机可读取介质存储的软件命令来执行这些过程。计算机可读取介质在此被定义为非暂时性存储器装置。存储器装置包含有单个物理存储装置内的存储器空间或者跨越多个物理存储装置扩展的存储器空间。
73.软件命令可以从其他计算机可读取介质或者从其他装置经由通信接口370读入到存储器330和/或存储构成要素340内。存储器330和/或存储构成要素340所存储的软件命令在被执行时可以使处理器320执行在此记述的一个以上的过程。
74.追加地，或者代替地，为了执行在此记述的一个以上的过程，可以代替软件命令或者与软件命令组合地使用布线连接的电路。因此，在此记述的实现方式不限制于硬件电路和软件的任意特定的组合。
75.图3中所示的构成要素的数目和配置是作为例子提供的。实际上，装置300可以包含在图3中所示的构成要素以外的追加性的构成要素、比这些更少的构成要素、与这些不同的构成要素、或者以与这些不同的方式配置的构成要素。追加地，或者代替地，装置300的构成要素的设置(例如，一个以上的构成要素)可以执行被记述为通过装置300的构成要素的其他设置执行的一个以上的功能。
76.在实施方式中，图1的动作的任意一个均可以通过图2～3中所例示的要素的任意一个实现或者使用其来实现。例如，一个以上的动作110～140的任意一个均可以通过用户装置210、平台220、运算资源224或装置300中的一个以上的构成要素中的任意一个以上来实现，或者可以与其对应。
77.图4是在此记述的实施方式的概要的图。如图4中所示，过程400可以生成用于验证系统的构成要素中的特性的正确性的测试计划或测试程序。
78.如图4中所示，在动作410中，可以识别系统的构成要素的特性。系统的构成要素的特性可以包含系统的构成要素的已知特性和系统的未知特性。系统的构成要素的已知特性是可以基于系统的规范来识别的。系统的规范可以是假定系统执行什么或不许执行什么的正式或非正式的记述。在正式的规范中，系统的构成要素的特性可以使用如句法或领域特有的含义规则等那样的特定的结构来表达。该正式的结构可以用于推定关于系统的构成要素的特性的信息和它们之间的关系。在实施方式中，可以将特定的语言用于规范记述，语言不限制于下列，可以包含抽象状态机(asm)、java建模语言(jml)、对于应用公共lisp(acl2)
的运算逻辑等。作为例子，在车辆或自主车辆的情况下，制动构成要素的已知特性可以是所发出的制动命令可具有最大20毫秒的等待时间。该已知特性可以基于正式的规范识别或者从法律或保证基准取得或提取。
79.然而，在若干实施方式中，在对本公开的实施方式的正式的规范追加地，或者在没有正式的规范的情况下，识别系统的构成要素的已知特性可以包含解析系统的设计、解析系统的构成或者通过程序导出而解析系统的代码。
80.在若干实施方式中，识别系统的构成要素的特性可以包含：动态地决定系统的构成要素的未知特性。在若干实施方式中，动态地决定系统的构成要素的未知特性可以包含对动作定义一个以上的前提条件，为了正确地执行动作，可以满足一个以上的前提条件。然后，可以对动作定义一个以上的后置条件，可以在正确地执行动作之后满足一个以上的后置条件。最终地，系统的构成要素的未知特性的界限可以通过测试来识别。
81.系统的构成要素的已知特性和系统的构成要素的未知特性可以与功能的安全性、安全、隐私、能源利用和资源利用中的至少一个关联起来。例如，已知特性可以基于与功能的安全性、隐私、安全、资源利用、误差传播、内部和外部传感器或系统内的通信关联起来的工业保证基准。
82.在动作420中，可以将系统的构成要素的所预期的行为列表化。在若干实施方式中，系统的构成要素或系统整体的所预期的行为的列表可以手动书写。在若干实施方式中，可以对系统的构成要素或系统整体的所预期的行为的列表进行编码。作为例子，可以通过约束、协定和条件，使用编程语言对所预期的行为进行编码。在若干实施方式中，所预期的行为可以基于工业保证基准或法律。根据实施方式，系统的构成要素或系统整体的所预期的行为的列表可以是正式或非正式的规范的形式。在系统的构成要素或系统整体的所预期的行为的列表可以是如工业基准或程序代码等那样的非正式的规范的形式的实施方式中，为了生成列表，可以使用如机器学习、自然语言处理或自动程序解析等那样的任意的合适的技术。
83.在动作430中，可以基于系统的构成要素的所识别的特性和系统的构成要素的所预期的行为来生成用于验证特性的正确性的测试计划或测试程序。根据公开的实施方式，一个以上的测试计划或测试程序是可以基于系统的构成要素的已知特性和系统的构成要素的未知特性的所识别的界限来生成的。所生成的测试计划和测试程序可以用于动态地测试所有的已知或未知特性，或者可以用于静态地测试为了合理地确保系统的构成要素的已知或未知特性能够在系统的动作范围中维持而所充分的情况。在若干实施方式中，可以进一步地精炼所生成的测试计划或测试程序，以便测试系统的构成要素的特定的特性的性能。
84.在动作440中，系统的构成要素的特性的正确性是可以基于所生成的测试计划或测试程序来验证的。基于所生成的测试计划或测试程序来验证系统的构成要素的特性的正确性可以包含：测试或决定系统的构成要素的已知特性和系统的构成要素的未知特性是否能够在系统的动作范围中维持。决定系统的构成要素的已知特性和系统的构成要素的未知特性在系统的动作范围内维持可以包含：决定系统的构成要素或系统整体以所预期的方式工作。为了决定系统的构成要素或系统整体是否以所预期的方式工作，可以使用系统的构成要素或系统整体的所预期的行为的列表。
85.在若干实施方式中，验证系统的构成要素的已知特性和系统的构成要素的未知特性的正确性可以使用布尔可满足性求解器来执行。作为例子，验证系统的构成要素的已知特性和系统的构成要素的未知特性的正确性可以使用如戴维斯-普特南-洛吉曼-洛夫兰德(dpll)求解器、冲突驱动子句学习(cdcl)求解器、并行sat求解器等那样sat求解器来执行。在若干实施方式中，验证系统的构成要素的已知特性和系统的构成要素的未知特性可以使用一阶验证引擎来执行。例如，验证系统的构成要素的已知特性和系统的构成要素的未知特性可以使用可满足性模理论(smt)求解器来执行。
86.在若干实施方式中，验证系统的构成要素的已知特性和系统的构成要素的未知特性可以基于正确性的模糊含义或近似性的含义来执行。作为例子，正确性的模糊含义可以在系统的构成要素的已知或未知特性可能是无限的或者测试系统的构成要素的所有的已知或未知特性可能太过于使用资源的若干实施方式中使用。
87.图4示出过程400的作为例子的块，但是在若干实现方式中，过程400可以包含图4中所示的块以外的追加性的块、比这些更少的块、与这些不同的块或者以与这些不同的方式配置的块。在实施方式中，过程400的作为例子的块的一个以上的块可以以任意的顺序或任意的数量组合或配置。在实施方式中，过程400的2个以上的块可以并行地执行。过程400的各个动作也可以由图2～3的任意装置执行。
88.在实施方式中，示出问题的场景的信息可以包含识别网络的功能不全和基于网络的功能不全而取得的作为例子的信号跟踪的信息。
89.在实施方式中，作为例子的信号跟踪可以示出与网络的功能不全对应的多个重要的性能指标。
90.本公开的实施方式参照所附的附图。在不同的附图中的相同的附图标记可以识别相同或相似的要素。
91.本公开提供例示和记述，但是不旨在网罗全部，另外，也不旨在将实现方式限制于所公开的正确形式。如果考虑上述的公开，则修正和变形是可能的，或者可以从实现方式的实践取得。
92.显然，在此记述的系统和/或方法能够以硬件、固件或者硬件和软件的组合的不同的形式实现。用于实现这些系统和/或方法的实际的特殊化的控制硬件或软件代码不限制实现方式。因此，关于系统和/或方法的动作和行为，虽然在此未提及特定的软件代码进行了记述，但是应理解，软件和硬件可以被设计为基于此处的记述来实现系统和/或方法。
93.如在本领域中习惯性的那样，实施方式可以用执行所记述的一个或多个功能的块来记述和例示。这些块在此处可以称为单元或模块，可以通过如逻辑门、集成电路、微处理器、微控制器、存储器电路、无源电子构成要素、有源电子构成要素、光构成要素、布线连接电路等那样的模拟或数字电路在物理上实现，可以由固件和软件驱动。电路例如可以在一个以上的半导体芯片中或者在如印刷电路基板等那样的基板支撑上具体化。在块中所包含的电路可以通过专用的硬件或者通过处理器(例如，一个以上的编程的微处理器和关联起来的电路)或者用于执行块的若干功能的专用硬件和用于执行块的其他功能的处理器的组合来实现。实施方式的各个块可以在物理上分离为两个以上的相互作用的分离的块。同样地，实施方式的块可以在物理上组合为更复杂的块。
94.在权利要求的范围中列举和/或在说明书中公开了特征的特殊组合，但是这些组
合不旨在限制可能的实现方式的公开。实际上，这些特征多数可以用未在权利要求书中具体列举和/或未在说明书中具体公开的方法进行组合。下述一览中所示的各个从属权利要求可以直接依赖于仅一个权利要求，但是可能的实现方式的公开包含有与权利要求的集合中的所有其他权利要求的组合中的各个从属权利要求。
95.在此所使用的任意要素、行动或命令只要未被显式地记述为是重要的或必不可少的，就不应当被那样地解释。另外，如在此所使用的那样的冠词“某个”旨在包含一个以上的项目，能够与“一个以上”可互换地使用。在旨在仅一个项目时，使用“一个”这样的术语或相似的语言。另外，如在此处所使用那样的术语“具有”、“有”、“包含”、“包含有”等旨在无任何约束的术语。进一步地，关于短语“基于(根据)”，只要未显式地记述为不是那样，就旨在意思是“至少部分地基于(根据)”。
96.如在此所使用的那样，“构成要素”这样的术语旨在被广义地解释为硬件、固件、软件、软件的特征或功能、或者这些的组合。

技术特征：
1.一种由电子装置执行的用于决定系统的构成要素中的特性的正确性的方法，所述方法具备：设定所述系统的所述构成要素的已知特性；动态地决定所述系统的所述构成要素的未知特性；验证所述系统的所述构成要素的所述已知特性和所述系统的所述构成要素的所述未知特性；以及为了反映所述系统的所述构成要素的所述已知特性和所述系统的所述构成要素的所述未知特性，更新接口定义语言idl程序代码，其中，所述动态地决定具备：对动作定义为了正确地执行所述动作而必须满足的一个以上的前提条件；对所述动作定义在正确地执行所述动作之后必须满足的一个以上的后置条件；以及通过测试来识别所述系统的所述构成要素的所述未知特性的界限。2.如权利要求1所述的方法，其中，通过测试来识别所述系统的所述构成要素的所述未知特性的界限具备：用仿真的系统进行测试。3.如权利要求1或2所述的方法，其中，通过测试来识别所述系统的所述构成要素的所述未知特性的界限具备：测试硬件构成要素。4.如权利要求1至3中的任一项所述的方法，其中，所述系统是自主车辆。5.如权利要求1至4中的任一项所述的方法，其中，验证所述系统的所述构成要素的所述已知特性和所述系统的所述构成要素的所述未知特性具备下列中的至少一个：决定最坏情况的执行时间；决定最坏情况的误差传播；决定最坏情况的时间表设定；以及决定最坏情况的网络使用。6.如权利要求1至5中的任一项所述的方法，其中，设定所述系统的所述构成要素的所述已知特性具备：解析所述系统的设计；解析所述系统的构成；或者通过基于程序的导出而解析所述系统的计算机代码。7.如权利要求1至6中的任一项所述的方法，其中，所述验证是基于决定所述系统的所述构成要素的所述已知特性和所述系统的所述构成要素的所述未知特性是否在所述系统的动作范围内维持来进行的。8.如权利要求1至7中的任一项所述的方法，其中，识别所述构成要素的所述未知特性的界限具备：识别与所述构成要素的所述未知特性关联起来的边角情况。9.如权利要求1至8中的任一项所述的方法，其中，验证所述系统的所述构成要素的所述已知特性和所述系统的所述构成要素的所述未知特性是使用布尔可满足性求解器来执行的。
10.如权利要求1至8中的任一项所述的方法，其中，验证所述系统的所述构成要素的所述已知特性和所述系统的所述构成要素的所述未知特性是使用一阶逻辑验证引擎来执行的。11.如权利要求1至10中的任一项所述的方法，其中，所述系统的所述构成要素的所述已知特性和所述系统的所述构成要素的所述未知特性与功能的安全性、安全、隐私、能源利用和资源利用中的至少一个关联起来。12.一种用于决定系统的构成要素中的特性的正确性的装置，所述装置具备：存储器，构成为存储命令；以及一个以上的处理器，所述一个以上的处理器构成为执行所述命令，所述命令进行：设定所述系统的所述构成要素的已知特性；动态地决定所述系统的所述构成要素的未知特性；验证所述系统的所述构成要素的所述已知特性和所述系统的所述构成要素的所述未知特性；为了反映所述系统的所述构成要素的所述已知特性和所述系统的所述构成要素的所述未知特性，更新接口定义语言idl程序代码，其中，所述动态地决定具备：对动作定义为了正确地执行所述动作而必须满足的一个以上的前提条件；对所述动作定义在正确地执行所述动作之后必须满足的一个以上的后置条件；以及通过测试来识别所述系统的所述构成要素的所述未知特性的界限。13.如权利要求12所述的装置，其中，通过测试来识别所述系统的所述构成要素的所述未知特性的界限具备：用仿真的系统进行测试。14.如权利要求12或13所述的装置，其中，通过测试来识别所述系统的所述构成要素的所述未知特性的界限具备：测试硬件构成要素。15.如权利要求12至14中的任一项所述的装置，其中，验证所述系统的所述构成要素的所述已知特性和所述系统的所述构成要素的所述未知特性具备下列中的至少一个：决定最坏情况的执行时间；决定最坏情况的误差传播；决定最坏情况的时间表设定；以及决定最坏情况的网络使用。16.如权利要求12至15中的任一项所述的装置，其中，设定所述系统的所述构成要素的所述已知特性具备：解析所述系统的设计；解析所述系统的构成；或者通过基于程序的导出而解析所述系统的计算机代码。17.如权利要求12至16中的任一项所述的装置，其中，所述验证是基于决定所述系统的所述构成要素的所述已知特性和所述系统的所述构成要素的所述未知特性是否在所述系统的动作范围内维持来进行的。18.如权利要求12至17中的任一项所述的装置，其中，
识别所述构成要素的所述未知特性的界限具备：识别与所述构成要素的所述未知特性关联起来的边角情况。19.如权利要求12至18中的任一项所述的装置，其中，所述系统的所述构成要素的所述已知特性和所述系统的所述构成要素的所述未知特性与功能的安全性、安全、隐私、能源利用和资源利用中的至少一个关联起来。20.一种非暂时性计算机可读取介质，所述非暂时性计算机可读取介质存储有命令，所述命令具备一个以上的命令，所述一个以上的命令在由装置的一个以上的处理器执行时，预测单词的含义，使所述一个以上的处理器进行：设定所述系统的所述构成要素的已知特性；动态地决定所述系统的所述构成要素的未知特性；验证所述系统的所述构成要素的所述已知特性和所述系统的所述构成要素的所述未知特性；为了反映所述系统的所述构成要素的所述已知特性和所述系统的所述构成要素的所述未知特性，更新接口定义语言idl程序代码，其中，所述动态地决定具备：对动作定义为了正确地执行所述动作而必须满足的一个以上的前提条件；对所述动作定义在正确地执行所述动作之后必须满足的一个以上的后置条件；以及通过测试来识别所述系统的所述构成要素的所述未知特性的界限。

技术总结
提供正确性验证系统、方法、装置和程序。一种由电子装置执行的用于决定系统的构成要素中的特性的正确性的方法，该方法具备：设定系统的构成要素的已知特性；动态地决定系统的构成要素的未知特性，其中，动态地决定具备，对动作定义为了正确地执行动作而必满足的一个以上的前提条件，对动作定义在正确地执行动作之后必须满足的一个以上的后置条件，以及通过测试来识别系统的构成要素的未知特性的界限；验证系统的构成要素的已知特性和系统的构成要素的未知特性；以及为了反映系统的构成要素的已知特性和系统的构成要素的未知特性，更新接口定义语言IDL程序代码。口定义语言IDL程序代码。口定义语言IDL程序代码。


技术研发人员：J-F
受保护的技术使用者：织望丰田股份有限公司
技术研发日：2023.03.22
技术公布日：2023/10/6