面向软件行为的需求模型及特性检测

摘要

Requirements model and its verification are important procedures in software requirements.In this paper, the existing methods on requirements model are discussed and the related works of software behavior are concerned; furthermore, why utilizing software behavior in requirements model is illuminated. So a software behavior oriented requirements model is proposed formally which is named behavior description language (BDL). Its syntax and semantics of the model are given subsequently, and the hierarchy of behavior-oriented requirements model is presented based on BDL.In order to compare BDL with the current results and make full use of the latter related tools, the transformational relation is considered between BDL and CCS (calculus of communication system)which is an algebra process developed by Milner Robin. A transformation function which maps BDL into CCS is constructed and denoted by M [｜-｜]. For the sake of verifying properties of behavior-oriented requirements model, consistency of system, safety of system, behavioral trust and behavioral non-termination are depicted by μ-calculus, which is used to describe properties of labeled transition systems and for verifying these properties. At the end, an example described by BDL is analyzed and the specified properties are verified through CWB (Concurrency WorkBench) which is a model checking tool of CCS.%软件需求模型及其检测是软件需求工程中的重要工作.在分析现有需求建模方法和软件行为相关研究的基础上,对将软件行为概念引入需求模型进行了详细的阐述,提出一个面向软件行为的需求模型描述语言BDL(behavior description language),定义了它的语法、语义;讨论了CCS(calculus of communication system)与BDL的转换关系,构造了BDL到CCS的转换函数M[I-I];给出了需求模型的系统一致性、系统安全性、行为可信性及行为非终止性等4种系统特性的时序逻辑描述;最后用模型验证工具CWB(Concurrency WorkBench)对BDL描述的具体实例进行验证分析.