控制单元的程序的形式化验证的制作方法

1.本发明涉及一种用于控制单元的程序的形式化验证的方法和装置。


背景技术：

2.从现有技术中已知对控制单元的程序的形式化验证。程序的形式化验证是程序具有规范中所要求的所有特性的证明。
3.然而，适用于形式化验证的程序表示的生成是一项复杂且容易出错的手动工作。


技术实现要素：

4.因此，本发明的目的是提供一种可以自动执行程序的形式化验证的方法和相应装置。
5.该目的通过独立权利要求的特征来实现。在从属权利要求中说明了有利的实施方式。应指出的是，从属于独立权利要求的权利要求的附加特征在没有独立权利要求的特征或者仅在与独立权利要求的特征子集相组合的情况下可构成独立于独立权利要求的所有特征组合的单独发明，其可成为独立权利要求、分案申请或后续申请的主题。这同样适用于说明书中所述的技术理论，其可形成独立于独立权利要求的特征的发明。
6.本发明的第一方面涉及一种用于控制单元、特别是用于机动车的控制单元的程序的形式化验证的方法。
7.在此，形式化验证是控制单元的程序的正确性的形式化证明或控制单元的程序具有所要求的所有特性的证明。
8.该方法的一个步骤是提供控制单元的程序的图解模型。
9.图解模型是表示一组对象连同这些对象之间存在的连接的抽象结构。在此，对象的数学抽象称为图形的节点。节点之间的成对连接称为边。边可以是定向或非定向的。
10.在此，控制单元的程序的图解模型表示控制单元的程序的行为的模型。图解模型的节点对应于控制单元的程序的内部状态。图解模型的边对应于控制单元的程序的内部状态之间的转换。
11.在此，图解模型的边特别是分别指明对于各个状态转换必须存在的至少一个条件。
12.图解模型特别是一个状态机。
13.该方法的另一步骤是提供控制单元的程序应符合的规范。控制单元的程序应符合的该规范说明了控制单元的程序应符合的特性，其中这些特性例如由程序的开发者预设。
14.该方法的另一步骤是根据控制单元的程序的图解模型来确定克里普克结构。
15.克里普克结构是由四元组(s、s0、r、l)定义的有向图：
16.·
s：状态的有限集合，
17.·
s0：初始状态集合和s的子集，
18.·
r：s中的状态之间的转换关系，以及
19.·
l：标签函数，其将一个状态映射到在该状态下有效的原子逻辑语句。通过标签函数l分配给一个状态的有效原子逻辑语句在下文中被称为“标签”。
20.该方法的另一步骤是检验克里普克结构是否符合控制单元的程序应符合的规范。
21.例如，这可以借助于现有技术中已知的方法模型检查来进行，该已知方法适用于检验克里普克结构是否符合应符合的规范。
22.在本发明的有利实施方式中，根据控制单元的程序的图解模型来确定克里普克结构包括：检验步骤，即检验在存在前置条件的情况下是否可到达控制单元的程序的图解模型的一个节点。
23.在此，前置条件是指在控制单元的程序的图解模型中可能导致状态转换的条件。在该有利的实施方式中，在此考虑与节点处的传入边相关联的条件。
24.为了更好的可读性，特别是关于稍后将说明的另一有利实施方式，这些与节点处的传入边相关联的条件被称为“前置条件”。
25.换言之，方法的该步骤描述了是否可以通过传入边到达图解模型的节点。
26.本发明的该有利实施方式的另一步骤是，如果在存在前置条件的情况下可到达控制单元的程序的图解模型的该节点，则利用控制单元的程序的图解模型的该节点和该前置条件作为标签生成克里普克结构中的节点。
27.特别是如果为图解模型的所有节点执行这些步骤，则由此能够生成克里普克结构的所有节点及其标签。
28.在本发明的另一有利实施方式中，根据控制单元的程序的图解模型确定克里普克结构包括：确定步骤，即确定在存在后置条件的情况下是否可以从控制单元的程序的图解模型的第一节点到达控制单元的程序的图解模型的第二节点。
29.在此，后置条件是在控制单元程序的图解模型中可能导致状态转换的条件。在该有利的实施方式中，在此考虑与节点处的传出边相关联的条件。
30.为了更好的可读性，特别是关于在另一有利实施方式中引入的前置条件，这些与节点处的传出边相关联的条件被称为“后置条件”。
31.换言之，术语“前置条件”和“后置条件”表示控制单元的程序的图解模型的相同元素，即与边相关联的条件。不同的名称只是为了更好的可读性。
32.本发明的该有利实施方式的另一步骤是，如果在存在后置条件的情况下可以从控制单元的程序的图解模型的第一节点中到达控制单元的程序的图解模型的第二节点，则生成克里普克结构中的边，该边从克里普克结构中的其标签包括控制单元的程序的图解模型的第一节点的节点开始到克里普克结构中的其标签包括控制单元的程序的图解模型的第二节点和后置条件的节点。
33.换言之，如果可以经由一个边从图形结构中的第一节点到达第二节点，则在克里普克结构中生成一个边。
34.克里普克结构中的这个边从克里普克结构中其标签包括控制单元程序的图解模型的第一节点的节点开始。克里普克结构中的这个边指向克里普克结构中其标签包括控制单元程序图解模型的第二节点和该边在控制单元程序图解模型中的后置条件的节点。由此，涉及可唯一确定的定向边。
35.为了识别克里普克结构中的边所指向的克里普克结构中的节点，特别是检验克里
普克结构的所有节点的标签。
36.特别是如果对图解模型的所有节点执行这些步骤，则由此可以生成克里普克结构的所有边。
37.在本发明的另一有利实施方式中，提供控制单元的程序的图解模型包括：生成控制单元程序的输入信号的轨迹的步骤，其中控制单元的程序的输入信号的轨迹包括至少一个引起控制单元程序的状态转换的条件。
38.在此，用于控制单元的程序的输入信号特别是离散的且已知的。
39.控制单元的程序的输入信号轨迹的生成可以例如通过从控制单元的程序的已知输入信号集合中必要时随机地选择元素来进行。
40.本发明的该有利实施方式的另一步骤是利用控制单元的程序的输入信号的轨迹来激励控制单元的程序。
41.在此，控制单元的程序本身特别是代表所谓的“黑盒”，从本发明方法的角度来看，其内容是未知的。
42.换言之，利用控制单元的程序的输入信号的轨迹来激励控制单元的程序意味着控制单元的程序的输入信号轨迹的元素被顺序地传输到控制单元的程序作为输入信号。
43.本发明的该有利实施方式的另一步骤是在利用控制单元的程序的输入信号的轨迹激励控制单元的程序之后接收关于控制单元的程序的当前状态的信息。
44.特别是如果在利用输入信号的轨迹激励控制单元的程序之后控制单元的程序没有输出关于控制单元的程序的当前状态的信息，或者该信息指示出当前输入信号促使其状态转换，则输入信号的轨迹的下一元素在该点处已可以被传输到控制单元的程序，因为在这种情况下在该点处已明确的是，对于控制单元的程序的当前状态和当前输入信号不需要生成图解模型中的任何元素。
45.关于控制单元的程序的当前状态的信息特别是控制单元的程序的当前状态本身。
46.本发明的该有利实施方式的另一步骤是根据输入信号的轨迹和关于控制单元的程序的当前状态的信息来生成控制单元的程序的图解模型。
47.根据输入信号的轨迹和关于控制单元的程序的当前状态的信息来生成控制单元的程序的图解模型可以特别是通过如下方式进行，即在图解模型中为控制单元的程序的每个观察状态生成一个节点。
48.图解模型中的边由控制单元的程序的观察状态的观察状态转换的结果产生，其中触发相应状态转换的输入信号可以用作图解模型中相应边的条件。
49.在本发明的另一有利实施方式中，控制单元的程序的输入信号的轨迹包括至少两个分别引起控制单元的程序的状态转换的条件，并且关于控制单元的程序的当前状态的信息没有唯一地识别控制单元的程序的至少一个状态。
50.在本发明的该有利实施方式中，根据输入信号的轨迹和关于控制单元的程序的当前状态的信息生成控制单元的程序的图解模型包括以下步骤：针对关于控制单元的程序的当前状态的信息，确定程序的可能状态的集合。
51.本发明的该有利实施方式的另一步骤是根据由控制单元的程序响应于利用输入信号的轨迹对控制单元的程序的激励所输出的、关于控制单元的程序的当前状态的信息的顺序，去除控制单元的程序的可能状态集合中的至少一个元素。
52.因此，例如通过对由控制单元程序响应于利用输入信号的轨迹对控制单元程序的激励的顺序进行评估，可以区分控制单元程序的不同的内部状态，尽管其可能使得输出关于控制单元程序的当前状态的相同信息。
53.这是由于这些状态的前置条件和后置条件彼此不同，从而随着输入信号的轨迹越来越长，与克里普克结构中的相应状态相关联的程序内部状态的集合变得越来越小，这特别是由于后置条件的重复计算及其与关于控制单元程序的当前状态的信息的组合。
54.本发明的第二方面涉及一种用于控制单元的程序的形式化验证的装置，其中该装置被配置为：提供控制单元的程序的图解模型，提供控制单元的程序应符合的规范，根据控制单元的程序的图解模型确定克里普克结构，并且验证克里普克结构是否符合控制单元的程序应符合的规范。
55.关于根据本发明第一方面的方法的上述陈述也相应地适用于根据本发明第二方面的装置。在此且在权利要求中未明确说明的装置的有利实施例相应于上述或在权利要求中所述的方法的有利实施例。
附图说明
56.下面借助于实施例参考附图来说明本发明。其中：
57.图1示出了根据本发明的图解模型gm的实施例，
58.图2示出了对应于图1中所示的图解模型gm的克里普克结构ks的实施例，并且
59.图3示出了根据本发明的方法的实施例。
具体实施方式
60.图1示出了根据本发明的图解模型gm的实施例。
61.在此例如是机动车的驾驶员辅助系统的图解模型gm，其包括以下状态作为节点：
62.·
101：不可用，
63.·
102：待机，
64.·
103：可用，以及
65.·
104：激活。
66.在此，起始状态101以图形方式突出显示。
67.驾驶员辅助系统的状态转换由以下输入信号触发，这些输入信号在图解模型gm中表示为边的条件：
68.·
111：无错误，
69.·
112：错误，
70.·
113：环境正常，
71.·
114：环境不正常，
72.·
115：关闭，以及
73.·
116：打开。
74.在此，图解模型不是一个完整的图，因此并非所有节点都通过边直接相互连接。
75.相应地，也不是在每个节点中每个条件都激活向另一节点的状态转换。
76.例如，如果图解模型gm处于状态101“不可用”，则条件111“无错误”触发向状态102“待机”的状态转换。然而，在状态101“不可用”中条件113“环境正常”不会触发状态转换，因为没有从节点101出来的边与条件103相关联。
77.图2示出了对应于图1中所示的图解模型gm的克里普克结构ks的实施例。
78.图2中所示的克里普克结构ks根据控制单元sg的程序pc的图解模型gm由本发明的方法确定。
79.在此，起始状态203以图形方式突出显示。
80.根据控制单元sg的程序pc的图解模型gm确定克里普克结构ks包括检验步骤，即检验在存在前置条件111、112、113、114、115、116的情况下是否可以到达控制单元sg的程序pc的图解模型gm的节点101、102、103、104。
81.换言之，在此检验是否可以经由传入边到达图解模型gm的节点101、102、103、104。
82.该方法的另一步骤是，如果在存在前置条件111、112、113、114、115、116的情况下可以到达控制单元sg的程序pc的图解模型gm的节点101、102、103、104，则利用控制单元sg的程序pc的图解模型gm和前置条件111、112、113、114、115、116作为标签生成克里普克结构ks中的节点201、202、203、204、205、206。
83.在本示例中，在存在条件116的情况下可以经由传入边到达图解模型gm的节点104。因此，在克里普克结构ks中生成节点201。该节点分配有标签104和116，即在图解模型gm中可到达的节点104和图解模型中的前置条件116。
84.在存在条件115的情况下，可以经由传入边到达图解模型gm的节点103。因此，在克里普克结构ks中生成节点202。类似于节点201的过程，这分配有标签103和115。
85.在存在条件112的情况下，可以经由传入边到达图解模型gm的节点101。因此，在克里普克结构ks中生成节点203。类似于节点201的过程，这分配有标签101和112。
86.在存在条件111的情况下，可以经由传入边到达图解模型gm的节点102。因此，在克里普克结构ks中生成节点204。类似于节点201的过程，这分配有标签102和111。
87.在存在条件113的情况下，可以经由传入边到达图解模型gm的节点103。因此，在克里普克结构ks中生成节点205。类似于节点201的过程，这分配有标签103和113。
88.在存在条件114的情况下，可以经由传入边到达图解模型gm的节点102。因此，在克里普克结构ks中生成节点206。类似于节点201的过程，这分配有标签102和114。
89.当控制单元sg的程序pc的图解模型gm的所有节点101、102、103、104的所有前置条件111、112、113、114、115、116均已被考虑时，则克里普克结构ks的节点被完全生成。
90.根据控制单元sg的程序pc的图解模型gm确定克里普克结构ks包括确定步骤，即确定在存在后置条件111、112、113、114、115、116的情况下是否可以从控制单元sg的程序pc的图解模型gm的第一节点101、102、103、104到达控制单元sg的程序pc的图解模型gm的第二节点101、102、103、104。
91.如果在存在后置条件111、112、113、114、115、116的情况下可以从控制单元sg的程序pc的图解模型gm的第一节点101、102、103、104到达控制单元sg的程序pc的图解模型gm的第二节点，则生成克里普克结构ks中的边211、212、213、214、215、216、217、218、219、220、221、222、223，这些边从克里普克结构ks中其标签包括控制单元sg的程序gm的图解模型gm的第一节点101、102、103、104的节点201、202、203、204、205、206开始到克里普克结构ks中其标签包括控制单元sg的程序pc的图解模型gm的第二节点101、102、103、104和后置条件
111、112、113、114、115、116的节点。
92.为了清楚起见，在图2中在与沿两个节点中的每一个的方向的边直接连接的该两个节点之间仅绘制有一个边，然而其在每一端都以箭头标记。例如，节点203和204由边211和212连接，其中图2中的图示应理解为，边211从节点203指向节点204，并且边212沿相反方向从节点204指向节点203。这同样适用于连接节点205和206的边214和215以及连接节点201和202的边220和221。
93.在本示例中，在图解模型gm中，在存在后置条件111的情况下可以从第一节点101到达第二节点102。因此，在克里普克结构ks中生成边211。边211从克里普克结构ks中其标签包括第一节点101的节点引出。因此，节点203是边211的起点。边211指向克里普克结构ks中其标签包括图解模型gm的第二节点102和后置条件111的节点。因此，节点204是边211的终点。
94.在图解模型gm中，在存在后置条件112的情况下可以从节点102到达节点101。因此，类似于边211，在克里普克结构ks中生成边212。边212从克里普克结构ks中其标签包括第一节点102的节点引出。因此，节点204是边212的起点。边212指向克里普克结构ks中其标签包括图解模型gm的第二节点101和后置条件112的节点。因此，节点203是边212的终点。
95.在图解模型gm中，在存在后置条件113的情况下可以从节点102到达节点103。因此，类似于边211和212，在克里普克结构ks中生成边213。边213从克里普克结构ks中其标签包括第一节点102的节点引出。因此，节点204是边213的起点。边213指向克里普克结构ks中其标签包括图解模型gm的第二节点103和后置条件113的节点。因此，节点205是边213的终点。
96.类似于边211、212和213，此外还生成边214-223。
97.当控制单元sg的程序pc的图解模型gm的所有节点101、102、103、104的所有后置条件111、112、113、114、115、116均已被考虑时，则克里普克结构ks的边被完全生成。
98.图3示出了根据本发明的方法的实施例，其用于控制单元sg的程序pc的形式化验证。
99.该方法的一个步骤是提供控制单元sg的程序pc的图形模型gm。
100.控制单元sg的程序pc的图解模型gm的提供包括以下步骤：生成控制单元sg的程序pc的输入信号轨迹se，其中控制单元sg的程序pc的输入信号的轨迹se包括至少一个引起控制单元sg的程序pc的状态转换的条件111、112、113、114、115、116。
101.控制单元sg的程序pc的图解模型gm的提供包括另一步骤，即利用控制单元sg的程序pc的输入信号的轨迹se来激励控制单元sg的程序pc。
102.控制单元sg的程序pc的图解模型gm的提供包括另一步骤，即在利用控制单元sg的程序pc的输入信号的轨迹se来激励控制单元sg的程序pc之后，接收关于控制单元sg的程序pc的当前状态101、102、103、104的信息iz。
103.然后根据输入信号的轨迹se和关于控制单元sg的程序pc的当前状态101、102、103、104的信息iz来生成控制单元sg的程序pc的图解模型gm。
104.例如，如果控制单元sg的程序pc处于状态103“可用”并且被输入信号116“打开”激励，则输出关于控制单元sg的程序pc的当前状态的信息iz，其表征状态104“激活”，或者必要时直接输出状态104“激活”。
105.基于该认知，可以在图解模型中插入具有条件116的从节点103到节点104的边。如果在该时间点节点104在图解模型中还不存在，则也可以先插入节点104。
106.如果关于控制单元sg的程序pc的当前状态101、102、103、104的信息iz没有唯一地识别控制单元sg的程序pc的至少一个状态101、102、103、104，则仍然可以生成图解模型gm。
107.为此必要的是，控制单元sg的程序pc的输入信号的轨迹se包括至少两个分别引起控制单元sg的程序pc状态转换的条件111、112、113、114、115、116。
108.在此，可以首先针对关于控制单元sg的程序pc的当前状态101、102、103、104的信息iz，生成程序pc的可能状态101、102、103、104的集合。
109.例如，如果关于控制单元sg的程序的当前状态101、102、103、104的信息iz对于状态101“不可用”和状态102“待机”是相同的，则可以在第一步骤中对于图解模型中的两个位置分别插入集合{101,102}作为可能的状态。
110.在另一步骤中，根据由控制单元sg的程序pc响应于利用输入信号的轨迹se对控制单元sg程序pc的激励所输出的、关于控制单元sg的程序pc的当前状态101、102、103、104的信息iz的顺序，去除控制单元sg的程序pc的可能状态101、102、103、104的集合中的至少一个元素。
111.如果基于可能的状态101、102、103、104的相应集合{101,102}以输入信号{112,111}的轨迹se激励控制单元sg的程序pc，则例如可以唯一地识别状态102，并且可以从该集合{101,102}中去除状态101。
112.该方法的另一步骤是提供控制单元sg的程序pc应符合的规范sp。
113.该方法的另一步骤是根据控制单元sg的程序pc的图解模型gm来确定克里普克结构ks。
114.该方法的另一步骤是例如借助于模型检验器mc来检验克里普克结构ks是否符合控制单元sg的程序pc应符合的规范sp。

