一种适用于软件生命周期系统模型的需求获取方法研究

龚洁静 ，张广泉 ，肖刚

0 引言

需求工程出现于上个世纪80年代中期，目前已发展成为软件工程的一个独立研究分支。需求获取技术是需求工程中一个非常重要的研究内容。如何用适当的方法，把软件需求详细精确地描述出来，这不仅影响着开发人员之间，对软件系统的理解和的交流，更影响到最终软件产品的成败，尤其是在安全悠关系统的开发中。

目前主流的软件需求描述方法有两类：自然语言描述和半形式化描述，自然语言描述是目前工程实践中使用的主要方法，半形式化描述以UML/OCL为代表。自然语言存在着二义性和不一致性等缺陷，而UML/OCL的建模元素，同样缺乏精确的形式化语义，也不可避免地产生多义性，尽管辅之以OCL可以在一定程度上减少歧义性，但仍不能从根本上解决UML需求模型歧义性的问题。以这两类方法为基础的软件需求描述和构造过程，往往潜藏着大量的错误和缺陷，错误在一定程度上可以依靠测试来解决，软件需求中的缺陷，测试是无能为力的。形式化方法作为一种以数学为基础的方法，能够清晰、精确、抽象、简明地描述和验证软件系统及其性质，能够发现软件需求中的缺陷，极大地提高软件的安全性和可靠性，但在需求获取过程中，尚无形式化方法成功应用的案例。

1 公平离散系统模型

在需求构建过程中，离散系统模型是对问题系统的抽象，在实现过程中，离散系统模型是对程序的抽象（它的语义等价于转移系统模型），离散系统应能很好的描述系统或程序的性质，通过前面的讨论知道，离散系统模型应能描述系统和程序的安全性和活性。对于并发系统、反应系统和分布系统，离散系统模型还应能准确地描述系统事件被选中执行的方式，即离散系统模型应能准确地描述系统事件之间的公平性。

通过前面的描述，可以对基本离散系统模型作如下扩充，作为软件开发过程中使用的统一框架模型，公平离散系统模型包含如下几个组成部分：状态变量的集合、状态变量定义域和常量的集合、状态之间的转移的集合、初始化条件的集合、公平约束的集合。用符号 FDSM（U，V，INIT，T,MP,WF,SF）,下面就说明一下这几个符号的意义（约定本文用FDSM表示公平离散系统模型）

U＝{u1,u2,．．．．．un}模型内一组有穷的状态变量的集合，针对有限状态系统，所有的状态变量定义域是有限的。无穷状态系统状态变量的取值范围是无限的。本文仅讨论有穷状态系统，状态变量的类型，一定要和其定义域中的元素的类型一致。假设在一个状态s上给状态变量u赋值的形式是s[u] 。用U代表整个系统的状态空间。

V＝{v1,v2,……vn}是状态变量定义域及常量的集合，表示整个状态变量的取值范围和在这模型中所必需的常量。

INIT是模型的初始条件的集合，这些条件定义出所有FDSM 的初始状态，如果一个状态满足条件 INIT，那么就称其为初始状态。

T―模型中事件的集合，如果一个事件t∈T,那么一定有ρt⊆V×V，ρt表示从一个状态到另一个状态之间的转移。

MP＝{m1,m2,……,mn}是 MP公平的集合,其中 mi∈T,直观的解释如果 m⊆MP,在一定的状态下 m中的事件的卫条件为真，那么一定有部分的事件发生，且转移到下一个状态。

WF＝{w1,w2,……,wn}是弱公平的集合，其中wi∈T，直观的解释如下：如果在模型的一个无穷计算序列中wi的卫条件一直为真，那么在这个计算序列中wi一定能被无限多次选中运行。

SF＝{s1,s2,……,sn}是弱公平的集合，其中 si∈T,直观的解释如下：如果模型中的无穷计算序列中 si的卫条件无穷多次为真，那么在这个计算序列中 si一定能被无限多次的选中运行。

一个公平离散系统模型所有的计算序列必需满足以下几个条件：

(1) 初始化 s0是初始状态，那么 s0一定是满足条件INIT的状态之一。

(2) 连续性

公平离散系统模型中事件的发生是非确定，事件发生方式受到公平性的约束，在一个状态下可能多个事件的卫条件均为真，最终是那一个事件发生是不确定。当所有事件的卫条件均为真时，不能确定那些事件真实的执行。公平离散系统模型的可终止性不是必需的。事实上用这个模型研究的系统大多数都是不终止的，比如锅炉控制系统、核电厂控制系统。

2 需求获取过程中复杂性控制方法

利用公平离散系统模型构建系统需求模型是一个步进的过程，在构建系统的需求时，首先开始构建一个最简单的系统模型，这个模型只具备一些大粒度的事件，验证最初的模型。验证完成之后，在个模型的基础上，进一步考察系统对获得的需求，在验证中扩充。这个过程和从规约到程序的过程有点类似，仿造从规约到程序演化过程的概念，把这过程也称之为求精。求精之后的需求更接近实际系统，需求求精过程和规约的演化过程有本质的区别，在规约到程序的演化过程中，涉及到数据类型和语言概念上的变化，而在需求的获取过程中数据类型是一致的，且不存在语言概念上的变化，在需求求精过程中使用的语言是完全相同。更直观的讲，需求的求精过程有点类似于观察一个事物，当距离较远时，看到的系统的特征较大，能看见的系统的行为很少，当距离近一些时，看到的特征粒度就会小些，能看见的系统行为就比之前多些，这样逐步拉近和观察事物的距离，看到的细节就越来越多，直到最终获取所观察事物的所有细节，在这个观察的过程中，使用方法和借助的工具均是相同的。

