一种应用软件形式化模型验证方法及装置

摘要

本发明实施例公开一种应用软件形式化模型验证方法及装置。该方法包括：获取待验证的应用软件形式化模型；基于自动化的模型转换工具Beagle Translator，将应用软件形式化模型中的各进程模型转换为对应的模块模型，将应用软件形式化模型中的功能安全性质转换为对应的待验证属性，得到扩展标签迁移模型，并对扩展标签迁移模型进行功能安全性质验证；基于自动化的模型转换验证工具Proverif Translator，对应用软件形式化模型进行模型预定义、初始化信息转换、状态机模型转换、以及信息安全性质转换，得到基于π演算的进程代数模型，并对进程代数模型进行信息安全性质验证。应用本发明实施例提供的方案，能够提高模型验证效率。

说明书

技术领域

本发明涉及模型验证技术领域，具体而言，涉及一种应用软件形式化模型验证方法及装置。

背景技术

应用软件模型验证技术以构造阶段的质量保证为目标，以模型验证关键技术作支撑，确保软件模型的安全性。

应用软件的分布式特性使得软件模型包含多个模块，极易产生组合空间爆炸问题。已知的模型验证方法中，为了应对模型检测的空间爆炸问题，快速高效地找出系统中违背安全属性的反例，可以采用限界模型检测的方法，将模型逐步展开，验证给定的安全属性是否成立。然而，上述方法需要将模型逐步展开进行验证，过程繁杂，且只能验证模型的安全属性，从而导致模型验证效率较低。因此，为了提高模型验证的效率，亟需一种模型验证方法。

发明内容

本发明提供了一种应用软件形式化模型验证方法及装置，以提高模型验证的效率。具体的技术方案如下。

第一方面，本发明实施例提供一种应用软件形式化模型验证方法，所述方法包括：

获取待验证的应用软件形式化模型；

基于自动化的模型转换工具Beagle Translator，将所述应用软件形式化模型中的各进程模型转换为对应的模块模型，将所述应用软件形式化模型中的功能安全性质转换为对应的待验证属性，得到扩展标签迁移模型，并对所述扩展标签迁移模型进行功能安全性质验证；

基于自动化的模型转换验证工具Proverif Translator，对所述应用软件形式化模型进行模型预定义、初始化信息转换、状态机模型转换、以及信息安全性质转换，得到基于π演算的进程代数模型，并对所述进程代数模型进行信息安全性质验证。

可选的，所述基于自动化的模型转换工具Beagle Translator，将所述应用软件形式化模型中的各进程模型转换为对应的模块模型，将所述应用软件形式化模型中的功能安全性质转换为对应的待验证属性，得到扩展标签迁移模型的步骤包括：

基于自动化的模型转换工具Beagle Translator，针对所述应用软件形式化模型中的每个进程模型，将该进程模型的进程属性转换成为模块模型的变量声明，将该进程模型中的通信信道转换成为所述模块模型的标签声明，将该进程模型中的有限状态自动机中的状态转换成为所述模块模型中的位置声明，从该进程模型中的初始化信息转换得到所述模块模型的初始化迁移，从该进程模型的状态机模型的状态迁移转换得到所述模块模型中的状态迁移；所述状态迁移包括进程方法的状态迁移以及通信动作的状态迁移；

将使用时序逻辑CTL的不变式条件描述的功能安全性质AG f转换成为模型检测工具的待验证属性INVARSPEC f，得到扩展标签迁移模型。

可选的，所述对所述扩展标签迁移模型进行功能安全性质验证的步骤包括：

将所述扩展标签迁移模型输入模型检测工具Beagle中，得到功能安全性质验证结果。

可选的，所述基于自动化的模型转换验证工具Proverif Translator，对所述应用软件形式化模型进行模型预定义、初始化信息转换、状态机模型转换、以及信息安全性质转换，得到基于π演算的进程代数模型的步骤包括：

将所述应用软件形式化模型中的进程属性、进程方法以及通信信道转换成为对应的变量类型定义、进程方法声明以及通信信道声明；

将所述应用软件形式化模型中的初始化信息转换成为对应的进程代数模型中的初始化进程；