技术特征：
1.一种用于控制单元(sg)的程序(pc)的形式化验证的方法，其中所述方法包括如下步骤：
·
提供所述控制单元(sg)的程序(pc)的图解模型(gm)，
·
提供所述控制单元(sg)的程序(pc)应符合的规范(sp)，
·
根据所述控制单元(sg)的程序(pc)的图解模型(gm)来确定克里普克结构(ks)，并且
·
检验所述克里普克结构(ks)是否符合所述控制单元(sg)的程序(pc)应符合的规范。2.根据权利要求1所述的方法，其中根据所述控制单元(sg)的程序(pc)的图解模型(gm)来确定所述克里普克结构(ks)包括如下步骤：
·
检验在存在前置条件(111、112、113、114、115、116)的情况下是否能够到达所述控制单元(sg)的程序(pc)的图解模型(gm)的一个节点(101、102、103、104)，并且
·
如果在存在所述前置条件(111、112、113、114、115、116)的情况下能够到达所述控制单元(sg)的程序(pc)的图解模型(gm)的所述节点(101、102、103、104)，则利用所述控制单元(sg)的程序(pc)的图解模型(gm)的所述节点(101、102、103、104)和所述前置条件(111、112、113、114、115、116)作为标签生成所述克里普克结构(ks)中的节点(201、202、203、204、205、206)。3.根据前述权利要求中任一项所述的方法，其中根据所述控制单元(sg)的程序(pc)的图解模型(gm)来确定所述克里普克结构(ks)包括如下步骤：
·
确定在存在后置条件(111、112、113、114、115、116)的情况下是否能够从所述控制单元(sg)的程序(pc)的图解模型(gm)的第一节点(101、102、103、104)到达所述控制单元(sg)的程序(pc)的图解模型(gm)的第二节点(101、102、103、104)，并且
·
如果在存在所述后置条件(111、112、113、114、115、116)的情况下能够从所述控制单元(sg)的程序(pc)的图解模型(gm)的所述第一节点(101、102、103、104)到达所述控制单元(sg)的程序(pc)的图解模型(gm)的所述第二节点(101、102、103、104)，则生成所述克里普克结构(ks)中的边(211、212、213、214、215、216、217、218、219、220、221、222、223)，所述边从所述克里普克结构(ks)中的其标签包括所述控制单元(sg)的程序(pc)的图解模型(gm)的所述第一节点(101、102、103、104)的节点开始到所述克里普克结构中的其标签包括所述控制单元(sg)的程序(pc)的图解模型(gm)的所述第二节点(101、102、103、104)和所述后置条件(111、112、113、114、115、116)的节点(201、202、203、204、205、206)。4.根据前述权利要求中任一项所述的方法，其中提供所述控制单元(sg)的程序(pc)的图解模型(gm)包括如下步骤：
·
生成所述控制单元(sg)的程序(pc)的输入信号的轨迹(se)，其中所述控制单元(sg)的程序(pc)的输入信号的轨迹(se)包括至少一个引起所述控制单元(sg)的程序(pc)的状态转换的条件(111、112、113、114、115、116)，
·
利用所述控制单元(sg)的程序(pc)的输入信号的轨迹(se)来激励所述控制单元(sg)的程序(pc)，
·
在利用所述控制单元(sg)的程序(pc)的输入信号的轨迹(se)激励所述控制单元(sg)的程序(pc)之后，接收关于所述控制单元(sg)的程序(pc)的当前状态(101、102、103、104)的信息(iz)，并且
·
根据所述输入信号的轨迹(se)和关于所述控制单元(sg)的程序(pc)的当前状态
(101、102、103、104)的信息(iz)生成所述控制单元(sg)的程序(pc)的图解模型(gm)。5.根据权利要求4所述的方法，其中
·
所述控制单元(se)的程序(pc)的输入信号的轨迹(se)包括至少两个分别引起所述控制单元(sg)的程序(pc)的状态转换的条件(111、112、113、114、115、116)，
·
关于所述控制单元(sg)的程序(pc)的当前状态(101、102、103、104)的信息(iz)没有唯一地识别所述控制单元(sg)的程序(pc)的至少一个状态(101、102、103、104)，并且
·
根据所述输入信号的轨迹(se)和关于所述控制单元(sg)的程序(pc)的当前状态(101、102、103、104)的信息(iz)生成所述控制单元(sg)的程序(pc)的图解模型(gm)包括如下步骤：
·
针对关于所述控制单元(sg)的程序(pc)的当前状态(101、102、103、104)的信息(iz)，确定所述程序(pc)的可能状态(101、102、103、104)的集合，并且
·
根据由所述控制单元(sg)的程序(pc)响应于利用所述输入信号的轨迹(se)对所述控制单元(sg)的程序(sg)的激励所输出的、关于所述控制单元(sg)的程序(pc)的当前状态(101、102、103、104)的信息(iz)的顺序，去除所述控制单元(sg)的程序(pc)的所述可能状态(101、102、103、104)的集合中的至少一个元素。6.一种用于控制单元(sg)的程序(pc)的形式化验证的装置，其中所述装置被配置为：
·
提供所述控制单元(sg)的程序(pc)的图解模型(gm)，
·
提供所述控制单元(sg)的程序(pc)应符合的规范(sp)，
·
根据所述控制单元(sg)的程序(pc)的图解模型(gm)来确定克里普克结构(ks)，并且
·
检验所述克里普克结构(ks)是否符合所述控制单元(sg)的程序(pc)应符合的规范。

技术总结
本发明的一个方面涉及用于控制单元的程序的形式化验证的方法。该方法的一个步骤是提供控制单元的程序的图解模型。该方法的另一步骤是提供控制单元的程序应符合的规范。该方法的另一步骤是根据控制单元的程序的图解模型来确定克里普克结构。该方法的另一步骤是检验该克里普克结构是否符合控制单元的程序应符合的规范。合的规范。合的规范。


技术研发人员：南凯弗
受保护的技术使用者：宝马汽车股份有限公司
技术研发日：2021.12.03
技术公布日：2023/10/15