基于模型检验的需求不一致研究

郭 兆，魏长江

(青岛大学 数据科学与软件工程学院，山东 青岛 266071)

0 引 言

随着计算机软件自身规模的不断增大和业务逻辑变得复杂，软件需求在整个软件开发中变得越来越重要。在软件需求中，由于涉众复杂，使用目前的一些建模与需求分析方法，还是不可避免带来不一致性、不确定性等问题。其中，不一致的需求，会导致软件系统的混乱，甚至是错误。因此，在需求分析阶段，保证需求的一致性至关重要。

目前，解决需求一致性的方法主要分几类：采用经典逻辑检测逻辑表达式的值来发现需求的不一致性[1]；采用模型检验的方法检测需求规格说明中的错误；采用KAOS(knowledge acquisition in automated specification)方法通过建立具有自身语义的元模型发现矛盾。张建等[2]将UML(unified modeling language)模型集合转化为时间自动机网络模型并使用模型检验方法进行验证；周宇等[3]将层次自动机转换为系统并发时间自动机使用模型检验方法进行验证，但是未能提供需求不一致的定位策略；李思杰等[4]结合SCR(soft cost reduction)方法和模型检验的方法进行安全性和一致性验证，但是过于形式化，不能保证其它参与者的理解。

为了获得清晰且无二义性的软件需求，又能保证用户的理解，本文在现有研究基础上提出一种基于自然语言描述与模型检验相结合的方法。该方法利用自然语言蕴含语义关系进行提取并转换成自动机模型，然后根据对应关系转换成相应的形式模型并利用模型检验的工具和方法进行一致性验证。

1 研究框架

本文针对于需求分析中需求不一致的问题，提出了一种基于自然语言和模型检验相结合的需求描述分析方法。通过提取自然语言中的关键词，建立自动机模型，利用模型间的关联性将模型进行转换，将转换后的模型和性质规约引入模型检验中，通过模型检验发现不一致的需求。本文的研究框架图如图1所示,主要包含3部分内容。

图1 基于模型检验的需求不一致的研究框架

建模准备阶段：自然语言描述的需求有较强的表达能力，将自然语言描述的需求使用相似度算法计算出具有相似性的需求，给潜在的需求不一致提供定位策略。并使用模板提取需求语言中的关键词。

模型建立阶段：提取自然语言中的关键词后，使用表格转换法转换成自动机模型，并利用模型间的关联性转换成能被模型检验识别的形式模型(SMV模型)。同时在转换过程中，对属性进行说明，将属性规约用计算树逻辑(computaiton tree logic,CTL)进行描述。

模型检验阶段：根据转换成的形式模型和时态逻辑公式，利用NuSMV结构和语义上的关联制定出转换规则[5]，并把转换后的模型利用模型检验工具检测其中与属性规约不一致的地方，得出满足或者不满足属性规约的结论，为需求模型的完善提供关键性意见。

2 基于自然语言需求

2.1 需求子句相似度模型

在需求分析过程中，表达能力较强的自然语言常用于需求描述，不同参与者从不同角度描述的需求不可避免存在重复现象，Spanoudakis认为两个需求描述元素之间存在重叠关系，重叠关系有4种，包含无重叠关系、完全重叠关系、包含性重叠关系和部分重叠关系，当重叠关系出现后3种的时候，才可能会导致需求描述的不一致性的现象发生，可以说需求重叠现象是出现需求不一致的根本原因。考虑到需求描述重叠的情况，本文提出使用相似度方法计算自然语言描述需求，若两个自然语言的需求描述相似度越高说明重叠概率越大，即存在需求不一致的概率越大。

本文以自然语言需求子句为结点，构建了一种需求子句模型。如图2所示，使用句子相似度算法，表征句子之间的相似性。

图2 由自然语言生成的需求子句模型

在处理过程中，将自然语言描述的需求划分为需求子句(sentence)，然后对需求子句进行分词处理,统计每个需求子句中词语的词频(F)和词性(N),利用相似度算法计算出这些需求子句的相似度，把具有相似度需求子句放到一个组里。其中,词频(F)表示需求子句中某个关键词出现次数的统计量，初始值为1，随着不断切词累增。词性(N),是一组枚举值，取值范围{n,v,adj,adv,nq,pro,pre,con}分别表示名词、动词、形容词、副词、数量词、代词、介词、连接词,为了解决部分词语不规范的问题，使用可替换同义词(T)表示需求领域内对某些名词的通用规范用法。算法1给出了需求子句相似度的计算过程，相应的算法伪代码表示如下：

