自适应软件需求的形式化建模与验证  

Formal modeling and verification of self-adaptive software requirement

作　　者：雷义伟[1] 贲可荣 何智勇[1,2] 

机构地区：[1]海军工程大学电子工程学院,武汉430033 [2]武汉大学软件工程国家重点实验室,武汉430072

出　　处：《海军工程大学学报》2015年第6期73-78,共6页Journal of Naval University of Engineering

基　　金：国家部委基金资助项目(513150402);软件工程国家重点实验室基金资助项目(SKLSE 2012-09-38)

摘　　要：为使自适应软件的需求规约与软件约束一致性验证能够得到已有验证工具的支持,提出了一种基于模型转换的验证方法。该方法通过对Tropos建模方法进行上下文和异常条件扩展来满足自适应软件需求,给出从Tropos需求模型到状态变迁模型的映射规则,并通过验证软件约束公式在状态变迁模型上的可满足性,达到验证软件需求与软件约束一致性的目的。最后,通过舰船火灾损管系统的实例说明了自适应软件需求的建模和验证过程。In order to make the process of consistency verification of requirement specifications with software constraints supported by existing formal analysis tools, a verification method based on the model transformation is presented. The Tropos is extended with context and exception conditions to model the adaptive software requirements by this method. Transforming rule from Tropos require- ment model to state transition model is presented and the consistency of the requirement specifications with constrains are verified through formula satisfiability verifications on the state/transition model. An application example of the ship fire damage control system is used to illustrate the process of adap- tive software requirement modeling and verification.

关 键 词：自适应软件 需求分析 可满足性验证 

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]