| 基于事件确定有限自动机的UML2.0 序列图描述与验证 |
| |
| 引用本文： | 张琛,段振华,田聪.基于事件确定有限自动机的UML2.0 序列图描述与验证[J].软件学报,2011,22(11):2625-2638. |
| |
| 作者姓名： | 张琛 段振华 田聪 |
| |
| 作者单位： | 西安电子科技大学计算理论与技术研究所,陕西西安710071;西安电子科技大学ISN国家重点实验室,陕西西安710071 |
| |
| 基金项目： | 国家自然科学基金(60433010,60873018,60910004,91018010,61003078,61003079,61133001); 国家重点基础研究发展计划(973)(2010CB328102); 国家教育部博士点基金(200807010012); 中央高校基本科研业务费专项资金(JY10000903004) |
| |
| 摘 要： | 为了确保软件分析与设计阶段UML2.0序列图模型的可靠性,采用命题投影时序逻辑(propositional projection temporal logic,简称PPTL)模型检测方法对该模型进行分析和验证.提出了事件确定有限自动机(event deterministic finite automata,简称ETDFA),并使用该自动机为序列图建立形式化模型,通过给出的基于ETDFA的PPTL模型检测算法得到验证结果.该方法可以在基于Spin的PPTL模型检测器的支持下实现.实例结果表明,该方法可以验证序列图的性质并保证其可靠性.
|
| 关 键 词： | UML2.0序列图 事件确定有限自动机 模型检测 命题投影时序逻辑 验证 |
| 收稿时间： | 2010/10/23 0:00:00 |
| 修稿时间： | 2010/12/9 0:00:00 |
Specification and Verification of UML2.0 Sequence Diagrams Based on Event Deterministic Finite Automata |
| |
| ZHANG Chen,DUAN Zhen-Hua and TIAN Cong.Specification and Verification of UML2.0 Sequence Diagrams Based on Event Deterministic Finite Automata[J].Journal of Software,2011,22(11):2625-2638. |
| |
| Authors: | ZHANG Chen DUAN Zhen-Hua and TIAN Cong |
| |
| Affiliation: | ZHANG Chen1,2,DUAN Zhen-Hua1,TIAN Cong1,2 1(Institute of Computing Theory and Technology,Xidian University,Xi'an 710071,China) 2(State Key Laboratory of Integrated Service Networks,China) |
| |
| Abstract: | To ensure the reliability of UML2.0 sequence diagrams(SD),which are used in software analysis and design,propositional projection temporal logic(PPTL) model checking is adopted in this paper.First,event deterministic finite automata(ETDFA) are proposed and used to describe the formal models of SD.Furthermore,an algorithm for model checking ETDFA with PPTL formulas being the properties is presented.Finally,based on the implementation of PPTL model checker,the ETDFA models of SD are verified.Experimental resu... |
| |
| Keywords: | UML2 0 sequence diagram event deterministic finite automata model checking propositional projection temporal logic verification |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|
