文献类型：期刊文章

作　　者：梁盟磊[1] 王小平[1] 薛小平[2] 李刚[2]

机构地区：[1]同济大学电子与信息工程学院计算机科学与技术系,上海200092 [2]同济大学电子与信息工程学院信息与通信工程系,上海200092

出　　处：《计算机工程》

基　　金：国家自然科学基金资助项目(60972036)

年　　份：2011

卷　　号：37

期　　号：2

起止页码：72-74

语　　种：中文

收录情况：AJ、BDHX、BDHX2008、CAS、CSA、CSA-PROQEUST、CSCD、CSCD2011_2012、IC、INSPEC、JST、RCCSE、SCOPUS、UPD、ZGKJHX、核心刊

摘　　要：统一建模语言(UML)不能直接对所建立模型的正确性进行形式化验证。为解决上述问题,从UML模型的静态结构和动态行为2个方面分别提出结合行为时序逻辑(TLA)的模型形式化方法,在此基础上提出将UML模型转化为TLA+的形式化描述方法,并用TLC工具形式化检测TLA+描述的正确性。通过实例分析证明了该方法的有效性。

关 键 词：形式化方法 形式化验证 统一建模语言 行为时序逻辑

分 类 号：TP391]