为使自适应软件的需求规约与软件约束一致性验证能够得到已有验证工具的支持 ,提出了一种基于模型转换的验证方法.该方法通过对T ropos建模方法进行上下文和异常条件扩展来满足自适应软件需求 ,给出从T ropos需求模型到状态变迁模型的映射规则 ,并通过验证软件约束公式在状态变迁模型上的可满足性 ,达到验证软件需求与软件约束一致性的目的.最后 ,通过舰船火灾损管系统的实例说明了自适应软件需求的建模和验证过程.%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 .
展开▼