将所述应用软件形式化模型中的状态机模型转换成所述进程代数模型中的通信进程模型；

将所述应用软件形式化模型中的信息安全性质进行转换，得到基于π演算的所述进程代数模型。

可选的，所述将所述应用软件形式化模型中的进程属性、进程方法以及通信信道转换成为对应的变量类型定义、进程方法声明以及通信信道声明的步骤包括：

将所述应用软件形式化模型中所有自定义的进程属性声明出来，根据所述应用软件形式化模型的进程方法中的构造方法以及析构方法转换成为对应的进程代数模型中的进程方法声明，根据所述应用软件形式化模型中的通信信道及私有性在进程代数模型中声明通信信道；

所述将所述应用软件形式化模型中的初始化信息转换成为对应的进程代数模型中的初始化进程的步骤包括：

将所述应用软件形式化模型中的初始化信息中的进程属性在初始化进程中声明出来，并且作为对应的进程模型的输入参数生成初始化进程模板；

所述将所述应用软件形式化模型中的状态机模型转换成所述进程代数模型中的通信进程模型的步骤包括：

在所述应用软件形式化模型的进程模型中声明所有在这个进程中用到的变量，将进程模型的状态机模型中的状态转换成为进程代数模型中的事件并声明，将状态机模型中的状态迁移根据进程方法的状态迁移或通信动作的状态迁移转换得到所述进程代数模型中的语句；

将所述应用软件形式化模型中的信息安全性质进行转换的步骤包括：

将信息安全性质中的机密性转换成为所述进程代数模型中的机密性查询语句，将信息安全性质中的认证性转换成为所述进程代数模型中的认证性查询语句。

可选的，所述对所述进程代数模型进行信息安全验证的步骤包括：

将所述进程代数模型输入协议分析工具Proverif中，得到信息安全性质验证结果。

第二方面，本发明实施例提供一种应用软件形式化模型验证装置，所述装置包括：

模型获取模块，用于获取待验证的应用软件形式化模型；

功能安全验证模块，用于基于自动化的模型转换工具Beagle Translator，将所述应用软件形式化模型中的各进程模型转换为对应的模块模型，将所述应用软件形式化模型中的功能安全性质转换为对应的待验证属性，得到扩展标签迁移模型，并对所述扩展标签迁移模型进行功能安全性质验证；

信息安全验证模块，用于基于自动化的模型转换验证工具Proverif Translator，对所述应用软件形式化模型进行模型预定义、初始化信息转换、状态机模型转换、以及信息安全性质转换，得到基于π演算的进程代数模型，并对所述进程代数模型进行信息安全性质验证。

可选的，所述功能安全验证模块包括：

模块转换子模块，用于基于自动化的模型转换工具Beagle Translator，针对所述应用软件形式化模型中的每个进程模型，将该进程模型的进程属性转换成为模块模型的变量声明，将该进程模型中的通信信道转换成为所述模块模型的标签声明，将该进程模型中的有限状态自动机中的状态转换成为所述模块模型中的位置声明，从该进程模型中的初始化信息转换得到所述模块模型的初始化迁移，从该进程模型的状态机模型的状态迁移转换得到所述模块模型中的状态迁移；所述状态迁移包括进程方法的状态迁移以及通信动作的状态迁移；

功能安全性质转换子模块，用于将使用时序逻辑CTL的不变式条件描述的功能安全性质AG f转换成为模型检测工具的待验证属性INVARSPEC f，得到扩展标签迁移模型。

可选的，所述功能安全验证模块，具体用于将所述扩展标签迁移模型输入模型检测工具Beagle中，得到功能安全性质验证结果。

可选的，所述信息安全验证模块包括：

预定义子模块，用于将所述应用软件形式化模型中的进程属性、进程方法以及通信信道转换成为对应的变量类型定义、进程方法声明以及通信信道声明；

初始化信息转换子模块，用于将所述应用软件形式化模型中的初始化信息转换成为对应的进程代数模型中的初始化进程；

状态机模型转换子模块，用于将所述应用软件形式化模型中的状态机模型转换成所述进程代数模型中的通信进程模型；

