为在需求分析阶段验证软件是否满足非功能质量要求,提出一种基于场景行为的需求建模及质量特性检测方案。该方案定义能够建立高精度、可推理、易理解的需求行为模型的行为描述语言BDL,构造需求行为模型到状态迁移模型CCS的模型转换函数,以互模拟的定义为前提,验证转换函数的正确性,进而开发可信建模检测工具MTS。该工具导出的行为模型能够与质量特性表达式一起导入特性检测工具CWB实现质量检测。最后,使用该工具对手机软件升级这一需求进行行为建模,成功验证手机软件的一致性、安全性、行为可信性及行为非终止性。
To verify whether the software meets the non functional requirements in the requirements analysis phase,this paper proposed the solution of requirement formal modeling and quality characteristics detection based on scene behavior. First,it defined behavior description language( BDL) to establish the demand behavior model which was accurate,reasoning and easy to understand. Second,it constructed the model transfer function from a demand behavior model to state transfer model called calculus of communication system( CCS). Third,it proved the correctness of model transformations with the concept of strong bi-simulation. Then,it developed a trusted requirement modeling tool( MTS) to create behavior model which could be imported into concurrency workbench( CWB) with quality characteristics expressions together to achieve quality verification. Finally,it used this tool to establish behavior model according to mobile phone software upgrade scenario,and verify consistency,security,credibility and non-termination of mobile software successfully.