在需求的求精过程中，随着观察系统的细节越来越多，获得的系统需求模型在空间量和时序量上均有扩张，空间量上的扩张表现为系统状态的增多，因为求精后更接近实际系统，故求精后的系统的需求模型的状态肯定多于求精前。随着状态的增加，状态之间的事件亦随之增多，许多事件在抽象模型中是看不见的，因为新事件在抽象模型中不存在，故新事件不能修改从抽象模型中继承的状态变量，新事件可以引用原有变量，但仅能修改新引入的状态变量。需求的求精就是在更细粒度的空间和时序下观察系统，时序量的扩张表现在随着系统状态增多和事件的增多。需求求精过程和从规约到程序的求精过程一样，包含：操作求精和数据求精，不过这两类求精的表现完全不同。数据求精在后者中设计的数据类型和数据表述方式的变化，可能与求精前后使用的数据类型和数据的表述方式完全不同，而数据求精在前者中，只是增加或减少变量来表述系统的行为，两者的语言相同类型相同，可能在特定场合中也有数据类型的变化，但求精前后表述的语句的语法方式是完全相同的。操作求精在两者中也有区别，在后者中求精越来越接近程序设计语言，从最初的抽象规约到程序两者的描述体系与语法完全不同，而需求求精只是在操作中增加更多的描述细节，而不改变原有变量的类型和值及数据表述方式，最初的需求模型和最终的需求模型，在描述体系和语法上完全相同。

需求求精和从规约到程序的演化过程相同，为了保证求精前后的一致性和完备性，在需求求精过程中，也必需对求精前后的需求模型进行验证。需求模型求精过程中首先要验证的是：一是求精过程中需要保持的性质，二是新增事件有关性质的验证。在第一点关于求精前后的需求模型需要验证：

(1) 抽象模型中的状态在具体需求模型中均可找到其对应的状态，当然在具体模型中可能有多个具体状态对应与抽象模型中的状态。

(2) 抽象模型和具体模型具有相同的死锁性和可终止性。

(3) 抽象模型和具体模型公平的一致性。

(4) 外部事件的不变性。

第二点中必需验证如下几方面：

(1) 新增事件安全性的验证。这包括新引入事件的可行性、操作不变性、无死锁性等等。

(2) 新增事件公平下活性的验证，这包括无活锁、可终止性。

通过这两方面的验证，基本上可以保证需求模型求精的正确性和一致性。

在获取需求模型的过程中，随着求精步骤的增加，模型中事件和状态变量会大量的增加，当到达一定数量时，模型的控制就变得非常的困难，继续利用原模型求精会变得极为复杂和难以处理，这时为了降低模型的复杂度，使模型在求精过程中容易控制，可以借用结构化的分解原理多模型进行分解，把复杂的模型分解成几个较为容易控制的小模型，分解的原则是模块化，高内聚和低耦合（在后面的章节会给出具体的分解算法），模型分解后各个子模型相互之间没有依赖关系，可以单独的求精验证。在分解的过程中应验证相关的性质，应特别注意特定公平下活性的验证。分解得到的子模型应是可复原的，可以通过组合这几个子模型构造出的复合模型应和原模型一致。

3 需求模型复用

在程序的开发方法尤其是面向对象的开发方法中，复用在整个方法学中占有很重要的地位，同样在基于公平离散系统框架下，构造系统需求模型的方法中，也引入复用的概念。在这个方法中，复用第一种情况是可以从别的系统需求模型中，引用与本系统需求有关的需求模型，甚至是整个系统的需求模型。第二种情况是，可以把一些公用的系统或子系统的需求模型模板化，把与业务逻辑无关的数据从需求模型中分离出去。在需要用到时只须给模板赋以具体的参数，就可实例化出不同业务系统的需求模型。因为模板模型在构造时已经对其进行了推理验证，引用到具体的需求中时就不需对其进行验证，因此引用模板和引用其他需求模型中，已证明的模型可以大量节约构建系统需求模型的时间。

4 小结

本文在回顾相关概念后，提出了可以适用于软件生命周期所有阶段的模型－公平离散系统模型，并给出了初步的形式化的定义，非形式化地描述了公平离散系统模型，在需求获取过程中的相关性质的验证及控制模型复杂性的方法、需求复用。

[1] Manna Z, Pnueli A. The Temporal Logic of Reactive and Concurent Systems Specification [M] . Springer-Verlag New York, INC. 1992.

[2] Manna Z, Pnueli A. Temporal Verification of Reactive Systems [M] . Springer-Verlag New York, INC. 1995.

[3] Back R J R, Xu Q W. Fairness in Action Systems[R] .Technical Report No159,Abo Akademi,Finland,1995.

[4] Back R J R, Xu Q W. Refinement of fair action systems[J] . Acta Informatica ,1998,35:131-165.

[5] Lamport L. The Temporal Logic of Actions [J] . ACM Transactions on Programming Languages and Systems,1994, 16(3):872-923.

[6] L amport L. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers [M] .Addison-Wesley, 2003.

[7] J.M. Spivey. The Z Notation: A Reference Manual Second Edition [M] . Prentice Hall International (UK) Ltd,1992.