信息安全性质转换子模块，用于将所述应用软件形式化模型中的信息安全性质进行转换，得到基于π演算的所述进程代数模型。

可选的，所述预定义子模块，具体用于：将所述应用软件形式化模型中所有自定义的进程属性声明出来，根据所述应用软件形式化模型的进程方法中的构造方法以及析构方法转换成为对应的进程代数模型中的进程方法声明，根据所述应用软件形式化模型中的通信信道及私有性在进程代数模型中声明通信信道；

所述初始化信息转换子模块，具体用于：将所述应用软件形式化模型中的初始化信息中的进程属性在初始化进程中声明出来，并且作为对应的进程模型的输入参数生成初始化进程模板；

所述状态机模型转换子模块，具体用于：在所述应用软件形式化模型的进程模型中声明所有在这个进程中用到的变量，将进程模型的状态机模型中的状态转换成为进程代数模型中的事件并声明，将状态机模型中的状态迁移根据进程方法的状态迁移或通信动作的状态迁移转换得到所述进程代数模型中的语句；

所述信息安全性质转换子模块，具体用于：将信息安全性质中的机密性转换成为所述进程代数模型中的机密性查询语句，将信息安全性质中的认证性转换成为所述进程代数模型中的认证性查询语句。

可选的，所述信息安全验证模块，具体用于将所述进程代数模型输入协议分析工具Proverif中，得到信息安全性质验证结果。

由上述内容可知，本发明实施例提供的应用软件形式化模型验证方法及装置，可以获取待验证的应用软件形式化模型；基于自动化的模型转换工具Beagle Translator，将应用软件形式化模型中的各进程模型转换为对应的模块模型，将应用软件形式化模型中的功能安全性质转换为对应的待验证属性，得到扩展标签迁移模型，并对扩展标签迁移模型进行功能安全性质验证；基于自动化的模型转换验证工具Proverif Translator，对应用软件形式化模型进行模型预定义、初始化信息转换、状态机模型转换、以及信息安全性质转换，得到基于π演算的进程代数模型，并对进程代数模型进行信息安全性质验证，因此能够基于自动化的模型转换方法，对形式化模型进行转换，转换后的模型可以通过验证工具直接进行验证，从而可以提高模型验证效率。并且，通过对形式化模型进行不同的转换，可以同时对形式化模型进行功能安全性质验证和信息安全性质验证，也就是说，可以同时对两种不同的安全性质进行验证，从而可以进一步提高模型验证效率。当然，实施本发明的任一产品或方法并不一定需要同时达到以上所述的所有优点。

本发明实施例的创新点包括：

1、基于自动化的模型转换方法，对形式化模型进行转换，转换后的模型可以通过验证工具直接进行验证，从而可以提高模型验证效率。并且，通过对形式化模型进行不同的转换，可以同时对形式化模型进行功能安全性质验证和信息安全性质验证，也就是说，可以同时对两种不同的安全性质进行验证，从而可以进一步提高模型验证效率。

2、通过模型检测工具Beagle，可以准确的对形式化模型进行功能安全性质验证，通过协议分析工具Proverif，可以准确的对形式化模型进行信息安全性质验证，从而可以提高模型验证的准确性。

附图说明

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

图1为本发明实施例提供的应用软件形式化模型验证方法的一种流程示意图；

图2示出了本发明实施例的功能安全性质验证过程示意图；

图3示出了本发明实施例的信息安全性质验证过程示意图；

图4为本发明实施例提供的应用软件形式化模型验证装置的一种结构示意图。

具体实施方式

下面将结合本发明实施例中的附图，对本发明实施例中的技术方案进行清楚、完整的描述。显然，所描述的实施例仅仅是本发明的一部分实施例，而不是全部的实施例。基于本发明中的实施例，本领域普通技术人员在没有付出创造性劳动前提下所获得的所有其他实施例，都属于本发明保护的范围。

需要说明的是，本发明实施例及附图中的术语“包括”和“具有”以及它们的任何变形，意图在于覆盖不排他的包含。例如包含的一系列步骤或单元的过程、方法、系统、产品或设备没有限定于已列出的步骤或单元，而是可选地还包括没有列出的步骤或单元，或可选地还包括对于这些过程、方法、产品或设备固有的其他步骤或单元。

