安全协议可视化建模和验证方法的分析与设计

作者：付杰; 闫振林; 张玉民; 息明东; 李升

来源：佳木斯大学学报(自然科学版), 2013, (05): 737-739+742.

• 安全协议
• 形式化分析
• 模型检测
• 可视化模型
• SPIN security protocol
• formal analysis
• model checking
• visualization model
• SPIN

统一建模语言(UML)是用于软件分析与设计的可视化建模语言,由于其缺乏精确的语义描述,因而进一步分析和验证比较困难.而形式化分析方法具有精确的数学语义和自动化验证工具的支持,可以对软件规范进行严格的分析和验证.本文提出了一种将安全协议的可视化模型转换成PROMELA规范的方法,使用SPIN工具对安全协议UML可视化模型进行了分析验证.

• 出版日期2013
• 单位佳木斯大学