算法1： 需求子句相似度算法

Input: Requirement Description;

Output: Similar Sentence;

begin:

Requirement Description(DS)∅； //需求描述

Requirement Sentence(RS) ∈∅； //需求子句为空

n* RS ← DS； //将需求描述转换为n个需求子句

i=0,j=0; //设置变量i,j初始化

forall the Ai∈ RSido

n*Ai*Fi+n*Ai*N =RSidivided; //遍历所有子句， 将子句进行分词处理， 划分成词频和词性

newAi=n*Ai*Fi+n*Ai*N+T; //出现不规范词用专业词替换

forall the Fiin new Ando //重复遍历每一个分词处理结果

j=i；

forall the Fjin new An/2do //任意两个之间作比较

j=i;

if(SimFreq(Fj,new An/2)>0.5) //相似度大于0.5

then

add Fj∪new An/2join Similar Sentence[ ]//相似的放在一组

n++; //继续循环

i++; //继续循环

end;

需求描述里的关键词信息能够直观反应关键词在文本中的重要程度[6]，当关键词在文档中出现的次数越多，说明该词所占比例越大即所占的权重越高。本文借鉴于传统的VSM[7]计算方法，基于向量空间模型的算法，使用两个向量的夹角表示出两个向量之间的相似度。其计算过程如式(1)所示

(1)

通过式(1)来计算两个需求子句之间的相似度, 首先根据上文提到的需求子句进行分词处理，然后进行词频计算并形成特征向量，这样可以将两个需求子句这种非结构化数据抽象为向量表现形式, 之后便可以将自然语言表述的需求问题转换成数学上的向量夹角问题，同时需求关键词词频的数量在一定程度上能够反映重要程度，当需求描述文本规模比较大时，使用此方法可以有效且快速找出需求相似的地方，为解决需求不一致提供定位策略。示例过程如下所示：

假设有两个需求描述子句见表1。

表1 需求相似度计算示例

以上需求子句经过分词处理得：

需求子句1:“乘客 按下 向上 按钮 电梯 响应 请求 向上运行”

需求子句2:“乘客 按下 向下 按钮 电梯 响应 请求 向下运行”

获得向量集 “乘客 按下 向上 向下 按钮电梯 响应 请求 向上运行 向下运行”

对于需求子句A:乘客(1)按下(1)向上(1)向下(0)按钮(1)电梯(1)响应(1)请求(1)向上运行(1)向下运行(0)。

对于需求子句B:乘客(1)按下(1)向上(0)向下(1)按钮(1)电梯(1)响应(1)请求(1)向上运行(0)向下运行(1)。

经过词频计算得A需求子句的特征向量 {1,1,1,0,1,1,1,1,1,0}， B需求子句的特征向量 {1,1,0,1,1,1,1,1,0,1}。 根据式(1)计算得两个需求子句的相似度为2/3，说明两句需求描述的语句比较相似，根据需求重叠理论，需求越相似的地方存在不一致的概率越大,所以首先定位到这两句需求描述的位置，以这两句为基础结合上下文进行建模分析。

2.2 需求子句提取自动机模型

自动机是有限状态机(FSM)的数学模型, 是表示有限个状态以及在这些状态之间的转移和动作等行为的模型。有限状态机是一个五元组： (Σ,Q,Δ,q0,F)， 其中：Σ是一个有限字母表。 Q是一个有限状态集合。 Δ⊆Q×Σ→Q代表变迁关系。q0⊆Q是起始状态。 F⊆Q是终止状态的集合。

自动机可以用于并发系统和交互式系统建模。一个简单的自动机模型如图3所示，q0表示系统的起始状态，q2和q3是终止状态F，q1是过程状态，它们都属于状态集合Q， 其余为状态变迁。状态Q和字母表Σ都可以表示待建模系统状态的集合。本节中，将需求定义为一组由动作序列控制的状态变迁关系[8]，以此刻画自动机模型,将具有分解规范的自然语言指定为由事件(Event)、状态(State)以及动作列表(Action)组成的结构。这种类型的规范结构描述了一个由动作和事件驱动的状态改变结构。其中，Event 是指导致系统表现出可预测行为的动作或过程。State表示某时刻系统的某个行为。Action表示人或系统的操作列表，可能会导致状态的改变。一个简单的状态变迁如图4所示。

图3 简单自动机模型

图4 一个Event事件的状态变迁

本文结合此方法和BDL方法[9]对模型进行改进，改进后的表述使用电梯模型描述此行为，见表2.