本发明实施例公开了一种应用软件形式化模型验证方法及装置，能够提高模型验证的效率。下面对本发明实施例进行详细说明。

图1为本发明实施例提供的应用软件形式化模型验证方法的一种流程示意图。该方法应用于电子设备。该方法具体包括以下步骤。

S110：获取待验证的应用软件形式化模型。

例如，电子设备可以接收用户输入的应用软件形式化模型，作为待验证的应用软件形式化模型；或者，可以根据用户预先设定的存储位置，从该存储位置处获取应用软件形式化模型，作为待验证的应用软件形式化模型。

S120：基于自动化的模型转换工具Beagle Translator，将应用软件形式化模型中的各进程模型转换为对应的模块模型，将应用软件形式化模型中的功能安全性质转换为对应的待验证属性，得到扩展标签迁移模型，并对扩展标签迁移模型进行功能安全性质验证。

通常情况下，由于格式不匹配等原因，电子设备接收到的应用软件形式化模型不能通过模型检测工具直接进行验证。在本发明实施例中，为了提高模型验证的效率，电子设备可以对获取的待验证应用软件形式化模型进行转换，将其转换为与模型检测工具匹配的模型，从而可以通过模型检测工具直接进行验证。

在一种实现方式中，对应用软件形式化模型进行功能安全性质验证时，电子设备可以将应用软件形式化模型以及功能安全性质规约转换成为模型检测工具Beagle所接受的扩展标签迁移模型。之后再调用模型检测工具进行验证分析并返回验证结果。针对这个模型转换的过程，我们开发了自动化的模型转换工具Beagle Translator，也可以称为模型转换验证工具。

这个自动化的模型转换验证工具是将应用软件形式化模型，也可以称为系统模型，以及功能安全性质规约转换成为扩展标签迁移模型的自动化转换工具。上述功能安全性质规约指用形式化逻辑描述的属性，也可以称为功能安全属性。

图2示出了本发明实施例的功能安全性质验证过程示意图。如图2所示，将系统模型与安全性规约输入模型转换工具Beagle Translator后，扩展标签迁移模型的转换算法主要分成两个部分：第一部分是扩展标签迁移模型的模块部分的转换，第二部分是功能安全性质的转换部分。首先需要遍历系统模型的进程模型，对于每一个进程模型我们都会对应的转换到一个扩展标签迁移模型的模块。

具体的，针对每个进程模型，从进程模型到模块模型的转换有五个步骤。第一步是将进程模型的进程属性转换成为模块模型的变量声明。第二步是将进程模型中的通信信道转换成为模块模型的标签声明。第三步是将进程模型的有限状态自动机中的状态转换成为模块模型中的位置声明。第四步是从初始化信息转换得到模型模块的初始化迁移。最后一步是从进程模型的状态机模型的状态迁移转换得到模块模型中的状态迁移。这里分成两种状态迁移，分别是进程方法的状态迁移以及通信动作的状态迁移。

在完成了模块模型的转换之后，我们还需要将系统模型中的功能安全性质，也可以称为功能验证属性转换成为扩展标签迁移模型可以接受的待验证属性。具体的，可以将使用CTL(Linear-time Temporal Logic，时序逻辑)的不变式条件描述的功能安全性质AGf转换成为模型检测工具的待验证属性INVARSPEC f，得到扩展标签迁移模型BeagleModel。

在得到了应用软件形式化模型对应的扩展标签迁移模型之后我们可以调用模型检测工具Beagle进行安全分析，若验证结果为真则说明当前的系统模型满足功能安全条件，若验证结果为假则模型检测工具将会返回一条反例路径供使用者进行错误分析。

S130：基于自动化的模型转换验证工具Proverif Translator，对应用软件形式化模型进行模型预定义、初始化信息转换、状态机模型转换、以及信息安全性质转换，得到基于π演算的进程代数模型，并对进程代数模型进行信息安全性质验证。

对应用软件形式化模型进行信息安全性质验证时，电子设备可以将系统模型以及安全性规约转换成为协议分析工具所接受的进程代数模型。之后再调用Proverif工具进行验证分析并返回验证结果。针对这个模型转换的过程，我们开发了自动化的模型转换验证工具Proverif Translator。

