南昌大学学报(工科版)
南昌大學學報(工科版)
남창대학학보(공과판)
JOURNAL OF NANCHANG UNIVERSITY ENGINEERING & TECHNOLOGY EDITION
2008年
2期
170-174
,共5页
安全协议%统一建模语言%模型检测%SPIN/Promela
安全協議%統一建模語言%模型檢測%SPIN/Promela
안전협의%통일건모어언%모형검측%SPIN/Promela
统一建模语言(UML)是设计和建模安全协议的常用方法,但UML缺少精确的语义,不能对协议模型作进一步分析和验证;Promela是一种具有精确语义的形式化语言,通过Promela规范给协议的UML模型赋予精确语义可以结合两者的优势,提出一种将安全协议UML模型转换成Promela规范的方法,定义了转换规则实现模型间的转换,实例表明该方法的可行性.
統一建模語言(UML)是設計和建模安全協議的常用方法,但UML缺少精確的語義,不能對協議模型作進一步分析和驗證;Promela是一種具有精確語義的形式化語言,通過Promela規範給協議的UML模型賦予精確語義可以結閤兩者的優勢,提齣一種將安全協議UML模型轉換成Promela規範的方法,定義瞭轉換規則實現模型間的轉換,實例錶明該方法的可行性.
통일건모어언(UML)시설계화건모안전협의적상용방법,단UML결소정학적어의,불능대협의모형작진일보분석화험증;Promela시일충구유정학어의적형식화어언,통과Promela규범급협의적UML모형부여정학어의가이결합량자적우세,제출일충장안전협의UML모형전환성Promela규범적방법,정의료전환규칙실현모형간적전환,실례표명해방법적가행성.