表2 具有分解规范的自然语言分解过程

使用以上表格分解规范时，需要施加规则。其中Action中的Agent表示代理，可以参与到一个或多个动作当中，是与系统交互的人或系统，是行为的执行者。Activity是人或者系统执行的操作，可能会导致状态的改变，是行为本身。Object是受到原子动作中代理和资源作用影响的人或其它系统，是行为的被执行者。在电梯模型中，由于Action而导致整个系统的改变，开始时电梯在一楼，为空闲状态，乘客进入电梯后,电梯由空闲变为待载，等待上行的指令。当乘客按下按钮时，乘客作为代理操纵了系统，导致了系统状态的改变，电梯由待载状态变为上升状态。根据上文提到的表格将具有分解规范的自然语言描述的需求分解成自动机模型如图5所示。

图5 电梯空闲事件的自动机模型

图5描述了由自然语言过渡到自动机模型的一个例子，从图中可以看出，由于整个的Action行为才导致系统状态的变迁，这符合BDL中描述的行为执行者依照软件功能对被执行者实施操作的过程。

3 基于模型检验的一致性验证

模型检验最早是由Clarke和Emerson以及Quielle和Sikakis在针对时态逻辑实际验证算法时提出。目前在系统的安全性和一致性方面应用很广[10],模型检验是一种自动验证系统模型是否具有特定性质的方法，简单来说就是先把系统建模为有限状态转移系统，后利用时态逻辑描述待验证的规范，对整个系统的行为空间进行自动化遍历搜索，与定理证明按照一步步展开严格证明推导不同，模型检验具有自动化和高效化的特点。

在模型检验中，把系统的状态变换等价为变量值的变化，变量值的改变体现了状态的迁移，利用状态间的约束关系和状态转移的关联关系构成自动机模型或状态图[11]，因此在模型检验中使用上文的自动机模型可以将系统和待检测的性质用同一种方式来表示。其检验过程如图6所示。

图6 模型检验过程

本文将需求描述的系统模型的自动机图，转化为一个模型检验的问题，即将自然语言描述的需求问题，转换模型检验中的“状态不可达”，“不存在此条路径”等类似性质进行验证[12]。通过建立被测系统的状态行为模型，并用CTL时态逻辑描述系统待验证的性质，经由模型检验工具NuSMV检测，最终得出一条反例。反例的出现首先表明性质规约验证了模型，其次反例的出现可以加大对模型的理解，发现模型的不足。基于此，增加对模型的验证部分，包括可达性，前向一致性，陷阱性质的验证。其中，可达性的表述为在一次状态变换中，总是至少存在一条路径可以到达目标状态。前向一致性的表述为如果某个状态S1出现，那么该系统模型在后续变换中一定能够出现可预见的状态S2。例如，事件S1表示电梯系统启动，事件S2表示乘客按下上行按钮，事件S3表示电梯到达目标楼层。则事件S1和事件S2满足前向一致性。陷阱性质的描述为对某一性质进行取反操作，由模型检验的工具进行检测。通过检测以上性质可以得出和预期不一致的地方，并通过产生的反例帮助构建更为完整的需求模型。

3.1 定 义

定义1 Kripke结构。令AP为原子命题集合，则AP上的Kripke结构M是一个三元组M=(S,R,L)， 其中，S是状态的有限集合，R是完全变迁关系，L是标记函数，它标记在该状态下为真的原子命题集合。

Kripke结构有向图中，用圆圈表示可能的事件，有向弧线表示可能事件的关系，标记函数在圆圈内。

定义2 计算树逻辑(CTL*)。是一种离散、分支时间、命题时态逻辑，将系统的状态变化的所有可能性表示为树状结构。

计算树逻辑的语法结构如下：CTL*式由路径量词和时序运算符组成。路径量词的作用是表述计算树逻辑的结构，由A和E两种构成,如图7所示。

图7 CTL公式结构

A表示从当前开始在未来的所有路径符合某一性质。E表示从当前开始在未来至少有一条路径符合性质。有5个基本的运算符，直观上的意义如下：

X(“Next”)说明从某状态起始路径的第二个状态开始，性质满足。

F(“Finally”)刻画从路径中的某个状态开始，最终性质满足。

G(“Global”)说明性质在路径上的每个状态都满足。

U(“Until”)表示在此状态之前路径上所有状态第一性质满足。

R(“Release”)表示从当前状态开始到满足第一个性质的状态结束，第二个性质一直保持成立。

3.2 模型检验算法

