一种面向软件行为和多视点的需求模型验证方法

Requirement Model Checking Approach Based on Multi-view and Software Behavior

软件需求分析是软件开发生命周期中最重要的步骤之一.模型驱动的需求分析方法将需求模型作为需求规格说明的补充,从一个或多个角度对非形式化的需求信息进行正确性验证以发现需求规格中的不一致和不完整性等.本文在一种新型的,基于软件行为和多视点的需求建模方法基础上,依据其构造特点,提出需求模型的分析以及验证方法.该方法主要通过构造模型待验证性质的行为时序逻辑规约,以需求模型对应的有穷状态迁移系统为基础,结合On-The-Fly的方法验证性质规约是否语义满足该状态迁移系统.此外,从命题抽象的角度对该验证方法进行优化.针对该方法实现了模型验证工具原型.

Software requirement is one of the most important steps in the whole software implementation life cycle.Model driven requirement analysis is to make requirement model as the complement of requirement specification.Requirement model plays the role that to discovery the incorrent and inconsiste facts in requirement specification.In this paper,w e proposed an requirement model checking approach based on a muliti view point requirement analysis methology.The main idea of this methology is to construct the properties in a behavior temporal logic style,and the finite state machine of the requirement model and check w hether the properties could satisfy the model.Besides,w e have also discussed about its optimizing manner in proposition abstraction w ay.We also have implemented model checking toolkit for further research.