一种用于验证自动飞行系统复杂逻辑的形式化验证方法

摘要

本发明提出了一种用于验证自动飞行系统复杂逻辑的形式化验证方法，该方法包括：步骤1，根据自动飞行系统的复杂逻辑需求构建出形式化验证测试样例；步骤2，采用指定的形式化验证工具，基于自动飞行系统的逻辑模型，运行形式化验证测试样例，生成形式化验证检测报告，用于指示逻辑模型与自动飞行系统逻辑需求的一致性。本发明实施例提供的技术方案，解决了采用现有验证手段对复杂逻辑系统进行验证，由于依赖设计人员对测试用例的设计，从而导致验证方案存在覆盖率不足，验证工作量大等缺点，且不具备保证复杂逻辑系统设计安全性的能力的问题。

说明书

技术领域

本发明涉及自动飞行系统设计验证的技术领域，尤其是指一种用于验证自动飞行系统复杂逻辑的形式化验证方法。

背景技术

飞行控制系统作为飞机的安全关键系统，具有验证覆盖率要求高的特点。针对飞行控制系统的硬件验证、软件验证以及功能验证都有着详尽的规定与标准。设计人员在进行相关功能的开发时，需要借助这些验证测试手段的辅助，对设计结果进行反复的设计验证迭代，保证飞行控制系统的高安全性。

自动飞行系统的设计研制中，由于功能模态的全面需求，不可避免的造成了自动飞行系统功能逻辑的复杂。从数学角度分析，若自动飞行系统包含n个模态，则其中需要验证的转换关系(包含允许转换与禁止转换)则为n*(n-1)条，功能的增加会造成自动飞行系统逻辑的复杂程度呈指数型的上升。

对自动飞行系统的设计和验证，既需要保证自动飞行系统功能的丰富程度，又需要保证复杂逻辑系统设计与需求的一致性。传统的验证手段依赖设计人员对测试用例的设计，而复杂逻辑系统测试用例的设计对于设计人员来说是一个费时、费力且无法保证测试覆盖率的工作。因此采用传统的验证手段存在覆盖率不足，验证工作量大的缺点，已经不具备保证复杂逻辑系统设计安全性的能力。但若不能对复杂逻辑系统进行详尽的测试，日后将会进一步的影响到飞机的安全性。

发明内容

本发明的目的是：本发明实施例提供一种用于验证自动飞行系统复杂逻辑的形式化验证方法，以解决采用现有验证手段对复杂逻辑系统进行验证，由于依赖设计人员对测试用例的设计，从而导致验证方案存在覆盖率不足，验证工作量大等缺点，且不具备保证复杂逻辑系统设计安全性的能力的问题。

本发明的技术方案是：本发明提供了一种用于验证自动飞行系统复杂逻辑的形式化验证方法，包括：

步骤1，根据自动飞行系统的复杂逻辑需求构建出形式化验证测试样例；

步骤2，采用指定的形式化验证工具，基于自动飞行系统的逻辑模型，运行形式化验证测试样例，生成形式化验证检测报告，用于指示逻辑模型与自动飞行系统逻辑需求的一致性。

可选地，如上所述的用于验证自动飞行系统复杂逻辑的形式化验证方法中，所述步骤1包括：

步骤11，对自动飞行系统的复杂逻辑需求进行分析和解算，得到自动飞行系统复杂逻辑的系统逻辑表；

步骤12，根据系统逻辑表，依照形式化验证工具的测试要求，基于自动飞行系统的逻辑需求构建形式化验证测试样例。

可选地，如上所述的用于验证自动飞行系统复杂逻辑的形式化验证方法中，

所述步骤1中所构建出的每条形式化验证测试样例包括：自动飞行系统在转换前所处模态为A模态，转换后所处模态为a模态，由A模态转换到a模态的唯一转换条件为转换条件b，以及转移判定B；所述转移判定B表示A模态仅在转换条件b满足时转换到a模态。

可选地，如上所述的用于验证自动飞行系统复杂逻辑的形式化验证方法中，

所述步骤1中，根据自动飞行系统的复杂逻辑需求，构建符合每条形式化验证测试样例的验证约束，包括：模型输入约束和满足需求期待的模型输出约束，并将验证约束作为形式化验证的输入引入形式化验证工具中；其中，模型输入约束为转换条件b，模型输出约束为A模态或a模态。

可选地，如上所述的用于验证自动飞行系统复杂逻辑的形式化验证方法中，