本文以一个简单的例子来说明模型检验算法。例如：房间加热器可能处于如下的4种状态中的任何一个：Idle——空闲状态；End——结束使用；Heat——开始加热，达到某个温度；Warning——系统警告。图8给出了房间加热器Kripke结构。为清楚起见，每个状态都用在该状态为真的原子命题和在该状态为假的原子命题的否定形式标记出来，带箭头的弧标记表示了引起状态变迁的动作名称。

图8 房间加热器的Kripke结构

因为结果集合中没有包含初始状态1，所以可以得出结论：这个用Kripke结构描述的系统不满足给定的性质规约。

3.3 模型转换与模型检验

采用模型检验方法需要对被测系统进行建模分析，用时序逻辑描述系统的结构和性质，利用模型内部的状态迁移关系来验证整个模型内部某些特定性质是否正确。本文用模型检验中的SMV语言描述描述待测系统，用CTL时态逻辑描述系统性质。对模型内部中系统状态的可达性进行分析。

将上文提到的自动机图提取状态元素转换成SMV模型，以供模型检验的工具所识别。SMV模型包含变量声明模块VAR和IVAR，关键字定义模块MOUDLE；使用ASSIGN模块定义系统的初始状态，使用INIT定义系统初始状态的变量值。其对应转换规则见表3。

表3 自动机图中元素与SMV的对应关系

按照表3的描述，可以将上文中的自动机图用SMV的语法表达出来。如下所示:

MOUDULE main

VAR

state：{IDLE,UP,DOWN}

button_F1:boolean

ASSIGN:

init(state):IDLE;

init(button_F1):false;

next(state):case

state:IDLE&button_F1:UP

esac;

可以看出，提取出图中元素后按照对应关系可以将上文提到的自动机模型逐步转换成能被模型检验工具所识别的SMV模型。

4 案例分析—电梯模型

由于完整的系统模型庞大而复杂，本文通过精简电梯模型[13]，选取电梯模型对上述研究方法进行验证。

4.1 电梯模型的描述与建模

电梯的功能分为上行、下行、报警、显示、开/关门、电话机报警等。该模型的部分自然语言描述如下：

上行：电梯初态停在一楼。当乘客按下上行按钮后，电梯响应乘客的请求，向上运行。到达乘客所在楼层后，打开电梯门，乘客进入电梯，电梯检测乘客重量是否超标。如果超重就报警，否则就关闭电梯门。然后乘客在电梯内按下目标楼层。电梯系统判断目标楼层大于当前楼层，电梯向上运行。到达后乘客打开电梯门，乘客离开。电梯停在该楼层，并重新处于静止状态。

下行：当乘客按下下行按钮后，电梯响应乘客的请求，向下运行。到达乘客所在楼层后，打开电梯门，乘客进入电梯，电梯检测乘客重量是否超标。如果超重就报警，否则就关闭电梯门。然后乘客在电梯内按下目标楼层。电梯系统判定目标楼层小于当前楼层，电梯向下运行，到达后乘客打开电梯门，乘客离开。电梯停在该楼层，并重新处于静止状态。

报警：乘客在电梯内按下报警按钮，或者电梯出现故障紧急停止后，报警。

显示：显示面板会一直显示电梯的状态(运行状态、当前所在楼层)；如果发生故障或者乘客按下报警按钮，显示面板显示为“不可用”。

开/关门：乘客在电梯内/外按下开/关门的按钮后，电梯响应，打开或关闭电梯门。

对以上自然语言使用2.1节中的相似度算法进行分析，得到描述上行和下行需求描述的相似度约为0.95，说明两个需求描述存在重叠的地方，所以定位到这两个需求描述的位置，以此位置开始进行建模分析，避免遇到大规模的需求描述无法快速找到潜在不一致需求的情况。发现具有相似性需求描述后，根据2.2节中的分解规范提取自动机模型，其分解过程见表4。

表4 分词提取后的结果

根据表格提示结合上下文补充必要的节点可以生成自动机模型，为了便于观察，转换成自动机形式，如图9所示。根据表3的方法结合图6，可以简单生成一个电梯系统的SMV模型，该模型表述如下所示：(由于篇幅有限，只选取部分关键代码)。

图9 电梯模型的自动机模型

MODULE main

VAR

state:{Up,Down,Hold,Idle,Waiting,Warning,Stop,Fault};

position:{F1,F2,F3};

button_F1:boolean;

……

door_F1:{Opening,Opened,Closing,Closed};

