CN106411635A - 一种实时协议的形式化分析及验证方法 - Google Patents

Abstract

本发明公开了一种实时协议的形式化分析及验证方法，包括：数学建模步骤，用于利用进程代数建模，对实时协议进行形式化表示，建立实时协议模型，并对协议需求进行形式化表示；代码生成步骤，根据所述实时协议模型生成高级语言代码；仿真验证步骤，根据进程代数描述语言的语义对所述实时协议模型进行仿真执行，并根据数学建模步骤所输出的实时协议的形式化表示和协议需求的形式化表示，对所述实时协议模型所满足的需求性质进行分析与验证；验证结果处理步骤，对仿真验证步骤所输出的分析与验证结果进行统计及分类，并提供协议性质的评估。该方法提供不满足协议需求的协议执行过程，并提供协议性质的整体评估，提高了开发人员优化协议的效率。

Description

一种实时协议的形式化分析及验证方法

技术领域

本发明涉及实时协议的形式化分析与验证领域，尤其涉及一种实时协议的形式化分析及验证方法。

背景技术

为了保证软硬件的安全性、可靠性，形式化分析与验证技术在一些关键领域逐渐被广泛应用。例如在过去，形式化方法已广泛应用于安全性、容错性、基本一致性、面向对象编程、编译正确性、协议开发、硬件检测、计算机辅助设计和人类安全。基于形式化方法发现的一些安全漏洞，避免了许多工程项目中的巨大损失。

随着实时协议在工业、民用、军用领域的广泛应用，协议的设计与实现也面临着安全性、实时性等多方面的挑战。为了保证协议的安全性、健壮性、协议符合性等特征，形式化分析与验证技术逐渐被应用于一些协议的验证。目前缺乏一种针对实时协议分析及验证的方法。

发明内容

本发明的目的是通过以下技术方案实现的。

一种实时协议的形式化分析及验证方法，包括：数学建模步骤，用于利用进程代数建模，对实时协议进行形式化表示，建立实时协议模型，并对协议需求进行形式化表示；代码生成步骤，根据所述实时协议模型生成高级语言代码；仿真验证步骤，根据进程代数描述语言的语义对所述实时协议模型进行仿真执行，并根据数学建模步骤所输出的实时协议的形式化表示和协议需求的形式化表示，对所述实时协议模型所满足的需求性质进行分析与验证；验证结果处理步骤，对仿真验证步骤所输出的分析与验证结果进行统计及分类，并提供协议性质的评估。

优选地，在数学建模步骤中，所述对实时协议进行形式化表示包括利用进程代数对协议描述的数学表达。

优选地，所述数学表达包括对协议运行过程、协议算法进行表达、对实时协议的实时性、确定性、并发性、周期性及高精度同步进行表达。

优选地，所述对协议需求进行形式化表示包括利用时态逻辑、计算树逻辑、霍尔逻辑、分离逻辑对实时协议的需求进行准确的形式化表示。

优选地，所述代码生成步骤包括根据实时协议模型语言的语义生成高级语言代码。

优选地，所述仿真验证步骤包括模型仿真器步骤，模型检查算法库步骤，及模型性质的验证步骤。

优选地，所述模型仿真器步骤支持实时协议模型的仿真执行。

优选地，所述模型检查算法库步骤包括检查不同类型模型所适用的算法，并且支持用户对所述模型检查算法库步骤中模型检查算法库的扩展。

优选地，所述模型性质的验证支持根据检查模型的类别对算法进行智能选择，并根据算法及性质对模型进行验证。

优选地，所述验证结果处理步骤包括对所述实时协议模型所满足的需求性质的分析与验证结果进行统计与分类，并为不可满足的协议需求提供相应的协议执行过程。

本发明所述方法基于进程代数对实时协议进行形式化建模，支持复杂的并发通信协议的准确表达，实现对实时协议中的时间特性的描述，有效刻画实时协议的实时性、并发性及周期性等特征；代码生成步骤便于开发人员在已验证模型的基础上开发协议；采用模型检查的方式，支持验证模型时模型检查算法的智能自动化选择，简化验证操作。