所述步骤1中所构建出的形式化验证测试样例的验证方式包括：验证证明1和验证证明2；

所述验证证明1用于证明：无论在逻辑模型其他非约束输入为何值时，逻辑模型输出约束与模型输入约束都不存在任何冲突关系

所述验证证明2用于证明：无论在逻辑模型其他非约束输入为何值时，当模型输入约束全满足时，模型输出约束的转换一定会发生，当模型输入约束不全满足时，模型输出约束的转换一定不会发生。

可选地，如上所述的用于验证自动飞行系统复杂逻辑的形式化验证方法中，

所述步骤2中对每条形式化验证测试样例的验证方式为：采用形式化验证工具穷举逻辑模型的所有非约束输入，寻找不满足两个验证证明的反例，若无反例存在，则本条形式化测试样例的验证通过，若有反例存在，则不通过。

可选地，如上所述的用于验证自动飞行系统复杂逻辑的形式化验证方法中，所述步骤2之后，还包括：

步骤3，根据步骤2的试验结果，形成形式化验证报告，记录与预期不相符的验证错误；根据错误对逻辑模型进行修改，采用修改后的逻辑模型运行步骤1中构建出的形式化验证测试样例，直到形式化验证测试样例的验证全部通过。

可选地，如上所述的用于验证自动飞行系统复杂逻辑的形式化验证方法中，所述自动飞行系统的复杂逻辑需求包括以下需求中的至少一种：

飞行指引功能逻辑需求、自动驾驶功能逻辑需求、自动着陆功能逻辑需求、自动推力功能逻辑需求。

可选地，如上所述的用于验证自动飞行系统复杂逻辑的形式化验证方法中，每条形式化验证测试样例包括：形式化验证测试样例程序、测试说明文件。

本发明的有益效果是：本发明实施例提供一种用于验证自动飞行系统复杂逻辑的形式化验证方法，可以根据自动飞行系统的复杂逻辑需求构建出形式化验证测试样例；并且采用指定的形式化验证工具，基于自动飞行系统的逻辑模型，运行形式化验证测试样例，生成形式化验证检测报告，用于指示逻辑模型与自动飞行系统逻辑需求的一致性。本发明实施例提供的技术方案，针对飞机的自动飞行控制系统，使用形式化验证工具，对飞行指引功能逻辑、自动驾驶功能逻辑、自动推力功能逻辑和自动着陆功能逻辑进行全面地穷举测试，确保功能模态切换的正确性、可控性；具体具有以下有益效果：

1、可自动化穷举自动飞行系统功能逻辑中所有转换逻辑的情况；

2、确保自动飞行系统的逻辑设计需求与软件实现的一一对应；

3、减少了设计人员的工作负担，增加了测试效率及正确率；

4、通用性强，可应用于其它领域的复杂逻辑系统的验证方法；

5、提高了自动飞行系统软件的质量和可靠性。

附图说明

为了更清楚地说明本发明实施的技术方案，下面将对本发明的是说了中需要使用的附图作简单的解算。显而易见，下面所描述的附图仅仅是本发明的一些实施例，对于本领域的技术人员来讲，在不付出创造性劳动的前提下，还可以根据这些附图获得其他的附图。

图1为本发明实施例提供的一种用于验证自动飞行系统复杂逻辑的形式化验证方法的流程图；

图2为本发明实施例提供的用于验证自动飞行系统复杂逻辑的形式化验证方法的原理示意图。

具体实施方式

为使本发明的目的、技术方案和优点更加清楚明白，下文中将结合附图对本发明的实施例进行详细说明。需要说明的是，在不冲突的情况下，本申请中的实施例及实施例中的特征可以相互任意组合。

上述背景技术中已经说明，对自动飞行系统的设计和验证，既需要保证自动飞行系统功能的丰富程度，又需要保证复杂逻辑系统设计与需求的一致性。若采用现有验证手段对复杂逻辑系统进行验证，由于依赖设计人员对测试用例的设计，从而导致验证方案存在覆盖率不足，验证工作量大等缺点，且不具备保证复杂逻辑系统设计安全性的能力的问题。

针对飞机的自动飞行系统，本发明实施例提供一种基于形式化验证手段的自动飞行系统复杂逻辑验证的技术方案，用来解决复杂逻辑系统的测试用例设计；减少了设计人员的工作负担，增加了测试效率及覆盖率；验证系统功能与设计需求的一致性；提高了系统的质量和可靠性。