图3示出了本发明实施例的信息安全性质验证过程示意图。如图3所示，将系统模型与安全性规约输入模型转换验证工具Proverif Translator后，这个自动化的模型转换验证工具Proverif Translator主要包含了四个部分的内容。第一部分是模型预定义，这一部分会将系统模型中的进程属性、进程方法以及通信信道转换成为对应的变量类型定义、进程方法声明以及通信信道声明部分。第二部分是将系统模型中的初始化信息转换成为对应的进程代数模型中的初始化进程。第三部分是将状态机模型转换成进程代数模型中的通信进程模型。最后一部分是信息安全性质的转换，将机密性安全属性以及认证性安全属性分别转换成为对应进程代数模型中的机密性以及认证性查询语句。

在得到了对应的基于π演算的进程代数模型Proverif Model之后，电子设备可以调用协议安全分析工具Proverif来进行安全分析，若验证结果为真则说明当前通信协议模型满足信息安全属性的机密性以及认证性，若验证结果为假则会返回一条反例路径供使用者进行错误分析。

具体的，上述第一部分的模型预定义部分中主要包括了三个步骤：第一个步骤是自定义类型声明，需要将系统模型中所有自定义的进程属性声明出来。第二步是进程方法的声明，在这一部分中需要根据系统模型中的进程方法中的构造方法以及析构方法转换成为对应的进程代数模型中的方法声明。第三步是通信信道的声明，需要根据系统模型中的通信信道及私有性在进程代数模型中声明通信信道。

在第二部分的初始化进程转换中，主要是将系统模型中的初始化信息转换成为进程代数模型中的初始化进程。在这一步骤中主要是将初始化信息中的进程属性在初始化进程中声明出来，并且作为对应的进程模型的输入参数生成初始化进程模板。

第三部分是进程模型转换的部分，这一部分需要将系统模型中的通信进程的状态机模型转换成为进程代数模型中的通信进程模型。针对系统模型中的每一个进程模型都将会转换得到一个对应的进程代数模型中的进程模型。首先我们需要在进程模型中声明所有在这个进程中用到的变量。其次我们将进程模型的状态机模型中的状态转换成为进程代数模型中的事件并声明。最后一步是将状态机模型中的状态迁移根据进程方法的状态迁移或是通信动作的状态迁移转换得到对应的进程代数模型中的语句。

第四部分是信息安全性质的转换。信息安全性质包括了两种安全性质，分别是：机密性以及认证性。这两种安全性质需要分别对应的转换成为进程代数模型中的机密性查询语句以及认证性查询语句，之后使用协议安全分析工具进行安全分析。

由上述内容可知，本实施例可以基于自动化的模型转换方法，对形式化模型进行转换，转换后的模型可以通过验证工具直接进行验证，从而可以提高模型验证效率。并且，通过对形式化模型进行不同的转换，可以同时对形式化模型进行功能安全性质验证和信息安全性质验证，也就是说，可以同时对两种不同的安全性质进行验证，从而可以进一步提高模型验证效率。

如图4所示，其示出了本发明实施例的一种应用软件形式化模型验证装置的结构示意图，所述装置包括：

模型获取模块410，用于获取待验证的应用软件形式化模型；

功能安全验证模块420，用于基于自动化的模型转换工具Beagle Translator，将所述应用软件形式化模型中的各进程模型转换为对应的模块模型，将所述应用软件形式化模型中的功能安全性质转换为对应的待验证属性，得到扩展标签迁移模型，并对所述扩展标签迁移模型进行功能安全性质验证；

信息安全验证模块430，用于基于自动化的模型转换验证工具ProverifTranslator，对所述应用软件形式化模型进行模型预定义、初始化信息转换、状态机模型转换、以及信息安全性质转换，得到基于π演算的进程代数模型，并对所述进程代数模型进行信息安全性质验证。

可选的，所述功能安全验证模块420包括：