本发明的有益效果：

1.数学建模步骤支持使用多种逻辑对协议需求的刻画，支持多视角地展现协议行为特征；

2.模型检查算法库的自动化选择可以简化验证操作，而算法库的可扩展性允许用户定制相关协议的模型检查策略，对实时协议的验证更加具有针对性；

3.对验证结果的统计与分类，方便用户获得更加直观的实时协议测评结果。

该方法针对实时协议的特性及不同特征的模型，定制可靠的模型检查算法，给出实时协议的测评结果，便于用户根据结果对协议的设计与实现进行优化。

附图说明

图1是本发明实时协议的形式化分析及验证方法的流程图；

图2是实现本发明实时协议的形式化分析及验证方法的系统结构图。

具体实施方式

下面将参照附图更详细地描述本发明的示例性实施方式。虽然附图中显示了本发明的示例性实施方式，然而应当理解，可以以各种形式实现本公开而不应被这里阐述的实施方式所限制。相反，提供这些实施方式是为了能够更透彻地理解本公开，并且能够将本发明的范围完整的传达给本领域的技术人员。

如图1所示，一种实时协议的形式化分析及验证方法包括：数学建模步骤，利用进程代数对协议进行形式化表示，准确表达协议内容，并使用时态逻辑、计算树逻辑、霍尔逻辑、分离逻辑对实时协议需求进行刻画；代码生成步骤用于将协议模型转化为高级语言代码；仿真验证步骤，根据进程代数语义及相应的实时协议模型构建协议运行时的仿真，根据模型检查算法对协议需求进行分析与验证，获得协议验证的结果；验证结果处理步骤，对实时协议的性质验证结果进行处理和输出，所作的处理主要是根据性质的可满足性、可满足的概率等对结果进行统计和分类。

在所述实时协议的形式化分析及验证方法中，所述数学建模步骤，包括实时协议的建模和实时协议需求建模。该步骤使用进程代数对实时协议进行建模，并根据所使用的进程代数语言对模型进行语法语义的分析。进程代数是关于通信并发方法的代数理论的统称。进程代数提供了多个独立实体或者进程之间交互、通信以及同步的抽象描述，能够描述协议中的时序关系、时间性质、随机性质。同时，该理论提供了大量能对进程代数语言进行操作及分析的代数规则。进程代数语言可以用于验证进程之间的等价性，可以验证协议需求与协议模型之间的一致性。此外，该步骤使用时态逻辑、计算树逻辑、霍尔逻辑、分离逻辑对实时协议需求进行刻画，包括对协议中的实时性、无死锁性、无饥饿等待等性质进行准确描述，能表示大部分协议需求。

在所述实时协议的形式化分析及验证方法中，所述代码生成步骤能够根据建立的实时协议模型生成多种类型的高级语言代码。

在所述实时协议的形式化分析及验证方法中，所述仿真验证步骤，用于根据进程代数的语义进行协议运行的仿真。所述模型性质的验证主要依赖于模型检查技术。模型检查技术是针对并发方法的一种自动验证技术，方法用有限状态结构表示，被验证的性质可以采用多种逻辑进行描述，例如时态逻辑。验证过程是对涉及的状态空间进行搜索的过程，该过程确定被验证的性质在状态空间中的可达性或不可达性。所述模型检查算法库包括对所有类型的协议模型的验证算法，例如对概率模型、时间模型等分别有不同的模型检查算法。该步骤可以根据输入的协议模型类型，对模型检查算法进行智能选择，并在同类模型算法中选择验证效率较高的算法进行模型验证。

在所述实时协议的形式化分析及验证方法中，所述验证结果处理步骤，用于对协议需求的验证结果进行统计及分类，并向用户反馈处理后的验证结果。该步骤会根据协议性质的可满足性，可满足的概率，以及用户输入的性质优先级等进行统计、分类，并提供不可满足的协议需求的协议执行过程，有利于提高优化协议的效率。

