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

摘要

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

主权项

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