模块转换子模块，用于基于自动化的模型转换工具Beagle Translator，针对所述应用软件形式化模型中的每个进程模型，将该进程模型的进程属性转换成为模块模型的变量声明，将该进程模型中的通信信道转换成为所述模块模型的标签声明，将该进程模型中的有限状态自动机中的状态转换成为所述模块模型中的位置声明，从该进程模型中的初始化信息转换得到所述模块模型的初始化迁移，从该进程模型的状态机模型的状态迁移转换得到所述模块模型中的状态迁移；所述状态迁移包括进程方法的状态迁移以及通信动作的状态迁移；

功能安全性质转换子模块，用于将使用时序逻辑CTL的不变式条件描述的功能安全性质AG f转换成为模型检测工具的待验证属性INVARSPEC f，得到扩展标签迁移模型。

可选的，所述功能安全验证模块420，具体用于将所述扩展标签迁移模型输入模型检测工具Beagle中，得到功能安全性质验证结果。

可选的，所述信息安全验证模块430包括：

预定义子模块，用于将所述应用软件形式化模型中的进程属性、进程方法以及通信信道转换成为对应的变量类型定义、进程方法声明以及通信信道声明；

初始化信息转换子模块，用于将所述应用软件形式化模型中的初始化信息转换成为对应的进程代数模型中的初始化进程；

状态机模型转换子模块，用于将所述应用软件形式化模型中的状态机模型转换成所述进程代数模型中的通信进程模型；

信息安全性质转换子模块，用于将所述应用软件形式化模型中的信息安全性质进行转换，得到基于π演算的所述进程代数模型。

可选的，所述预定义子模块，具体用于：将所述应用软件形式化模型中所有自定义的进程属性声明出来，根据所述应用软件形式化模型的进程方法中的构造方法以及析构方法转换成为对应的进程代数模型中的进程方法声明，根据所述应用软件形式化模型中的通信信道及私有性在进程代数模型中声明通信信道；

所述初始化信息转换子模块，具体用于：将所述应用软件形式化模型中的初始化信息中的进程属性在初始化进程中声明出来，并且作为对应的进程模型的输入参数生成初始化进程模板；

所述状态机模型转换子模块，具体用于：在所述应用软件形式化模型的进程模型中声明所有在这个进程中用到的变量，将进程模型的状态机模型中的状态转换成为进程代数模型中的事件并声明，将状态机模型中的状态迁移根据进程方法的状态迁移或通信动作的状态迁移转换得到所述进程代数模型中的语句；

所述信息安全性质转换子模块，具体用于：将信息安全性质中的机密性转换成为所述进程代数模型中的机密性查询语句，将信息安全性质中的认证性转换成为所述进程代数模型中的认证性查询语句。

可选的，所述信息安全验证模块430，具体用于将所述进程代数模型输入协议分析工具Proverif中，得到信息安全性质验证结果。

由上述内容可知，本发明实施例提供的应用软件形式化模型验证装置，能够基于自动化的模型转换方法，对形式化模型进行转换，转换后的模型可以通过验证工具直接进行验证，从而可以提高模型验证效率。并且，通过对形式化模型进行不同的转换，可以同时对形式化模型进行功能安全性质验证和信息安全性质验证，也就是说，可以同时对两种不同的安全性质进行验证，从而可以进一步提高模型验证效率。

上述装置实施例与方法实施例相对应，与该方法实施例具有同样的技术效果，具体说明参见方法实施例。装置实施例是基于方法实施例得到的，具体的说明可以参见方法实施例部分，此处不再赘述。

本领域普通技术人员可以理解：附图只是一个实施例的示意图，附图中的模块或流程并不一定是实施本发明所必须的。

本领域普通技术人员可以理解：实施例中的装置中的模块可以按照实施例描述分布于实施例的装置中，也可以进行相应变化位于不同于本实施例的一个或多个装置中。上述实施例的模块可以合并为一个模块，也可以进一步拆分成多个子模块。

最后应说明的是：以上实施例仅用以说明本发明的技术方案，而非对其限制；尽管参照前述实施例对本发明进行了详细的说明，本领域的普通技术人员应当理解：其依然可以对前述实施例所记载的技术方案进行修改，或者对其中部分技术特征进行等同替换；而这些修改或者替换，并不使相应技术方案的本质脱离本发明实施例技术方案的精神和范围。