哈尔滨工程大学学报2011，Vol.32Issue(10)：1323-1328,6.DOI:10.3969/j.issn.1006-7043.2011.10.011
基于场景的并发系统需求验证方法研究
Scenario-based verification method of the requirements of concurrent systems
摘要
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 temporal logic,which describes the specifications of a system,were used as the input of the SPIN model checker. Using the model checking method automatically validates the consistency and completeness of the requirement design of concurrent systems. Finally,to prove the validity of the above method,a scenario-based validation instance of requirement design of the ATM system was given. The results show that this method can effectively find the errors and inconsistencies in the requirement design of concurrent systems and help to improve the design.关键词
模型检测/需求验证/并发系统/UML顺序图/SPINKey words
model checking/requirements validation/concurrent systems/UML sequence diagrams/SPIN分类
信息技术与安全科学引用本文复制引用
张涛,黄少滨,黄宏涛,吕天阳,刘刚..基于场景的并发系统需求验证方法研究[J].哈尔滨工程大学学报,2011,32(10):1323-1328,6.基金项目
国家自然科学基金资助项目(60873038,60903080) （60873038,60903080）
国家科技支撑计划基金资助项目(2009BAH42 B02) （2009BAH42 B02）
哈尔滨工程大学中央高校基本科研业务专项基金资助项目(100603). （100603）