door_F2:{Opening,Opened,Closing,Closed};

door_F3:{Opening,Opened,Closing,Closed};

passenger:{None,In,Out};

weight:{None,Normal,Overload};

arrived:boolean;

emergency:boolean;

ASSIGN

init(state)：= Idle;

init(passenger):=None;

……

next(position):=case

position=F1&state=Up:F2;

position=F2&state=Up:F3;

position=F2&state=Down:F1;

position=F3&state=Down:F2;

door_F1=Closed&(!button_F1)&position=F1

&state=Up:F2;

door_F3=Closed&(!button_F3)&position=F3

&state=Down:F2;

door_F2=Closed&(!button_F2)&position=F2

&state=Up:F3;

door_F2=Closed&(!button_F2)&position=F2

&state=Down:F1;

TRUE:position;

esac;

next(state):= case

state=Idle&(door_F1=Opening&passenger=In

&weight=Normal): Waiting;

state=Idle&(passenger=In&weight=Overload):

Warning;

state=Waiting&(passenger=In&weight=Normal&(button_F2|button_F3)): Up;

state=Waiting&(passenger=In&weight=Normal&

button_F1|button_F2): Down;

state=Waiting&emergency:Stop;

……

esac;

上述代码是对电梯模型的一个描述，代码中有几处省略部分，其中第一处是button_F2,button_F3,request_F1,request_F2,request_F3的数据类型，为boolean型，第二处是weight,button_F1,button_F2,button_F3,door_F1,door_F2,door_F3,arrived的初始化描述。第三处省略的部分是对电梯状态state和按钮状态door_F1,door_F2,door_F3的条件选择结构。

4.2 属性规约提取与验证

属性规约是系统运行过程中必须满足的规范，其保证了系统的一致性和安全性。针对于本文提到模型，主要从以下几个方面进行验证：①安全性。一个系统的运行首先要保证其安全性，对此要验证的是：在未来的任意一个时刻，电梯系统都不会把乘客困在电梯中。②前向一致性。电梯系统的运行需要满足前向一致性。对此验证电梯初始状态为空闲状态时，当有乘客进入时，未来的某一状态会由于超重导致电梯报警。③可达性。对此要验证电梯系统的自动机模型是否可以到达任何一个图中描述的状态。④陷阱性质。根据自动机图中描述的状态变迁，人为增加一条和某一行为需求描述相似的变迁，对其进行取反操作，观察模型检验能否检测出相似且不一致的行为。对此要验证当有乘客在一楼且按下上行按钮后，电梯不会出现上行状态。检测结果见表5。

表5是对以上几个属性规约性的表述。图10是NuSMV的验证结果。下面对NuSMV的验证结果进行分析。①安全性的CTL描述是在所有正常情况中，乘客不能被困在电梯中，结果显示是true，验证该电梯模型具有安全性质。②前向一致性。结果显示是true。表示在模型转换过程中状态前后的变迁关系是正确的，说明按照本文的转换规则从自然语言转换的自动机模型是可信的。③可达性的表述为，按照需求定义的功能判断整个系统中的某个

表5 性质验证结果

图10 NuSMV验证结果

状态是否可达，结果显示false，反例的出现说明了与预期不一致的行为，帮助构建更为完善的需求模型。④陷阱性质。结果显示是false。表示能够检测出需求描述不一致的行为。反例的出现首先说明了能够检测出与描述不一致的行为，其次，根据反例提供的路径信息可以进一步分析模型的内在联系，帮助构建更为全面的需求模型。

事实上，当变换面临的状态越多时，则所需要遍历的路径也就越多，不仅工作量大，而且容易忽略一些状态变换；而模型检验可以自动遍历所有状态，遇到与预期性质不一致的情况时自动生成一条反例。通过分析反例得出通过自然语言建立的模型的不足之处，以供继续分析完善模型。另一方面，当模型的状态空间变得足够大时，人工的方法几乎已经无法解决状态的遍历问题，只能依靠自动或者半自动的方法，这也是模型检验的优势所在。

5 结束语

针对于需求分析阶段难以获得清晰且一致性需求，本文提出一种使用自然语言和模型检验相结合的方法，使用相似度算法解决需求不一致定位问题，后进行模型提取和转换，并使用模型检验的方法进行验证和分析。最后通过电梯系统模型进行验证。结果表明，本文提到的方法有效，有助于对复杂系统的建模分析和测试。今后将继续对此方法进行研究，使其具有更高的普遍性并侧重于开发一套完整的工具集，便于更好的分析和验证。