如图2所示，一种基于进程代数的实时协议分析及验证系统包括：数学建模模块，利用进程代数对协议进行形式化表示，准确表达协议内容，并使用时态逻辑、计算树逻辑、霍尔逻辑、分离逻辑对实时协议需求进行刻画；代码生成模块用于将协议模型转化为高级语言代码；仿真验证模块，根据进程代数语义及相应的实时协议模型构建协议运行时的仿真，根据模型检查算法对协议需求进行分析与验证，获得协议验证的结果；验证结果处理模块，对实时协议的性质验证结果进行处理和输出，所作的处理主要是根据性质的可满足性、可满足的概率等对结果进行统计和分类。

在所述基于进程代数的实时协议分析及验证系统中，所述数学建模模块，包括实时协议的建模和实时协议需求建模。该模块使用进程代数对实时协议进行建模，并根据所使用的进程代数语言对模型进行语法语义的分析。进程代数是关于通信并发系统的代数理论的统称。进程代数提供了多个独立实体或者进程之间交互、通信以及同步的抽象描述，能够描述协议中的时序关系、时间性质、随机性质。同时，该理论提供了大量能对进程代数语言进行操作及分析的代数规则。进程代数语言可以用于验证进程之间的等价性，可以验证协议需求与协议模型之间的一致性。此外，该模块使用时态逻辑、计算树逻辑、霍尔逻辑、分离逻辑对实时协议需求进行刻画，包括对协议中的实时性、无死锁性、无饥饿等待等性质进行准确描述，能表示大部分协议需求。

在所述基于进程代数的实时协议分析及验证系统中，所述代码生成模块能够根据建立的实时协议模型生成多种类型的高级语言代码。

在所述基于进程代数的实时协议分析及验证系统中，所述仿真验证模块，用于根据进程代数的语义进行协议运行的仿真。所述模型性质的验证主要依赖于模型检查技术。模型检查技术是针对并发系统的一种自动验证技术，系统用有限状态结构表示，被验证的性质可以采用多种逻辑进行描述，例如时态逻辑。验证过程是对涉及的状态空间进行搜索的过程，该过程确定被验证的性质在状态空间中的可达性或不可达性。所述模型检查算法库包括对所有类型的协议模型的验证算法，例如对概率模型、时间模型等分别有不同的模型检查算法。该模块可以根据输入的协议模型类型，对模型检查算法进行智能选择，并在同类模型算法中选择验证效率较高的算法进行模型验证。

在所述基于进程代数的实时协议分析及验证系统中，所述验证结果处理模块，用于对协议需求的验证结果进行统计及分类，并向用户反馈处理后的验证结果。该模块会根据协议性质的可满足性，可满足的概率，以及用户输入的性质优先级等进行统计、分类，并提供不可满足的协议需求的协议执行过程，有利于提高优化协议的效率。

在优选实施例中，应用本发明实时协议的形式化分析及验证方法对Powerlink协议进行分析和验证。

开源实时通信技术Powerlink是一项在标准以太网介质上，用于解决工业控制及数据采集领域数据传输实时性的实时以太网协议。该协议主要规定了数据链路层上的通信。该协议支持周期通信和非周期通信，其中一个协议循环周期主要包括等时同步阶段和异步通信阶段，周期通信发生在等时同步阶段，而非周期通信发生在异步通信阶段。

Powerlink中包含两类通信节点，主站节点和从站节点。并且根据从站在等时同步阶段中与主站节点不同的通信机制，从站又划分为了三类节点，Normal节点，PRC节点及复用节点。此外，在该协议中存在五类帧信息。异步过程中存在对帧消息发送请求的调度。

在应用本发明实时协议的形式化分析及验证方法对Powerlink协议进行分析和验证的过程中：

首先，需要获得协议执行的规范以及协议需要满足的一些性质，便于之后对该协议的建模。在该协议中所需要满足的性质有无死锁性、无任务的“饥饿”等待、实时性等。

然后，使用本发明所述方法的数学建模步骤对该协议进行建模。对协议进行建模时，可以为每一类节点赋予一个进程模型，并用进程代数描述语言对这些进程模型之间的通信进行描述。通过初始化异步帧消息的调度请求，以及对协议中的调度算法的建模，完成协议周期中，调度帧信息的模拟。整个协议模型由这些不同类型节点的进程的并发组成。对协议需求进行建模，通过时态逻辑、计算树逻辑等描述协议的无死锁性、无任务的“饥饿”等待、实时性等特征。

