文献类型：期刊文章

作　　者：张琛[1,2] 段振华[1,2] 田聪[1,2]

机构地区：[1]西安电子科技大学计算理论与技术研究所,陕西西安710071 [2]西安电子科技大学ISN国家重点实验室,陕西西安710071

出　　处：《软件学报》

基　　金：国家自然科学基金(60433010;60873018;60910004;91018010;61003078;61003079;61133001);国家重点基础研究发展计划(973)(2010CB328102);国家教育部博士点基金(200807010012);中央高校基本科研业务费专项资金(JY10000903004)

年　　份：2011

卷　　号：22

期　　号：11

起止页码：2625-2638

语　　种：中文

收录情况：AJ、BDHX、BDHX2008、CSA、CSA-PROQEUST、CSCD、CSCD2011_2012、EI(收录号：20114814570358)、IC、INSPEC、JST、MR、RCCSE、SCOPUS、ZGKJHX、ZMATH、核心刊

摘　　要：为了确保软件分析与设计阶段UML2.0序列图模型的可靠性,采用命题投影时序逻辑(propositional projection temporal logic,简称PPTL)模型检测方法对该模型进行分析和验证.提出了事件确定有限自动机(event deterministic finite automata,简称ETDFA),并使用该自动机为序列图建立形式化模型,通过给出的基于ETDFA的PPTL模型检测算法得到验证结果.该方法可以在基于Spin的PPTL模型检测器的支持下实现.实例结果表明,该方法可以验证序列图的性质并保证其可靠性.

关 键 词：UML2.0序列图  事件确定有限自动机  模型检测  命题投影时序逻辑 验证  

分 类 号：TP311]