模型检测在软件需求分析及设计中的应用  

APPLICATION OF MODEL CHECKING IN SOFTWARE REQUIREMENTS ANALYSIS AND DESIGN

作　　者：贺亚博[1] 郝克刚[1] 葛玮[1] 

机构地区：[1]西北大学软件工程研究所,陕西西安710127

出　　处：《计算机应用与软件》2009年第4期128-130,共3页Computer Applications and Software

摘　　要：模型检测技术因其完全自动化并且验证速度快的优点在硬件及协议的验证中广泛应用,近年来在软件领域的应用研究也不断涌现。总结了模型检测在软件需求分析及设计中已有的应用技术,包括利用模型检测工具对RSML,SCR和UML图形的检测,以及直接的模型检测,并从不同角度对已有技术进行系统的分析和比较。最后对该项技术研究的方向进行展望。Model checking is used widely in hardware, protocol domain because of the virtue of automatism and high checking rate. Recent years, research of model checking in software domain is developing rapidly, too. We conclude the existed application technology about model checking in software requirements analysis and design,including model checking RSML, SCR, and UML diagrams with model checker, and model checking directly. We also analyze and compare existed technologies from two angles. Finally, we identify some issues which are still open to further research.

关 键 词：模型检测 模型检测工具 直接检测 

分 类 号：TP311.52[自动化与计算机技术—计算机软件与理论] TN915.04[自动化与计算机技术—计算机科学与技术]