摘要
为使自适应软件的需求规约与软件约束一致性验证能够得到已有验证工具的支持,提出了一种基于模型转换的验证方法。该方法通过对Tropos建模方法进行上下文和异常条件扩展来满足自适应软件需求,给出从Tropos需求模型到状态变迁模型的映射规则,并通过验证软件约束公式在状态变迁模型上的可满足性,达到验证软件需求与软件约束一致性的目的。最后,通过舰船火灾损管系统的实例说明了自适应软件需求的建模和验证过程。
-
单位软件工程国家重点实验室; 武汉大学; 中国人民解放军海军工程大学; 电子工程学院