本发明提供以下几个具体的实施例可以相互结合，对于相同或相似的概念或过程可能在某些实施例不再赘述。

图1为本发明实施例提供的一种用于验证自动飞行系统复杂逻辑的形式化验证方法的流程图。本发明实施例提供的形式化验证方法可以包括如下步骤：

步骤1，根据自动飞行系统的复杂逻辑需求构建出形式化验证测试样例；

步骤2，采用指定的形式化验证工具，基于自动飞行系统的逻辑模型，运行形式化验证测试样例，生成形式化验证检测报告，用于指示逻辑模型与自动飞行系统逻辑需求的一致性。

在本发明实施例中，上述步骤1的具体实施过程，可以包括：

步骤11，对自动飞行系统的复杂逻辑需求进行分析和解算，得到自动飞行系统复杂逻辑的系统逻辑表；

步骤12，根据系统逻辑表，依照形式化验证工具的测试要求，基于自动飞行系统的逻辑需求构建形式化验证测试样例。

需要说明的是，该步骤1中自动飞行系统的复杂逻辑需求包括以下需求中的至少一种：飞行指引功能逻辑需求、自动驾驶功能逻辑需求、自动着陆功能逻辑需求、自动推力功能逻辑需求；另外，每条形式化验证测试样例包括：形式化验证测试样例程序、测试说明文件。

在本发明实施例的一种实现方式中，步骤1中所构建出的每条形式化验证测试样例包括：自动飞行系统在转换前所处模态为A模态，转换后所处模态为a模态，由A模态转换到a模态的唯一转换条件为转换条件b，以及转移判定B；所述转移判定B表示A模态仅在转换条件b满足时转换到a模态。

在该实现方式中，步骤1中，根据自动飞行系统的复杂逻辑需求，构建符合每条形式化验证测试样例的验证约束的具体实施方式，可以包括：模型输入约束和满足需求期待的模型输出约束，并将验证约束作为形式化验证的输入引入形式化验证工具中；其中，模型输入约束为转换条件b，模型输出约束为A模态或a模态。

如图2所示，为本发明实施例提供的用于验证自动飞行系统复杂逻辑的形式化验证方法的原理示意图。

步骤1中所构建出的形式化验证测试样例的验证方式包括：验证证明1和验证证明2；

(1)，验证证明1用于证明：无论在逻辑模型其他非约束输入为何值时，逻辑模型输出约束与模型输入约束都不存在任何冲突关系

(2)，验证证明2用于证明：无论在逻辑模型其他非约束输入为何值时，当模型输入约束全满足时，模型输出约束的转换一定会发生，当模型输入约束不全满足时，模型输出约束的转换一定不会发生。

在本发明实施例中，上述步骤2中对每条形式化验证测试样例的验证方式为：采用形式化验证工具穷举逻辑模型的所有非约束输入，寻找不满足两个验证证明的反例，若无反例存在，则本条形式化测试样例的验证通过，若有反例存在，则不通过。举例来说，形式化验证工具例如为形式化验证工具MState。

本发明实施例在实际应用中，在步骤2之后还可以包括：

步骤3，根据步骤2的试验结果，形成形式化验证报告，记录与预期不相符的验证错误；根据错误对逻辑模型进行修改，采用修改后的逻辑模型运行步骤1中构建出的形式化验证测试样例，直到形式化验证测试样例的验证全部通过。

本发明实施例提供的用于验证自动飞行系统复杂逻辑的形式化验证方法，可以根据自动飞行系统的复杂逻辑需求构建出形式化验证测试样例；并且采用指定的形式化验证工具，基于自动飞行系统的逻辑模型，运行形式化验证测试样例，生成形式化验证检测报告，用于指示逻辑模型与自动飞行系统逻辑需求的一致性。本发明实施例提供的技术方案，针对飞机的自动飞行控制系统，使用形式化验证工具，对飞行指引功能逻辑、自动驾驶功能逻辑、自动推力功能逻辑和自动着陆功能逻辑进行全面地穷举测试，确保功能模态切换的正确性、可控性；具体具有以下有益效果：

1、可自动化穷举自动飞行系统功能逻辑中所有转换逻辑的情况；

2、确保自动飞行系统的逻辑设计需求与软件实现的一一对应；

3、减少了设计人员的工作负担，增加了测试效率及正确率；

4、通用性强，可应用于其它领域的复杂逻辑系统的验证方法；

5、提高了自动飞行系统软件的质量和可靠性。

