安全协议UML模型的SPIN分析
肖美华; 刘俏威; 朱宜炳
南昌大学信息工程学院； 南昌大学信息工程学院 江西南昌330031； 江西南昌330031；
XIAO Mei-hua,LIU Qiao-wei,ZHU Yi-bing(School of Information Engineering,Nanchang University,Nanchang 330031,China)
摘要 统一建模语言(UML)是设计和建模安全协议的常用方法,但UML缺少精确的语义,不能对协议模型作进一步分析和验证;Promela是一种具有精确语义的形式化语言,通过Promela规范给协议的UML模型赋予精确语义可以结合两者的优势,提出一种将安全协议UML模型转换成Promela规范的方法,定义了
关键词 ：
模型检测 ,
安全协议 ,
SPIN/Promela ,
统一建模语言
Abstract ：Unified Modeling Language(UML) is a commonly used method in designing and modeling security protocol.But it’s lack of precise semantics,which leads to the weakness in analyzing and validating UML models.Promela is a formal language with precise semantics
Key words ：
unified modeling language
security protocol
model checking
SPIN/Promela；
出版日期: 2008-06-28
[1]
江顺亮; 王小惠; 章文捷. 流体动力学的SPH模型面向对象设计及其实施
[2]
肖美华; 尹传文; 舒良春; 胡波; 邹芳红. 基于JPF的Java程序验证
[3]
肖美华; 熊昊. 模型检测中反例最小化分析
[4]
刘葵. 一种新的面向事实的快速建模方法
[5]
徐鹏飞; 陶俊才; 涂荣军. 基于UML的业务分析
2008, Vol. 30 