| 基于场景的并发系统需求验证方法研究 |
| |
| 引用本文： | 张涛,黄少滨,黄宏涛,吕天阳,刘刚.基于场景的并发系统需求验证方法研究[J].哈尔滨工程大学学报,2011(10):1323-1328. |
| |
| 作者姓名： | 张涛 黄少滨 黄宏涛 吕天阳 刘刚 |
| |
| 作者单位： | 哈尔滨工程大学计算机科学与技术学院; |
| |
| 基金项目： | 国家自然科学基金资助项目(60873038,60903080); 国家科技支撑计划基金资助项目(2009BAH42B02); 哈尔滨工程大学中央高校基本科研业务专项基金资助项目(100603) |
| |
| 摘 要： | 为验证并发系统需求设计的正确性,提出一种基于场景的并发系统需求验证方法.首先,用UML顺序图建模并发系统需求场景,通过定义顺序图的操作语义及转换规则,将顺序图的XML描述文件自动转换为Promela程序,而后将描述系统需求的Promela程序和描述系统规约的线性时序逻辑作为模型检测器SPIN的输入,用模型检测的方法自动...
|
| 关 键 词： | 模型检测 需求验证 并发系统 UML顺序图 SPIN |
Scenario-based verification method of the requirements of concurrent systems |
| |
| ZHANG Tao,HUANG Shaobin,HUANG Hongtao,Lü Tianyang,LIU Gang.Scenario-based verification method of the requirements of concurrent systems[J].Journal of Harbin Engineering University,2011(10):1323-1328. |
| |
| Authors: | ZHANG Tao HUANG Shaobin HUANG Hongtao Lü Tianyang LIU Gang |
| |
| Affiliation: | ZHANG Tao,HUANG Shaobin,HUANG Hongtao,Lü Tianyang,LIU Gang (College of Computer Science and Technology,Harbin Engineering University,Harbin 150001,China) |
| |
| Abstract: | In order to verify the correctness of requirement design in concurrent systems,this paper proposed a scenario-based verification method of the requirements of concurrent systems.First,UML sequence diagrams were used to model the requirements scenes of the concurrent systems.By defining the operational semantics and transformation rules of UML,the XML file of sequence diagrams was automatically converted to the Promela program.Secondly,the Promela program,which describes the system requirements,and linear te... |
| |
| Keywords: | model checking requirements validation concurrent systems UML sequence diagrams SPIN |
| 本文献已被 CNKI 等数据库收录！ |
|