建模完成后，用户可以通过代码生成步骤生成相应的高级语言代码。

本发明所述方法的仿真验证步骤支持对模型进行仿真，仿真过程可以呈现所有模型可能执行的路径及状态空间。每个状态可以提供对该状态下所有变量的当前值的提示，状态之间的迁移提示用户协议运行过程中发生的动作。用户可以通过对不同进程的仿真进行建模代码的调试分析。如果发生死锁，在仿真结果中也能非常直观地观察到发生死锁的位置及发生死锁的原因。

仿真验证步骤中一个重要的功能是，根据协议模型和协议需求的形式化表示，对协议所满足的性质进行验证。该步骤会默认选择适合该模型的模型检查算法进行验证。同时，用户也可以扩充模型检查算法库和自定义使用的模型检查算法。

最后，验证结果输出到验证结果处理步骤进行处理，针对Powerlink协议，可以验证该协议中是否存在死锁，是否会有调度请求一直得不到调度，以及调度请求的顺序是否满足优先级设定等。

以上所述，仅为本发明较佳的具体实施方式，但本发明的保护范围并不局限于此，任何熟悉本技术领域的技术人员在本发明揭露的技术范围内，可轻易想到的变化或替换，都应涵盖在本发明的保护范围之内。因此，本发明的保护范围应所述以权利要求的保护范围为准。

Claims (10)

1.一种实时协议的形式化分析及验证方法，其特征在于，包括：

数学建模步骤，用于利用进程代数建模，对实时协议进行形式化表示，建立实时协议模型，并对协议需求进行形式化表示；

代码生成步骤，根据所述实时协议模型生成高级语言代码；

仿真验证步骤，根据进程代数描述语言的语义对所述实时协议模型进行仿真执行，并根据数学建模步骤所输出的实时协议的形式化表示和协议需求的形式化表示，对所述实时协议模型所满足的需求性质进行分析与验证；

验证结果处理步骤，对仿真验证步骤所输出的分析与验证结果进行统计及分类，并提供协议性质的评估。

2.如权利要求1所述的实时协议的形式化分析及验证方法，其特征在于，数学建模步骤中，所述的对实时协议进行形式化表示包括利用进程代数对协议描述的数学表达。

3.如权利要求2所述的实时协议的形式化分析及验证方法，其特征在于，所述数学表达包括对协议运行过程、协议算法进行表达、对实时协议的实时性、确定性、并发性、周期性及高精度同步进行表达。

4.如权利要求1所述的实时协议的形式化分析及验证方法，其特征在于，所述对协议需求进行形式化表示包括利用时态逻辑、计算树逻辑、霍尔逻辑、分离逻辑对实时协议的需求进行准确的形式化表示。

5.如权利要求1所述的实时协议的形式化分析及验证方法，其特征在于，所述代码生成步骤包括根据实时协议模型语言的语义生成高级语言代码。

6.如权利要求1所述的实时协议的形式化分析及验证方法，其特征在于，所述仿真验证步骤包括模型仿真器步骤，模型检查算法库步骤，及模型性质的验证步骤。

7.如权利要求6所述的实时协议的形式化分析及验证方法，其特征在于，所述模型仿真器步骤支持实时协议模型的仿真执行。

8.如权利要求6所述的实时协议的形式化分析及验证方法，其特征在于，所述模型检查算法库步骤包括检查不同类型模型所适用的算法，并且支持用户对所述模型检查算法库步骤中模型检查算法库的扩展。

9.如权利要求6所述的实时协议的形式化分析及验证方法，其特征在于，所述模型性质的验证支持根据检查模型的类别对算法进行智能选择，并根据算法及性质对模型进行验证。

10.如权利要求1所述的实时协议的形式化分析及验证方法，其特征在于，所述验证结果处理步骤包括对所述实时协议模型所满足的需求性质的分析与验证结果进行统计与分类，并为不可满足的协议需求提供相应的协议执行过程。