该方法具有验证覆盖率高、设计可操作性强的特点，可大幅提高自动飞行系统复杂逻辑的设计验证效率。

以下通过一个具体实施例对本发明提供的用于验证自动飞行系统复杂逻辑的形式化验证方法的实施方式进行示意性说明。

参照图2所示自动飞行控制系统复杂逻辑的形式化验证方法的原理图，以及参照图1所示自动飞行控制系统复杂逻辑的形式化验证方法的流程图。该具体实施例提供的形式化验证方法可以包括以下步骤：

步骤1：根据自动飞行系统的复杂逻辑需求构建出形式化验证测试样例，设定自动飞行系统在转换前所处模态为A模态，设定转换后所处模态为a模态，由A模态转换到a模态的唯一转换条件为转换条件b，转移判定B为a与b不冲突的判断，该转移判定B表示A模态仅在转换条件b满足时转换到a模态。

步骤2：使用形式化验证工具MState进行形式化验证，采用验证证明1和验证证明2对每条测试样例进行验证；

步骤3：根据试验结果，形成形式化验证报告，记录与预期不相符的验证错误，根据错误，进行逻辑模型的修改与新一轮的形式化验证，直到形式化验证完全通过；

步骤4：形式化验证测试样例的验证全部通过后，生成形式化验证结果文件，为自动飞行系统设计的正确性和与需求的一致性提供证据。

参照图2所示自动飞行系统复杂逻辑的形式化验证方法的原理示意图。具体可以表示自动驾驶模态逻辑转换形式化验证的原理示例图。

根据自动飞行系统的复杂逻辑需求，构造与自动飞行系统中各项需求相关的模型输入约束(即b)和满足需求期待的模型输出约束(即A和a)，将验证约束作为形式化验证的输入引入MState工具中。

针对每个测试样例，定义用于形式化验证的两项验证证明，分别是：

Prove1：无论在逻辑模型的其他非约束输入为何值时，逻辑模型输出约束(A)与模型输入约束(b)都不存在任何冲突关系；

Prove2：无论在逻辑模型其他非约束输入为何值时，当模型输入约束(b)全满足时，模型输出约束的转换一定会发生(即A一定能转到a)，当模型输入约束(b)不全满足时，模型输出约束的转换一定不会发生(即A一定不能转到a)。

形式化验证工具穷举逻辑模型的所有非约束输入的情况，寻找不满足两个证明的反例，若无反例存在，则形式化验证通过，若有反例存在，则不通过。

具体的，针对上述测试样例的具体验证方式为：

所述验证证明1具体验证：自动飞行系统处于A模态下，验证A模态与转换条件b是否出现冲突；若验证为否，则验证策略1通过，若验证为是，则判定本条测试样例无效；

所述验证证明2具体验证：自动飞行系统处于A模态下，验证A模态仅在满足转换条件b的情况下转换为a模态，则验证策略2通过，否则，则判定逻辑模型与复杂逻辑需求不一致。

在本发明的实施例的一些可能的实现方式中，提供的自动飞行系统复杂逻辑的形式化验证方法可以包括但不限于：对飞行指引功能模态转换逻辑的形式化验证(如起飞、风切变模态到其他任意模态的转换逻辑)，对自动驾驶功能模态转换逻辑的形式化验证(如复飞、高度保持、高度截获、垂速、高度层改变等模态到其他任意模态的转换逻辑)，对自动着陆功能模态转换逻辑的形式化验证(如着陆等级转换逻辑与着陆控制模态逻辑)，对自动推力功能模态转换逻辑的形式化验证(如推力模态之间的转换逻辑或推力等级管理功能逻辑等)以及上述功能的通断逻辑的形式化验证。

在本发明的实施例的一些可能的实现方式中，指定的形式化验证工具可以为形式化验证工具MState。

在本发明的实施例的一些可能的实现方式中，自动飞行系统复杂逻辑需求包括以下需求中的一种或者多种：飞行指引功能逻辑需求、自动驾驶功能逻辑需求、自动着陆功能逻辑需求、自动推力功能逻辑需求。

在本发明的实施例的一些可能的实现方式中，形式化验证测试样例包括以下需求中的一种或者多种：形式化验证测试用例、形式化验证测试说明。

最后应该说明的是：以上实施例仅用以说明本发明的技术方案，但本发明的保护范围并不局限于此，任何熟悉本领域的技术人员在本发明揭露的技术范围内，可以轻易想到各种等效的修改或者替换，这些修改或者替换都应该涵盖在本发明的保护范围之内。