基模型检验需求致突消解研究
摘
着软件规模增软件需求分析变越越重目前建模分析方法定效果理实践方面存着描述需求致变更困难等问题文针问题进行研究：
发现需求描述中致问题首先然语言需求描述进行相似度计算模型检验提供定位策略然通然语言分解提取形成动机模型动机模型属性规约时交模型检验工具进行验证模型检验工具出属性规约致者致方
发现需求突进行消解首先需求进行分类分成功性需求非功性需求功性需求采需求关联度方法进行消解非功性需求采代价权衡策略进行突消解通样例说明提出方法性文提高软件需求质量方面定理意义应价值
关键词：模型检验 需求相似度 需求关联度代价权衡策略
Research on requirement inconsistency and conflict resolution based on model checking
Abstract
With the increase of software scale software requirement analysis is becoming more and more important Using some current modeling and analysis methods has certain effect but there are still some problems in theory and practice such as inconsistent requirements and change difficulties This paper studies these problems as follows
In order to find the inconsistencies in the requirement description we first use natural language to calculate the similarity of the requirement description and provide the positioning strategy for the model test Then through the decomposition and extraction of natural language an automata model is formed The automata model and the attribute specification are submitted to the model checking tool for
verification at the same time Finally the consistency or inconsistency between the model checking tool and the attribute specification is obtained
In order to resolve the conflict of requirements firstly different requirements are classified into functional requirements and non functional requirements The functional requirements are resolved by the method of demand relevance and the non functional requirements are resolved by the cost tradeoff strategy Finally an example is given to show the reliability of the proposed method Therefore this paper has certain theoretical significance and application value in improving the quality of software requirements
Keywords： Model Checking Requirement SimilarityRequirement Relevance Cost Tradeoff strategy
目录
第章 引言 1
11 研究背景意义 1
12 国外研究现状 3
13文研究容创新点 4
131 文研究容 4
132 文创新点 5
14 文组织结构 5
第二章 框架研究建立 6
21 需求致问题概述 6
211 需求致相关研究 6
22 需求突消解问题概述 7
221 需求突消解相关研究 7
23 研究整体框架 8
24 结 9
第三章 基模型检验需求致研究 10
31 基然语言需求描述转换 11
311 需求子句相似度模型 11
312 动机模型 14
313 然语言提取动机模型 15
32 基模型检验需求致 17
321 模型检验相关定义 19
322 模型检验实现 20
323 模型转换 22
324反例作 23
33 结 25
第四章 需求突消解研究实现 26
41 概述 26
42 功性需求突消解 27
421 需求关联性致化程度 27
422 基需求关联度突消解 28
43 非功性需求消解 30
431 代价权衡分析 30
432 度量策略 30
433 度量策略 32
44 结 36
第五章 案例分析 37
51电梯模型描述建模 37
52 属性规约提取验证 41
53 需求突消解 43
54结 44
第六章 总结展 44
61 总结 44
62 展 45
参考文献 46
攻读学位期间研究成果 48
附录1 农夫河问题SMV语言描述 49
致 谢 51
学位文独创性声明 52
学位文知识产权权属声明 53
第章 引言
11 研究背景意义
软件开发初期软件规模功简单软件开发阶段注重编码工作着计算机软件规模断扩功逐渐复杂原注重编码方式满足日益复杂需求软件危机开始爆发开始认识软件工程中技术方法软件开发程中重性关资料统计软件项目中40~60需求阶段埋祸根原容易忽略需求相关问题系列问题容易导致续阶段出现严重错误设计BoehmPapaccio1988年研究报告中表明[1]果需求定义程中找出修改基需求问题代价12设计阶段代价升 5编码时代价10单元测试时20系统提交代价变成200出正确软件开发阶段需求问题已变非常重
软件质量求越越高需求工程软件工程重分支便应运生需求工程着重研究利效技术工程化方法进行描述分析需求工程终目通系列科学效方法获取高质量软件需求[2]般意义软件工程包含需求开发需求理两部分中需求开发包含需求获取需求分析建模编写软件规格说明需求验证需求理包含需求踪需求变更控制等整软件开发生命周期中软件需求获取分析十分重部分首解决问题软件需求指户解决问题达目标需条件权反应系统系统部件满足合标准规模正式规定文档需具条件权文档说明般包括功性需求非功性需求[3]综软件需求应种清晰简明致二义性方式开发系统中方面进行描述集合
软件开发中软件设计实现程错误会导致软件项目失败软件需求分析存缺陷时设计实现程软件必然存错误获取分析形成正确二义性需求时更软件项目成功软件需求分析阶段涉众复杂需求变更频繁系统复杂度断提高导致需求分析变越越困难中需求致存会导致软件系统混乱甚错误许复杂软件系统中会概率出现需求致般说出现需求致原纳两点：需求描述阶段视点利益相关者事物描述存差异二需求迭代完善性维护中断增加新需求原旧需求间存致复杂系统说身描
述致新需求带致问题会系统带系列问题
需求致出现会系统出现矛盾甚错误目前量专家学者研究需求致问题般分三方面需求致检测诊断需求致处理需求致度量评估需求分析中需求致问题需求分析者需花费量时间种方法查找中问题然修正需求分析中出现错误目前方法进行需求分析处理时避免存问题：
（1）需求描述形式化难保障户分析员理解
需求描述阶段形式化方法VDMZ方法B方法等然前统建模语言UML拥更加严格语义推理机制研究发现需求描述接触普通需求分析者没非常专业数学知识样利需求模型构建
（2）难需求潜需求致进行定位
遇规模需求描述时纯手动方法已完成需求文档编写需动半动方法方法中少涉关需求致定位策略实际规模需求描述中需排关素保证需求描述正确性致性
（3）发现消致方法单
目前软件开发中系统需求持续更改断提出新需求情况更加频繁[4]需求致发现消方法单传统消致方法般侧重某点实际着系统复杂影响需求致素越越单素考虑消致适应复杂系统变化
文研究需求获取需求分析阶段发现消需求致问题通需求分析阶段需求描述进行分析建立模型实现发现需求致性根发现致运相应策略进行消解旨通文方法获取清晰完整致性系统需求通分析现研究方法优缺点提出种基模型检验需求致分析方法然语言描述需求中提取出出动机模型模型转换方法转换成模型检验够识模型模型检验工具动遍历模型出致方基础发现致需求结合需求关联度代价权衡提出消解策略结合类权衡代价进行需求突消解
文开展研究课题具方面重意义：
（1）然语言描述需求相似度算法潜需求致提供定位策略
（2）模型检验方法动遍历然语言形成动机模型出预期致方
（3）需求进行分类需求关联度代价权衡策略发现需求突提供消解方法策略
12 国外研究现状
年关需求致需求突消解问题已方面研究
研究需求致问题Nuseibe[5]等提出需求致理框架说具代表性工作框架中提出致性规关重需求致相规言分类采典逻辑方法通检测逻辑表达式值发现需求致[6]类方法需求描述逻辑断言进行关联运逻辑推理方法找出逻辑断言中矛盾进表示出需求描述中矛盾
二采模型检验方式检测需求规格说明中错误Heitmeyer C L[7]提出基模型检验检测需求致框架种方法需求表示状态变量通动遍历状态变量取值预期否相检测需求致三基目标方法先初始需求定义目标通目标分解抽象求精等目标子目标间关联约束等发现目标间致矛盾Van Lamsweerde A[8]KAOS方法进行需求描述设立目标级解决异常四基图描述方法方法通定某图性质语义关系检测出需求描述间致Glinz M[9]提出场景模型类模型相结合通建立交叉引检测中致问题
检测需求致问题处理需求突问题研究Lee K H[10]提出博弈基目标方法分析需求间权衡问题目标模型分析利益相关者目标意图博弈知识分析需求间权衡Sadiq M[11]提出种基模糊方法面目标需求启发程中需求优先级进行排序方法然二叉树排序方法获取需求优先级列表发生突需求提供消解策略Suhaib M[12]认软件开发阶段必须意识类型风险需求突识软件工程关键目标模型矩阵知识量化子目标间突步需求突消解做准备Gulzar K[13]提出新框架该框架侧重模糊逻辑性需求属性映射户语言评估框架优先考虑突性需求属性框架旨通动识解决性需求突整程帮助需求分析员做出更决策系统中务涉确定属性
权重考虑定量定性评估标准中重性Hassine J[14]提出面目标需求语言GRL集成i*NFR框架提出验数统计分析利统计学方法帮助检测解决目标模型中突Zhang W等[15]认现基证相似性需求突研究计算复杂度难满足系统实时性求提出DEMATEL新方法重新考虑证权重总关系矩阵出相似度然计算重性基Dempster合规获权重方法效处理矛盾降低计算复杂度
关需求致性需求突消解问题国许相关研究朱学峰金枝[16]需求致理方面工作做较系统分析总结目前需求致性处理三种方法需求重叠理提出种需求致理框架张建等[17]提出模型检验方法进行致性验证UML(Unified Modeling Language)模型集合转化成时间动机网络模型模型检验工具进行致性验证周宇等[18]提出种种行角度分析采时间动机软件演化程中致性方法层次模型转化干行时间动机模型利模型检验方法工具进行验证张璇等[19]鉴微观济领域生产理提出优权衡代价决策方法着重实现选择优方案实现需求突间佳权衡李瑞轩等[20]根策略目标出两种非致突消解方法代价方法字典编辑优方法认某策略加权突面较较该策略余策略发生突性较高湛浩旻等[23]需求层次出发提出解释结构层次分析法相结合ISM(Interpretative Strucuural Model)方法进行分层处理APH(analytic hierchy process)方法进行优先级排序需求出现突时通需求优先级消突王守堰等[24]博弈中纳什均衡策略应需求突中SCRI(strategy choosing tool for resolving inconsistency)工具妥协谈判架构消需求描述中致需求
13文研究容创新点
131 文研究容
文研究发现需求描述中致现象解决致需求突研究容：
（1）解需求分析需求工程重性通研究前需求致方法提出种新需求致研究方法需求致问题需求突消解问题融入架构中建立统模型
（2）文现研究基础需求致问题进行研究针需求致检测文提出模型检验方法进行改进提取然语言描述需求利相似性原理解决需求致定位问题制定出套完整模型转换方法供模型检验工具识
（3）针需求分析中者续增加新功等导致需求突问题文需求关联度代价权衡角度考虑综合考虑突类代价提出完整突消解框架消者减少需求突
（4）通案例实际展示文提出基模型检验方法需求工程中应
132 文创新点
文创新点包括：
（1）提出套完整需求致检测消解方法基础构建新建模分析框架
（2）改进基模型检验方法解决模型检验发现需求致问题定位问题规模需求分析减少工作量
（3）需求突单素消解现类代价权衡方法方法考虑更加适应时代软件发展脚步
14 文组织结构
文六章节组成章节容：
第章：引言章阐述课题研究背景意义介绍需求致性理需求突消解国外研究发展现状目前存问题说明文研究容创新点
第二章：研究框架建立章介绍需求致问题突消解问题前研究进行总结然前研究基础提出新需求致突消解研究方法结合该方法出文研究需求致需求突消解研究框架
第三章：基模型检验需求致研究章介绍基模型检验需求致问题总结模型检验优缺点提出需求子句相似度算法解决模型检验足处总结制定然语言动机模型间转换规模型检验工具验证
第四章：需求突消解研究实现针前文发现需求致需求突问题章出相应消解策略分析现突消解方法首先需求突进行分类针功性需求采基关联度方法进行消解针非功性需求采基验代价权衡方法进行消解
第五章：案例分析文提研究方法章通实际电梯模型案例说明文提方法行性效性
第六章：总结展总结文做工作成果然针文研究容方法提出足处未研究工作做出展
第二章 框架研究建立
21 需求致问题概述
软件需求种清晰简明致二义性方式开发系统中方面进行描述集合软件需求分析目获清晰完整高质量需求文档必须科学方法技术户软件开发程中提出需求进行整理分析外软件需求中软件设计程中约束非功性需求软件运行时软件关系需分析象
需求致问题软件系统开发中关键性问题问题处理坏直接影响软件规格说明书质量进影响软件产品质量需求致源视点角度分析需求分析员利益相关者事物描述相导致致产生参者事物前描述出现致现象
211 需求致相关研究
关需求致问题已研究关需求致研究方面：
基定理方法：定理证明方法形式化验证方法方法思想需求描述形式化逻辑表达式然利定理证明中常方法：纳总结方法然演绎法基表方法等方法找出需求描述中蕴含矛盾方法旦检测出矛盾表示需求描述中出现致现象基定理方法优点严谨具部分动推理力年
NASA等基定理方法动实现航天软件正确性缺点基定理证明方法十分强调逻辑性验证导致需求描述形式化难普通需求分析利益相关者掌握定理证明效率高阻碍技术身发展
基模型检验方法：模型检验方法利状态搜索原理种半形式化方法模型检验基思想需求等价系统状态变量状态变量取值表示系统处状态然设定性质规约通遍历系统状态出预先设定性质规约致方基模型检验方法优点完全动化速度快基定理方法样具良定检测程模型检验方法检测致存状态空间急剧增长影响身方法效率法准确定位问题文第三章详细说明改进方法
基目标方法基目标方法认需求阶段务确定系统想实现目标实现目标需约束条件通建立需求阶段目标服务约束规格说明系统实现作目标断分解精化抽象关系中两目标实现果具阻碍（thwarting）破坏（break）损害（hurt）负影响（some）关系时认出现两目致问题中较代表性工作时KAOS框架NFR框架i*语言等基目标方法优点便表达处理突需求
基图描述方法：基图描述方法种半形式化方法原理利面象图形形式UML中图相结合需求致检测策略通常根转换图特性语义检测出部致性优点图描述方法便表示理解缺点推导程逻辑性足
外某特定需求致问题采工检测方法
22 需求突消解问题概述
需求突消解需求致问题续步骤需求致实际需求分析中需求突检测需求突消解提供消解方法需求突消解功性分分成功性需求突消解非功性需求突消解模态形式分静态消解动态消解处理方法分直接法修正突法需求优先级划分法基协商方法等
221 需求突消解相关研究
关需求突消解处理方法分方面：
直接突：种方法突消解中直接快方法种方法强调需求分析者续新功增加时发现两存突需求时根系统特殊求直接某需求删例某软件系统中强调某项核心功时旦遇核心功致需求直接删掉需求保证没突发生种方法实际操作中常加较考虑情况直接删需求实际系统整体功削弱
修正突：种方法思想出现需求突时发生突两需求采修正改进策略通常会采弱化分解合需求方式两突需求减突甚完全消解掉种方法较复杂消解方式消解程中保证消解效性保证通弱化分解合新需求原需求间没突
基优先级策略：种方法强调种方法需求设定优先级序需求突出现时根预先设定需求优先级优先级低需求舍弃优先先实现优先级高需求样消解掉突需求基优先级策略较效方法相直接删修正突方法种方法权衡利弊做出决定关需求优先级分类例：基风险需求优先级排序基需求性优先级排序基属性决策需求优先级排序等方法外种方法常结合APH（层次分析法）Delphi法（专家调查法）等方法定性定量考虑决策方法避免素带观影响种方法通常缺乏优先级协商决策调整机制般出较单优先级方案
基协商消解策略：基协商突消解思想通分析利益相关者（stakehold）间利益体现消解需求突需求出现致时基协商消解策略出现突两需求进行识找出需求利益相关者然矩阵公式逻辑表达式等利益相关者进行协商处理种方式修正突方式区基协商方法更加考虑需求背利益相关需求认需求突质利益相关者需求求
23 研究整体框架
文前研究基础提出新研究框架图21示框架包含两部分第部分需求致研究鉴模型检验思想建模准备阶段然语言需求进行描述便理解采相似度算法模型检验提供定位策略提供系列转换规转换模型属性规约交模型检验验证终出属性规约致者致结果第二部分需求突处理部分部分中通发现需求进行分类分成功性需求非功性需求功性需求提出需求关联度方
法进行消解突中关联度需求进行舍弃者精化非功性需求继续分解度量策略度量策略度量策略提出基验方法进行消解度量策略
结合优先级策略协商策略改进代价权衡策略
24 结
节分析现需求致研究方法需求突消解方法建立新基模型检验需求致研究框架提出相应需求突消解方法通突类型分采消解方法外模型检验实现定位问题通相似度方法进行定位完善基模型检验需求致方法
图21研究架构图
第三章 基模型检验需求致研究
文第二章介绍研究架构方法章根前文框架解决需求致确定问题章首提出然语言模型检验相结合方法确定需求致问题提出需求子句相似度模型根模型然语言描述需求进行相似度较确定存需求致方模型检验提供定位策略时然语言描述需求中提取动机模型提出套模型转换方法然语言描述需求转换成模型检验工具够识模型然转换模型提出属性规约起模型检验工具进行验证出属性规约致者致方相应反例
31 基然语言需求描述转换
311 需求子句相似度模型
需求描述程中表达力较强然语言常常需求描述然语言描述需求更需求相关者参中需求更加全面完善然语言描述需求中参者视角描述需求避免存致现象Spanoudakis[23]认两需求描述元素间存重叠关系种重叠关系四种包含重叠关系完全重叠关系包含性重叠关系部分重叠关系重叠关系出现三种时候会导致需求描述致性现象发生说需求重叠现象出现需求致根原考虑需求描述重叠情况文提出相似度方法计算然语言需求描述两然语言需求描述相似度越高说明重叠概率越存需求致概率越种方法文模型检验提供定位策略
节然语言需求子句结点构建种需求子句模型图31示句子相似度算法表征句子间相似性处理程中节然语言描述需求划分需求子句(sentence)然需求子句进行分词处理程中统计需求子句中词语词频(F)词性(N)利相似度算法计算出需求子句相似度具相似度需求子句放组里中词频(F)表示需求子句中某词出现次数统计量初始值1着断切词累加词性(N)组枚举值取值范围分名词（n）动词（v）形容词（adj）副词（adv）数量词（nq）代词（pro）介词（pre）连接词（con）解决部分词语规范问题换义词
(T)表示需求领域某名词通规范法
图31需求子句相似度模型
算法31出需求子句相似度计算程相应算法伪代码表示：
算法31需求子句相似度算法
Input Requirement Description
Output Similar Sentence
begin
Requirement Description(DS) ∉∅需求描述
Requirement Sentence(RS) ∈ ∅需求子句空
n* RS ← DS 需求描述转换n需求子句
i0j0设置变量ij初始化
forall the Ai∈ RSi do
n*Ai*Fi+n*Ai*N RSi divided 遍历子句子句进行分词处理划分成词频词性
newAi n*Ai *Fi +n*Ai*N+T 出现规范词专业词换
foralltheFiinnewAndo 重复遍历分词处理结果
ji
forallthe Fj in newAn2 do 意两间做较
ji
if(SimFreq(FjnewAn2)>05) 相似度05
then
add Fj∪newAn2 join Similar Sentence[ ]相似放组
n++ 继续循环
i++ 继续循环
end
需求描述里关键词信息够直观反应关键词文中重程度[24]某需求关键词文档中出现次数越说明关键词整文档中占例越占权重越高求两需求子句间相似度文鉴传统VSM[25]计算方法基量空间模型算法两量夹角表示出两量间相似度程中词成维度词频率成值量样两需求子句相似度句子词频率构成空间计算程公式3(1)示
公式3(1)
SimFreqFSF·SF×S
i1n(xi×yi )i1nxi2×i1nyi2
通公式3(1)计算两需求子句间相似度 中FS分两需求子句量形式xiyi量值
文首先根文提需求子句进行分词处理然进行词频计算形成特征量样两需求子句种非结构化数抽象量表现形式 便然语言表述需求问题转换成数学量夹角问题时需求关键词词频数量定程度够反映重程度需求描述文规模较时方法效快速找出需求相似方解决需求致提供定位策略示例
程示：
假设两需求描述子句表31示
表31需求相似度计算示例
编号
然语言描述
1
客钮电梯响应请求运行
2
客钮电梯响应请求运行
需求子句分词处理：
需求子句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需求子句特征量{1110111110}B需求子句特征量 {1101111101}
根公式31计算两需求子句相似度
SimFreqFSF×SF×S 23
中
F1110111110S{1101111101}
F×S6
F12+12+12+02+12+12+12+12+12+024
S12+12+02+12+12+12+12+12+02+124
计算结果23说明需求描述中两需求子句较相似根需求重叠理需求越相似方存致概率越首先定位两句需求描述位置两句基础结合文进行建模分析
312 动机模型
动机限状态机(FSM)数学模型 表示限状态状态间转移动作等行模型限状态机五元组：（ΣQΔq0F）
中：
Σ限字母表
Q限状态集合
Δ⊆Q×Σ→Q代表变迁关系
q0⊆Q起始状态
F⊆Q终止状态集合
图32动机模型
动机发系统交互式系统建模简单动机模型图32示q0表示系统起始状态q2q3属终止状态Fq1程状态属状态集合Q余状态变迁状态Q字母表Σ表示建模系统状态集合
313然语言提取动机模型
节中需求定义组动作序列控制状态变迁关系[26]刻画动机模型具分解规范然语言指定事件(Event)状态(State)动作列表(Action)组成结构种类型规范结构描述动作事件驱动状态改变结构中Event指导致系统表现出预测行动作程State表示某时刻系统某行Action表示系统操作列表会导致状态改变简单状态变迁图图33示
图33Event事件状态变迁图
节结合方法BDL方法Error Reference source not found模型进行改进改进表述电梯模型描述行表2示
表2 具分解规范然语言分解程
FSM中元素
元素
分类
提取
源
Event
Subject
电梯
n
Behavior
空闲升
v adv
q0QF
State
State
载升
v adv
Agent
客
n．
ΔΣ
Action
Activity
v
Object
钮
n．
表格分解规范时需施加规中Action中Agent表示代理参动作中系统交互系统行执行者Activity者系统执行操作会导致状态改变行身Object受原子动作中代理资源作影响系统行执行者电梯模型中Action导致整系统改变开始时电梯楼空闲状态客进入电梯电梯空闲变载等行指令客钮时客作代理操系统导致系统状态改变电梯载状态变升状态根文提表格具分解规范然语言描述需求分解成动机模型图34示
图34电梯空闲事件动机模型
图描述然语言渡动机模型例子图中出整
Action行导致系统状态变迁符合BDL中描述行执行者软件功执行者实施操作程
32 基模型检验需求致
模型检测种基状态搜索形式化验证技术采动化技术遍历状态空间检查遍历状态空间否满足提出性质规约果发现预期性质致方会动定位错误位置模型检测项技术已成功应计算机硬件通信协议控制系统安全认证灯方面模型检验方法优点模型检验方法动化方法检测程较快提供属性规约模型检测工具动出属性规约致方通常说反例说明什满足方便查找检测需求分析设计中缺陷
模型检验早ClarkeEmersonQuielleSikakis针时态逻辑实际验证算法时提出目前系统安全性致性方面应广[27]模型检验种动验证系统模型否具特定性质方法简单说先系统建模限状态转移系统利时态逻辑描述验证规范整系统行空间进行动化遍历搜索定理证明步步展开严格证明推导模型检验具动化高效化特点
模型检测般包含三步骤系统建模性质描述性质验证
系统建模（modeling）：模型检验方法形式化方法首先需测系统进行形式化测系统中提取出Kripke结构者穷状态变迁系统结构中增加初始状态集终止状态集通常需建模时候利抽象技术进行剪枝减少模型状态爆炸问题
性质描述（specification）：通常建立系统总期该系统满足定性质安全性致性等性质描述已建立模型通常采模态逻辑时态逻辑公式动机形式表示性质称属性规约
性质验证（verification）：性质验证工作里利现模型检验工具属性规约动验证肯定者否定结果肯定表示属性规约符合开始预期说明性质验证否定表示属性规约符合预期出反例会产生错误路径帮助分析者设计者踪发生源
模型检验中系统状态变换等价变量值变化变量值改变体现状态迁移利状态间约束关系状态转移关联关系构成动机模型状态图[29]模型检验中文动机模型系统检测性质种方式表示检验程图35示
文需求描述系统模型动机图转化模型检验问题然语言描述需求问题转换模型检验中状态达存条路径等类似性质进行验证[30]
图35模型检验程
通建立测系统状态行模型CTL时态逻辑描述系统验证性质模型检验工具NuSMV检测终出条反例反例出现首先表明性质规约验证模型次反例出现加模型理解发现模型足基增加模型验证部分包括达性前致性陷阱性质验证中达性表述次状态变换中总少存条路径达目标状态前致性表述果某状态S1出现该系统模型续变换中定够出现预见状态S2例事件S1表示电梯系统启动事件S2表示客行钮事件S3表示电梯达目标楼层事件S1事件S2满足前致性陷阱性质描述某性质进行取反操作模型检验工具进行检测通检测性质出预期致方通产生反例帮助构建更完整需求模型
321 模型检验相关定义
定义：Kripke结构：令AP原子命题集合APKripke结构M三元组M(SRL)中S状态限集合R完全变迁关系L标记函数标记该状态真原子命题集合
Kripke结构图中圆圈表示事件弧线表示事件关
系标记函数圆圈图36示
图36 Kripke结构
CTL*种离散分支时间命题时态逻辑系统状态变化性表示树状结构CTL*公式原子命题布尔运算符时态算子路径量词构成CTL*公式两种类型：状态公式路径公式路径量词作表
述计算树逻辑结构AE两种构成
A表示前开始未路径符合某性质E表示前开始未少
条路径符合性质
时态算子5基运算符直观意义：
X(Next)说明某状态起始路径第二状态开始性质满足
F(Finally)刻画路径中某状态开始终性质满足
G(Global)说明性质路径状态满足
U(Until)表示状态前路径状态第性质满足
R(Release)表示前状态开始满足第性质状态结束第二性质
直保持成立
总根语法规CTL*状态公式集合描述反应式系统状态间转换序列形式化方法
定义2：计算树逻辑（computation tree logic）CTLCTL*子逻辑限制时态算子XFGUR必须前面加路径量词
定义3线性时态逻辑LTL：LTLCTL*子逻辑公式具形式Af中
f路径公式包含f里子状态公式仅仅原子命题
区：
图 37状态迁移系统
CTLLTL两系统例考虑图37状态迁移系统T：
显然T⊨FGp考虑路径ppppppp…该路径意节点AGp均成立T⊭AFAGp两性质样存状态转移中公式
成立成立描述非性质CTL*逻辑CTLLTL组合逻辑模型检验中常运
322模型检验实现
文简单例子说明模型检验算法例：房间加热器处四种状态中：Idle——空闲状态End——结束Heat——开始加热达某温度Warning——系统警告图38出房间加热器Kripke结构清楚起见状态该状态真原子命题该状态假原子命题否定形式标记出带箭头弧标记表示引起状态变迁动作名称
根图描述结构提出性质规约CTL公式描述：AG(Idle→AFIdle)该公式等价EF(IdleEGHeat)满足原子公式状态集合开始标记进复杂子公式令S(g)表示子公式g标记状态集合
S(Idle){2567}
S(Idle){12356}
计算S(EGIdle)首选出S’S(Idle)中非强联通分量集合SCC{{1235}}续步骤求EGHeat标记状态集合SCC中元素集初始时
T{1235}S’中没状态着S’中条路径达T中意状态计算中止
S(EGIdle){1235}
接计算S(IdleEGIdle){25}
计算S(EF(IdleEGIdle))时首先令TS(Idle
EGIdle)接着变迁关系逆关系标记满足公式状态
S(EF(IdleEGIdle){1234567}
S(EF(IdleEG Idle))
结果集合中没包含初始状态1出结：Kripke结构描述系统满足定性质规约
图38房间加热器Kripke结构
323 模型转换
采模型检验方法需测系统进行建模分析时序逻辑描述系统结构性质利模型部状态迁移关系验证整模型部某特定性质否正确文模型检验中SMV语言描述描述测系统CTL时态逻辑描述系统
性质模型部中系统状态达性进行分析
文提动机图提取状态元素转换成SMV模型供模型检验工具识SMV模型包含变量声明模块VARIVAR关键字定义模块MOUDE
ASSIGN模块定义系统初始状态INIT定义系统初始状态变量
值应转换规表32示
表32 动机图中元素SMV应关系
图中元素
SMV模型
说明
State
VARIVAR
变量声明状态集合
（源状态初始状态
目标状态）
ASSIGN(init)
定义约束集合
Event
Next
表示状态改名前状态收题代理影响准备迁移状态
Action
case…esac
系统状态变量受触发引起确定状态
表32描述文中动机图SMV语法表达出示
MOUDULE main
VAR
state：{IDLEUPDOWN}
button_F1boolean
ASSIGN
init(state)IDLE
init(button_F1)false
next(state)case
stateIDLE&button_F1UP
esac
出提取出图中元素应关系文提动机模型逐步转换成模型检验工具识SMV模型
324反例作
节典山羊河问题说明模型检验反例应问题描述：带着狼山羊白菜条河左岸条船正装三者行物带岸次带样东西摆渡河
狼羊留岸顾狼会羊吃掉样羊白菜岸顾羊会吃白菜中MGCWEmpty表示初始状态—左边符号表示应符号左岸—右边服务表述应符号右岸
M表示G表示羊goatC表示白菜CabbageW表示狼wolf
箭头表示表示次船运输物品种类详细描述参见附录1
图39 农夫河问题限状态机
安全河条件
TLSPEC
E [( ((goatwolf)> (goatferrymen)) & ((goatcabbage)>(goatferrymen)))U ((cabbageTRUE)& (goatTRUE) & (wolfTRUE) &(ferrymenTRUE))]
图310 模型检验正例验证
验证条件图310示显示true说明提出安全河性质规约建立模型说正确模型检验工具NuSMV会提供符合性质例子反例反例安全河条件取反
TLSPEC
E [( ((goatwolf)> (goatferrymen)) & ((goatcabbage)>(goatferrymen)))U ((cabbageTRUE)& (goatTRUE) & (wolfTRUE) &(ferrymenTRUE))]
表示存样条路径然交模型检验工具NuSMV验证验证结果图311示结果显示出性质规约false出条反例反例出现说明出现属性规约致方直接出条路径
图311 模型检验反例验证
33 结
节模型检验研究容通然语言相似度算法模型检验提供定位策略然语言描述中提取出动机模型进模型转换方法变成模型检验工具够识语言通样例说明模型检验工作原理说明模型检验反例作
第四章 需求突消解研究实现
章中模型检验然语言相结合方法研究需求致问题需求分析程者系统升级增加新功等导致需求致问题发生应该消掉发生需求致章需求突消解问题章首先突需求进行分类分解成功性需求非功性需求针两种类型需求突采消解方式功性需求采关联度方法进行消解非功性需求鉴济学中生产理成分析法提出代价权衡策略综合考虑非功需求达消解突目
41 概述
针型软件复杂系统开发获取更加全面需求防止需求信息遗漏需视点利益相关者（stakeholder）角度进行考虑分析中视点利益相关者需求避免存突需求突消解成需求分析中法回避重问题种方法消解掉需求描述中突
突消解问题般需求优先级权重两角度分析需求优先级权重需求优先级解决需求突问题时般结合具体方法层次分析法（Theanalytichierarchy process）简称AHP基思路建立系统层次结构模型关某项需求素属性分解成目标层指标层方案层然通构造矩阵判断矩阵中某元素标度分计算单次组合权量决定出元素优先级高元素优先级低外AHP方法进行组合做改进方法基ISM（InterpretativeStructuralModelMothod）AHP方法相结合基SAHP方法基Topsis（Technique for Order Preference by Similarity to an Ideal Solution ）AHP结合方法等类方法确定优先级方法KNAO模型KANO模型户需求分基型期型兴奋型差异型反型分析户需求户满意度影响体现户需求满足程度户满意间非线性关系部分优先级方法较单缺乏动态调整决策机制种解决突方法确定需求权重权重衡量总体中单位标志值总体中作数值表示某项指标系统中重程度表示指标项变情况指标项变化结果影响权重赋值方法常见三类：观赋权法客观赋权法组合赋权法中观赋权法通常专家调查法（Delphi法）层次分析法（AHP
法）二项系数法客观赋权法包括成分分析法熵值法目标规划法离差方差法等客观赋权法结合观客观思想客观赋权法包括折衷系数综合权重法线性加权单目标优化方法熵系数综合集成法外权值确定属性决策方法例DEMATEL方法C2R方法等属性决策方法通常结合需求优先级综合考虑权重问题
突stakeholder角度分析分业务突目标突情感突节指目标类突目标类突指系统需求般包含功性需求非功功性需求中功性需求求规定开发员必须产品中实现软件功户利功完成务满足业务需求系统中必须具备功软件非功需求称质量需求者质量属性实际软件属性者功需求约束非功需求软件产品满足户业务需求必须具功性需求外特性影响着产品否够持续高效提供服务非功性需求非功性需求重功性需求描述系统想完成功务非功性需求通常描述软件需满足某属性程度非功需求难量化手段表示满足需受时间成风险等种素影响
42 功性需求突消解
421 需求关联性致化程度
定义：需求关联性：基文然语言模型划分划分需求元素间否联系情况判断两者需求元素间否关联性
定义：需求关联度：需求关联度L针需求原集A需求突集B例关系公式1示
LiA∩BiA 公式4(1)
中：A需求原集文提出然语言分解需求集
B突集两部分部分原需求描述中突部分部分升级者增加新功导致原需求突部分
Bi突集中具体某突Bi⊂B
图41需求关联度
422 基需求关联度突消解
针功性需求间突节提出基需求关联度消解方法针复杂系统建模时消解流程概括：
（1）结合第三章划分成需求子句提取需求原集A
（2）根模型检验结果提取出两具突集BiBj
（3）根公式4(1)计算出突集BiBj需求原集A关联度
（4）分析较两突需求元素间关联度关联度更低
需求进行精化者舍弃
功性需求突消解中需求关联度重判断相直接根需求优先级方法需求关联度综合考虑需求元素间联系系统
状态图分解图42示
图中需求分解成干子需求子需求刻画成状态模式出确定系统说状态变迁关系应该唯确定现假设突需求集B加入需求原集A中新需求q10原集中q3突会引起系统确定等问题提取出q3需求图43示突集B需求原集存关联性示意图44示出突集B中包含元素中需求原集重叠重叠部分取出进行发现q3需求需求原
集4关联q10需求原集3关联关关联
图42 系统需求分解
根节式4(1)出q3需求关联度 Lq3A∩BiA41040q10需求关联度Lq3A∩BiA31030根需求关联度理应该q10需求进行舍弃者精化
图43 突集提取
图44新突集
43非功性需求消解
431 代价权衡分析
文针非功需求难量化问题鉴济学理改进非功性权衡代价分析方法改进目保证两非功需求发生突时总代价损失整体保证软件质量软件非功需求突质利益相关者策略执行避免引入果策略执行会导致突情况提升某非功性需求必须执行特定策略例软件会安全性响应时间作非功需求需考虑素情景中考虑安全性
强制实施密码策略增加密码复杂度认证程序程中复杂度增加势必导致响应时间增加说针两非功性需求提升安全性时必然会损害响应时间者说提高响应时间代价降低系统安全性必须找非功需求间佳权衡点系统整体代价损失
文鉴济学中代价权衡理济学中生产理需求工程相结合综合权衡非功性代价代价损失更表达非功需求文讲非功需求分两类类度量策略类度量策略
432 度量策略
度量策略通常现量化方式非功需求进行量化处理说难采数学方法非功需求进行代价权衡例Stacey Matrx模型
中图45示
图45 STACEY矩阵模型
问题没确定时果关系明显垂直（Y）轴团队团队组织间问题决策达成致程度频谱端果问题存高度确定性致性决策容易领域称（理性简单）传统方法（瀑布）方法效范围没该问题达成致意见没确定果关系区计划通常慷慨混乱政府状态盛行区极端稳定稳定性逆转极端应该避免混沌区域频谱两极端间存称复杂区区域里传统方法情感复杂区域中系统预测区域提前指定产品详细信息准确度方面详细信息达成致条件需户开发员间协作环境佳方法敏捷需高度创造力创新产生解决方案敏捷开发中软件项目构建切分成子项目子项目成果测试具备集成运行特征简单说敏捷开发追求前期完美设计完美编码力求短周期开发出产品核心功早发布出版然续生产周期新需求断迭代升级完善产品敏捷开发中强调作单功入手遇需求突时难
权衡量化针度量策略基验方法进行突消解基验需求突消解：
（1）型团队开始发挥作单位组建
（2）发现突时先进行部讨果员部讨解决突案例放策略库中备
（3）果部讨没解决问题进入调解程序 调解程序目员开发验进行决策解决策略放策略库中
433 度量策略
度量非功需求突采济学中生产理非功需求进行权衡分析例信软件中认果软件行总预期相致称信信软件应该软件结果预期够预期解决采取度量策略
定义1：策略代价Ps：策略S代价Ps实施策略S引发非功需求集合R策略代价P成PM函数关系中
（1）S满足非功需求必须实施某策略
（2）R策略S引发突非功需求集合∀r∈R 具体非功需求
（3）PM策略S时产生工作量成代价
定义2：成代价PM：PM策略S产生成公式：
PMA×（SIZE）E×i1nEMi(i123…17)
中：
（1）PM总工作量策略S时成
（2）A生产率常数COCOMOⅡ中A通常取值298
（3）SIZE估算软件功单元代码行数
（4）E指数子反应项目规模济性
（5）EMi成驱动子获取影响完成项目需工作量软件开发特征成驱动子模型系数COCOMOⅡ中定义17成驱动子
中指数子E计算公式：
E091+001j15SFj
式中j123…5指数子E体现5例子SFj作说明规模软件项目具相规模济济性SFj 例子项目工作量指数变化生产率变化重成规模子登记变动范围低极高
济学生产理中生产函数Q劳动L资K函数关系
Qf(LK)生产理描述两非功需求突时LK两突素r1r2Q产生策略代价度量P然度量值构造代价线图43示PM两突素中中变量产生成代价线图44
示n1n2分指策略S实施产生需权衡非功需求突策略S实施时r1度量值x1时r2应度量值y1r1取x2时r2取y2次类推产生策略S策略代价线P成代价线PMn1变量时r1非功需求取值x1确定时产生成代价y1r1非功需求取值x2时确定成代价y2类推产生策略成代价曲线PM策略代价线Pxiyi决定代价点描述策略S实施非功需求r1r2间反应权衡关系策略成线PM反应策略S实施阶段成代价权衡关系视r1r2间弹性代关系图4x见果r1取高点x4n2取低点y4类似r1降低求时取x3时n2达y4高y3r1r2间视消彼长代关系关系描述非功需求间相互代代价成代价线图x示需求r1取值x1时产生成y1需求r1取值x2时产生成y2
图43策略代价
图44成代价
优权衡代价决策图43出某策略实施非功性需求增强会导致非功需求降低者减弱动态程基思想需非功需求增加必约束样找利益相关者优权衡代价 图43示策略代价增加两约束条件利益相关者非功需求优先级约束便某非功需求低约束基线优先级约束线利益相关者非功需求间突权衡关系图45示干条直线表示非功需求
优先级约束斜率r1r2说明两非功需求r1优先级r2高利益相关者更需r1效率R1R2说明两非功需求R1优先级R2低利益相关者更需R2低约束基线利益相关者某项非功需求低限制图4x中阴影部分非功需求中低限制容分享网站中显示容量响应时间突量项调查显示户愿意等6秒超6秒会失耐心样系统说响应时间非功需求低约束基线6秒样容量低约束
基两约束条件出约束条件优策略代价图46阴影部分示R1min表示非功需求R1低约束基线R2min表示非功需求R2低约束基线(R1R2)1(R1R2)2分表示非功需求R1R2两种优先级两非功需求R1R2说首先排范围策略X1剩余两策略X2X3优策略需继续引入成代价线PM图47示图中出根前文R1PM关系成代价线策略代价线融合坐标系中出成代价线阴影部分交点PM1表示需求R1成变化关系需考虑X2X3应Y2Y3PM1绝距离保留距离成代价曲线点PM1策略X3非功需求R1R2代价权衡策略已出
图45约束策略
图46基约束策略代价
图47优权衡代价
44 结
节建立发现需求突基础需求突进行分类功性需求采需求关联度方法进行消解非功性需求采代价权衡策略进行消解终实现需求致性
第五章 案例分析
完整系统模型庞复杂文通精简电梯模型[31]Error Reference source not found选取电梯模型述研究方法进行验证
51电梯模型描述建模
电梯功分行行报警显示开关门电话机报警等该模型部分然语言描述：
行：电梯初态停楼客行钮电梯响应客请求运行达客楼层开电梯门客进入电梯电梯检测客重量否超标果超重报警否关闭电梯门然客电梯目标楼层电梯系统判断目标楼层前楼层电梯运行达客开电梯门客离开电梯停该楼层重新处静止状态
行：客行钮电梯响应客请求运行达客楼层开电梯门客进入电梯电梯检测客重量否超标果超重报警否关闭电梯门然客电梯目标楼层电梯系统判定目标楼层前楼层电梯运行达客开电梯门客离开电梯停该楼层重新处静止状态
报警：客电梯报警钮者电梯出现障紧急停止报警
显示：显示面板会直显示电梯状态(运行状态前楼层)果发生障者客报警钮显示面板显示
开关门：客电梯外开关门钮电梯响应开关闭电梯门
然语言21节中相似度算法进行分析描述行行需求描述相似度约095说明两需求描述存重叠方定位两需求描述位置位置开始进行建模分析避免遇规模需求描述法快速找潜致需求情况发现具相似性需求描述根
312节中分解规范提取动机模型分解程表51示
表51 分词提取结果
项
需求描述
根分解规范提取
应元素
#1
电梯初停楼
停（电梯楼）
State
#2
客行钮
（客钮）
Action
#3
电梯响应客请求运行
（电梯客）
State
#4
客达楼层客进入电梯
达进入（客楼层电梯）
Action
#5
电梯检测重量否超标
检测（电梯超标）
Action
#6
达客开电梯门客离开
开离开（客电梯门）
Action
#7
客行钮
（客钮）
Action
#8
电梯响应客请求运行
（电梯客）
State
#9
…
…
…
…
…
…
…
根表格提示结合文补充必节点生成动机模型便观察转换成动机形式图52示根文表32方法结合图34简单生成电梯系统SMV模型该模型表述示：（篇幅限选取部分关键代码）
图52 电梯模型模型描述
MODULE main
VAR
state{UpDownHoldIdleWaitingWarningStopFault}
position{F1F2F3}
button_F1boolean
……
door_F1{OpeningOpenedClosingClosed}
door_F2{OpeningOpenedClosingClosed}
door_F3{OpeningOpenedClosingClosed}
passenger{NoneInOut}
weight{NoneNormalOverload}
arrivedboolean
emergencyboolean
ASSIGN
init(state) Idle
init(passenger)None
……
next(position)case
positionF1&stateUpF2
positionF2&stateUpF3
positionF2&stateDownF1
positionF3&stateDownF2
door_F1Closed&(button_F1)&positionF1
&stateUpF2
door_F3Closed&(button_F3)&positionF3
&stateDownF2
door_F2Closed&(button_F2)&positionF2
&stateUpF3
door_F2Closed&(button_F2)&positionF2
&stateDownF1
TRUEposition
esac
next(state) case
stateIdle&(door_F1Opening&passengerIn
&weightNormal) Waiting
stateIdle&(passengerIn&weightOverload) Warning
stateWaiting&(passengerIn&weightNormal&(button_F2|button_F3)) Up
stateWaiting&(passengerIn&weightNormal& button_F1|button_F2) Down
stateWaiting&emergencyStop
……
esac
述代码电梯模型描述代码中处省略部分中第处button_F2button_F3
request_F1request_F2request_F3数类型boolean型第二处weightbutton_F1button_F2
button_F3door_F1door_F2door_F3arrived初始化描述第三处省略部分电梯状态state钮状态door_F1door_F2door_F3条件选择结构
52 属性规约提取验证
属性规约系统运行程中必须满足规范保证系统致性安全性针文提模型方面进行验证
(1)安全性系统运行首先保证安全性验证：未意时刻电梯系统会客困电梯中
(2)前致性电梯系统运行需满足前致性验证电梯初始状态空闲状态时客进入时未某状态会超重导致电梯报警
(3)达性验证电梯系统动机模型否达图中描述状态
(4)陷阱性质根动机图中描述状态变迁增加条某行需求描述相似变迁进行取反操作观察模型检验否检测出相似致行验证客楼行钮电梯会出现行状态检测结果表52示
表52 性质验证结果
验证性质
CTL性质描述
验证结果
安全性
SPEC AF (passengerIn>AG passengerOut)
true
前致性
SPEC AF(stateIdle&passengerIn>EF state Warning)
true
达性
SPEC AF(stateIdle > AG stateWarning)
false
陷阱性质
SPEC AG (position F1&state Up >AX position F2)
false
表属性规约性表述图53 54NuSMV验证结果面NuSMV验证结果进行分析
(1)安全性CTL描述正常情况中客困电梯中结果显示true证明该电梯模型具安全性质
(2) 前致性结果显示true表示模型转换程中状态前变迁关系正确说明文转换规然语言转换动机模型信
(3)达性表述需求定义功判断整系统中某状态否达结果显示false反例出现说明预期致行帮助构建更完善需求模型
(4)陷阱性质结果显示false表示够检测出需求描述致行反例出现首先说明够检测出描述致行次根反例提供路径信息进步分析模型联系帮助构建更全面需求模型
图 53验证结果1
图54验证结果2
事实变换越面状态越时需遍历路径越仅工作量容易忽略状态变换模型检验动遍历状态遇预期性质致情况时动生成条反例通分析反例出通然语言建立模型足处供继续分析完善模型方面模型状态空间变足够时工方法已法解决状态遍历问题动者半动方法模型检验优势
53 需求突消解
51节中出电梯系统模型基础假设电梯系统时需求改变增加条新需求全动化更加智化增加电梯操作均通智声控设备完成
原文中加入新需求增加SMV描述：
autostate{upDownHoldStop}
next(autostate)case
autostateup&(arrived&door_F1Opening|door_F2Opening|door_F3Opening)&passengerOut)Hold
autostateDown&(arrived&(door_F1Opening|door_F2Opening|door_F3Opening)&passengerOut)Hold
autostateHold&emergencyStop
TRUE autostate
esac
提出属性规约：
SPEC AF(state Stop & handleFALSE&emergencyTRUE > EG state Idle )
通模型检验工具出条反例图55示
图55模型检验结果
反例出条路径分析路径出出repairhandle状态均标记false关联状态stopfault 解释动化操作法处理电梯状态状态根
423节提出需求关联度方法autostate状态关联4原集8状态根文公式4(1)关联度12stopfault关联状态6根公式4(1)关联度23根需求关联度方法应该autosate需求进行重新考虑考虑删者精化
54结
节电梯系统实例基础文提出电梯系统需求进行致性验证验证文提方法行性外需求突消解类问题电梯系统中文提需求突消解方法进行分类相应方法进行消解达预期目标
第六章 总结展
61 总结
文研究种基模型检验需求致需求突消解方法通分析目前现需求致方法提出新基模型检验然语言相结合需求致研究框架提出模型框架进行致性验证外需求突消解问题提出需求关联度方法解决功性需求突非功性需求提出权衡策略解决突度量非功需求基验方法解决突度量方法代价权衡策略方法综合较出优代价策略文通电梯系统实例验证行性分析效验证
通文研究完成目标容：
（1） 分析现需求致建模方法应提出新基模型检验需求致研究框架
（2） 然语言进行分解提取利相似度算法计算出然语言描述相似性解决模型检验定位问题
（3） 提出套完整模型提取转换方法基然语言描述进行分类提取转换成动机模型然动机模型转换成模型检验够动识语言模型检验工具进行动识
（4） 突消解文出两种类突消解方法功性需求突消解问题需求关联度思想关联度低进行舍弃者精华消解掉需求突
（5） 非功需求突提出代价权衡策略进行分析综合考虑策略代价成代价济学生产理进行分析考虑消解非功需求突
（6） 结合电梯模型实际案例证实基模型检验需求致模型效意义电梯模型基础实现文提致性验证需求突处理问题验证文研究行性效性
62 展
文基模型检验需求致问题研究需求突消解然取定成果然存定局限性需进步进行研究：
（1） 文提出基模型检验需求致问题研究文中涉然语言相应模型基础进行分析步应该继续完善改进模型具更高普遍性
（2） 文需求突消解较合理方法发生需求突进行分类采方法进行消解考虑方面够例文没详细说明模型检验然语言功性需求非功性需求分类步考虑然语言处理中引入属性分解模型检验中引入时间动机等概念更表示非功性需求外某度量非功需求约束低约束高约束步工作约束进行更加深刻研究
（3） 文电梯实例相较简单没包含更加复杂系统功步工作研究更加复杂系统文研究容应复杂实际项目中更验证方法行性
参考文献
[1] Leffingwell D Widrig D Management Software Requirements：A Unified Approach[M] New JerseyAddisonWesley 2000 6572
[2] Pandey D Suman U Ramani A K An effective requirement engineering process model for software development and requirements management[C]2010 International Conference on Advances in Recent Technologies in Communication and Computing IEEE 2010287291
[3] 毋国庆等软件需求工程[M]北京机械工业出版社20088
[4] urkiewica J Nawrocki J Ochodek M et alHAZOPbased identification of events in use cases[J] Empirical Software Engineering 201520(1)82109
[5] Nuseibeh B Easterbrook S Russo A Leveraging inconsistency in software development[J] Computer 2000 33(4) 2429
[6] Walter B Hammes J Piechotta M et al A Formalization Method to Process Structured Natural Language to Logic Expressions to Detect Redundant Specification and Test Statements[C] Requirements Engineering Conference IEEE 2017(38) 263272
[7] Heitmeyer C L Jeffords R D Labaw B G Automated consistency checking of requirements specifications[J] Acm Transactions on Software Engineering & Methodology 1996 5(3)231261
[8] Van Lamsweerde A Letier E Handling obstacles in goaloriented requirements engineering[J] IEEE Transactions on Software Engineering 2000 26(10) 9781005
[9] Glinz M A lightweight approach to consistency of scenarios and class models[C] Requirements Engineering 2000 Proceedings 4th International Conference on 20004958
[10] K Lee and S Lee Applying Game Theoretic Approach to GoalDriven Requirements TradeOff Analysis for SelfAdaptation 2015 IEEE 39th Annual Computer Software and Applications Conference Taichung 2015 pp 330335
[11] Applying fuzzy preference relation for requirements prioritization in goal oriented requirements elicitation process [J] International Journal of System Assurance Engineering and Management 2014 5(4) 711723
[12] Suhaib M Ohnishi A Potential Conflicts Identification among Sub Goals in Goal Oriented Requirement Analysis Using Matrix[J] International Journal of Progressive Sciences and Technologies (IJPSAT) 2018 10(2)
[13] Gulzar K Sang J Ramzan M et al Fuzzy approach to prioritize usability requirements conflicts An experimental evaluation[J] IEEE Access 2017 5 1357013577
[14] Hassine J Amyot D An empirical approach toward the resolution of conflicts in goaloriented models[J] Software & Systems Modeling 2017 16(1) 279306
[15] Zhang W Deng Y Combining conflicting evidence using the DEMATEL method[J] Soft computing 2019 23(17) 82078216
[16] 朱雪峰 金芝 关软件需求中致性理[J] 软件学报 2005(07)2838
[17] 张建 吴俊 方景龙 模型动转换致性验证方法[J] 计算机工程设计 2017(9)
[18] 周宇 黄延凯 et al 种开放环境软件线演化致性验证方法[J] 软件学报 2015 26(4)747759
[19] 张璇 王旭 李彤 et al 软件非功需求权衡代价[J] 软件学报 2017(5)
[20] 李瑞轩 鲁剑锋 李添翼 et al 种访问控制策略非致性突消解方法[J] 计算机学报 2013(06)88101
[21] 湛浩旻 印桂生 赵蕴龙 基ISMAHP组合需求优先级排序方法Method of Prioritizing Requirements Based on the Combination of ISM and AHP[J] 计算机科学 040(3)225227243
[22] 王守堰 金英 张晶 Nash equilibrium strategy choosing method for resolving inconsistencies of requirements解决需求致纳什均衡策略选取方法[J] 计算机应研究 2015 000(002)466469474
[23] Spanoudakis G Finkelstein A Till D Overlaps in Requirements Engineering[J] Automated Software Engineering 1999 6(2)171198
[24] Xu Haoguang Wang Ning Liu Jiaming et al Comprehensive Computation Algorithm of Similarity for Natural Language Retrieval [J] Computer system application 2017 26(6)170175
[25] Cong Y Chan Y B Ragan M A A novel alignmentfree method for detection of lateral genetic transfer based on TFIDF[J]Scientific Reports 2016 6(30308)113
[26] Rui S Deming Z Translating software requirement from natural language to automaton[C]
International Conference on Mechatronic Sciences IEEE 201424562459
[27] Jin Huan Huang Qing Requirement formal modeling and quality characteristics verification based on scene behavior [J] Computer Applied Research 2016 33(5)13841398
[28] Huang Wudan Chen Zhe Model Checking of Security Issuses in Border Gateway Protocol [J] Journal of Chinese Computer Systems
201738(6)11881191
[29] Li Jiali Chen Yongle Li Zhi et al RTSP protocol vulnerability mining based on protocol state graph traversal [J] Computer Science 2018 45 (9) 171176
[30] He Yang Hong Mei Qi Linying et al Functional test case generation method based on model checking tool NuSMV [J] Computer application 2015 (A02) 155159
[31] Li Xin ASchedulingStrategy of TargetLayerReservationElevatorGroupBasedonModelCheckingMethod [D]NanchangJiangxi University of Finance and Economics 20181154
致 谢
研究生生活接尾声三年时间里导师xxx教授学生活中种指导帮助xxx老师步步引导做研究选择文献样精读文献样泛读文献引导中发现问题进步指引提出解决办法魏老师悉心指导完成篇文
做研究外导师教会做名研究生样更杜工研究生时代合理安排时间学余研究生生活证丰富彩教会处事道理工作学子中收益终身衷魏老师说声谢谢
完成该文程中师哥师姐帮助师哥师姐帮助查文献提供参考书籍分享验教训文撰写中少走弯路感谢帮助外研究生生活必少班学研究生生活变更意义
感谢直支持鼓励父母家培养父母付出遇什困难坚强盾希身体健康
感谢评阅位老师感谢位老师文提出宝贵意见指导谢谢
文档香网(httpswwwxiangdangnet)户传
《香当网》用户分享的内容，不代表《香当网》观点或立场，请自行判断内容的真实性和可靠性！
该内容是文档的文本内容，更好的格式请下载文档
摘
着软件规模增软件需求分析变越越重目前建模分析方法定效果理实践方面存着描述需求致变更困难等问题文针问题进行研究：
发现需求描述中致问题首先然语言需求描述进行相似度计算模型检验提供定位策略然通然语言分解提取形成动机模型动机模型属性规约时交模型检验工具进行验证模型检验工具出属性规约致者致方
发现需求突进行消解首先需求进行分类分成功性需求非功性需求功性需求采需求关联度方法进行消解非功性需求采代价权衡策略进行突消解通样例说明提出方法性文提高软件需求质量方面定理意义应价值
关键词：模型检验 需求相似度 需求关联度代价权衡策略
Research on requirement inconsistency and conflict resolution based on model checking
Abstract
With the increase of software scale software requirement analysis is becoming more and more important Using some current modeling and analysis methods has certain effect but there are still some problems in theory and practice such as inconsistent requirements and change difficulties This paper studies these problems as follows
In order to find the inconsistencies in the requirement description we first use natural language to calculate the similarity of the requirement description and provide the positioning strategy for the model test Then through the decomposition and extraction of natural language an automata model is formed The automata model and the attribute specification are submitted to the model checking tool for
verification at the same time Finally the consistency or inconsistency between the model checking tool and the attribute specification is obtained
In order to resolve the conflict of requirements firstly different requirements are classified into functional requirements and non functional requirements The functional requirements are resolved by the method of demand relevance and the non functional requirements are resolved by the cost tradeoff strategy Finally an example is given to show the reliability of the proposed method Therefore this paper has certain theoretical significance and application value in improving the quality of software requirements
Keywords： Model Checking Requirement SimilarityRequirement Relevance Cost Tradeoff strategy
目录
第章 引言 1
11 研究背景意义 1
12 国外研究现状 3
13文研究容创新点 4
131 文研究容 4
132 文创新点 5
14 文组织结构 5
第二章 框架研究建立 6
21 需求致问题概述 6
211 需求致相关研究 6
22 需求突消解问题概述 7
221 需求突消解相关研究 7
23 研究整体框架 8
24 结 9
第三章 基模型检验需求致研究 10
31 基然语言需求描述转换 11
311 需求子句相似度模型 11
312 动机模型 14
313 然语言提取动机模型 15
32 基模型检验需求致 17
321 模型检验相关定义 19
322 模型检验实现 20
323 模型转换 22
324反例作 23
33 结 25
第四章 需求突消解研究实现 26
41 概述 26
42 功性需求突消解 27
421 需求关联性致化程度 27
422 基需求关联度突消解 28
43 非功性需求消解 30
431 代价权衡分析 30
432 度量策略 30
433 度量策略 32
44 结 36
第五章 案例分析 37
51电梯模型描述建模 37
52 属性规约提取验证 41
53 需求突消解 43
54结 44
第六章 总结展 44
61 总结 44
62 展 45
参考文献 46
攻读学位期间研究成果 48
附录1 农夫河问题SMV语言描述 49
致 谢 51
学位文独创性声明 52
学位文知识产权权属声明 53
第章 引言
11 研究背景意义
软件开发初期软件规模功简单软件开发阶段注重编码工作着计算机软件规模断扩功逐渐复杂原注重编码方式满足日益复杂需求软件危机开始爆发开始认识软件工程中技术方法软件开发程中重性关资料统计软件项目中40~60需求阶段埋祸根原容易忽略需求相关问题系列问题容易导致续阶段出现严重错误设计BoehmPapaccio1988年研究报告中表明[1]果需求定义程中找出修改基需求问题代价12设计阶段代价升 5编码时代价10单元测试时20系统提交代价变成200出正确软件开发阶段需求问题已变非常重
软件质量求越越高需求工程软件工程重分支便应运生需求工程着重研究利效技术工程化方法进行描述分析需求工程终目通系列科学效方法获取高质量软件需求[2]般意义软件工程包含需求开发需求理两部分中需求开发包含需求获取需求分析建模编写软件规格说明需求验证需求理包含需求踪需求变更控制等整软件开发生命周期中软件需求获取分析十分重部分首解决问题软件需求指户解决问题达目标需条件权反应系统系统部件满足合标准规模正式规定文档需具条件权文档说明般包括功性需求非功性需求[3]综软件需求应种清晰简明致二义性方式开发系统中方面进行描述集合
软件开发中软件设计实现程错误会导致软件项目失败软件需求分析存缺陷时设计实现程软件必然存错误获取分析形成正确二义性需求时更软件项目成功软件需求分析阶段涉众复杂需求变更频繁系统复杂度断提高导致需求分析变越越困难中需求致存会导致软件系统混乱甚错误许复杂软件系统中会概率出现需求致般说出现需求致原纳两点：需求描述阶段视点利益相关者事物描述存差异二需求迭代完善性维护中断增加新需求原旧需求间存致复杂系统说身描
述致新需求带致问题会系统带系列问题
需求致出现会系统出现矛盾甚错误目前量专家学者研究需求致问题般分三方面需求致检测诊断需求致处理需求致度量评估需求分析中需求致问题需求分析者需花费量时间种方法查找中问题然修正需求分析中出现错误目前方法进行需求分析处理时避免存问题：
（1）需求描述形式化难保障户分析员理解
需求描述阶段形式化方法VDMZ方法B方法等然前统建模语言UML拥更加严格语义推理机制研究发现需求描述接触普通需求分析者没非常专业数学知识样利需求模型构建
（2）难需求潜需求致进行定位
遇规模需求描述时纯手动方法已完成需求文档编写需动半动方法方法中少涉关需求致定位策略实际规模需求描述中需排关素保证需求描述正确性致性
（3）发现消致方法单
目前软件开发中系统需求持续更改断提出新需求情况更加频繁[4]需求致发现消方法单传统消致方法般侧重某点实际着系统复杂影响需求致素越越单素考虑消致适应复杂系统变化
文研究需求获取需求分析阶段发现消需求致问题通需求分析阶段需求描述进行分析建立模型实现发现需求致性根发现致运相应策略进行消解旨通文方法获取清晰完整致性系统需求通分析现研究方法优缺点提出种基模型检验需求致分析方法然语言描述需求中提取出出动机模型模型转换方法转换成模型检验够识模型模型检验工具动遍历模型出致方基础发现致需求结合需求关联度代价权衡提出消解策略结合类权衡代价进行需求突消解
文开展研究课题具方面重意义：
（1）然语言描述需求相似度算法潜需求致提供定位策略
（2）模型检验方法动遍历然语言形成动机模型出预期致方
（3）需求进行分类需求关联度代价权衡策略发现需求突提供消解方法策略
12 国外研究现状
年关需求致需求突消解问题已方面研究
研究需求致问题Nuseibe[5]等提出需求致理框架说具代表性工作框架中提出致性规关重需求致相规言分类采典逻辑方法通检测逻辑表达式值发现需求致[6]类方法需求描述逻辑断言进行关联运逻辑推理方法找出逻辑断言中矛盾进表示出需求描述中矛盾
二采模型检验方式检测需求规格说明中错误Heitmeyer C L[7]提出基模型检验检测需求致框架种方法需求表示状态变量通动遍历状态变量取值预期否相检测需求致三基目标方法先初始需求定义目标通目标分解抽象求精等目标子目标间关联约束等发现目标间致矛盾Van Lamsweerde A[8]KAOS方法进行需求描述设立目标级解决异常四基图描述方法方法通定某图性质语义关系检测出需求描述间致Glinz M[9]提出场景模型类模型相结合通建立交叉引检测中致问题
检测需求致问题处理需求突问题研究Lee K H[10]提出博弈基目标方法分析需求间权衡问题目标模型分析利益相关者目标意图博弈知识分析需求间权衡Sadiq M[11]提出种基模糊方法面目标需求启发程中需求优先级进行排序方法然二叉树排序方法获取需求优先级列表发生突需求提供消解策略Suhaib M[12]认软件开发阶段必须意识类型风险需求突识软件工程关键目标模型矩阵知识量化子目标间突步需求突消解做准备Gulzar K[13]提出新框架该框架侧重模糊逻辑性需求属性映射户语言评估框架优先考虑突性需求属性框架旨通动识解决性需求突整程帮助需求分析员做出更决策系统中务涉确定属性
权重考虑定量定性评估标准中重性Hassine J[14]提出面目标需求语言GRL集成i*NFR框架提出验数统计分析利统计学方法帮助检测解决目标模型中突Zhang W等[15]认现基证相似性需求突研究计算复杂度难满足系统实时性求提出DEMATEL新方法重新考虑证权重总关系矩阵出相似度然计算重性基Dempster合规获权重方法效处理矛盾降低计算复杂度
关需求致性需求突消解问题国许相关研究朱学峰金枝[16]需求致理方面工作做较系统分析总结目前需求致性处理三种方法需求重叠理提出种需求致理框架张建等[17]提出模型检验方法进行致性验证UML(Unified Modeling Language)模型集合转化成时间动机网络模型模型检验工具进行致性验证周宇等[18]提出种种行角度分析采时间动机软件演化程中致性方法层次模型转化干行时间动机模型利模型检验方法工具进行验证张璇等[19]鉴微观济领域生产理提出优权衡代价决策方法着重实现选择优方案实现需求突间佳权衡李瑞轩等[20]根策略目标出两种非致突消解方法代价方法字典编辑优方法认某策略加权突面较较该策略余策略发生突性较高湛浩旻等[23]需求层次出发提出解释结构层次分析法相结合ISM(Interpretative Strucuural Model)方法进行分层处理APH(analytic hierchy process)方法进行优先级排序需求出现突时通需求优先级消突王守堰等[24]博弈中纳什均衡策略应需求突中SCRI(strategy choosing tool for resolving inconsistency)工具妥协谈判架构消需求描述中致需求
13文研究容创新点
131 文研究容
文研究发现需求描述中致现象解决致需求突研究容：
（1）解需求分析需求工程重性通研究前需求致方法提出种新需求致研究方法需求致问题需求突消解问题融入架构中建立统模型
（2）文现研究基础需求致问题进行研究针需求致检测文提出模型检验方法进行改进提取然语言描述需求利相似性原理解决需求致定位问题制定出套完整模型转换方法供模型检验工具识
（3）针需求分析中者续增加新功等导致需求突问题文需求关联度代价权衡角度考虑综合考虑突类代价提出完整突消解框架消者减少需求突
（4）通案例实际展示文提出基模型检验方法需求工程中应
132 文创新点
文创新点包括：
（1）提出套完整需求致检测消解方法基础构建新建模分析框架
（2）改进基模型检验方法解决模型检验发现需求致问题定位问题规模需求分析减少工作量
（3）需求突单素消解现类代价权衡方法方法考虑更加适应时代软件发展脚步
14 文组织结构
文六章节组成章节容：
第章：引言章阐述课题研究背景意义介绍需求致性理需求突消解国外研究发展现状目前存问题说明文研究容创新点
第二章：研究框架建立章介绍需求致问题突消解问题前研究进行总结然前研究基础提出新需求致突消解研究方法结合该方法出文研究需求致需求突消解研究框架
第三章：基模型检验需求致研究章介绍基模型检验需求致问题总结模型检验优缺点提出需求子句相似度算法解决模型检验足处总结制定然语言动机模型间转换规模型检验工具验证
第四章：需求突消解研究实现针前文发现需求致需求突问题章出相应消解策略分析现突消解方法首先需求突进行分类针功性需求采基关联度方法进行消解针非功性需求采基验代价权衡方法进行消解
第五章：案例分析文提研究方法章通实际电梯模型案例说明文提方法行性效性
第六章：总结展总结文做工作成果然针文研究容方法提出足处未研究工作做出展
第二章 框架研究建立
21 需求致问题概述
软件需求种清晰简明致二义性方式开发系统中方面进行描述集合软件需求分析目获清晰完整高质量需求文档必须科学方法技术户软件开发程中提出需求进行整理分析外软件需求中软件设计程中约束非功性需求软件运行时软件关系需分析象
需求致问题软件系统开发中关键性问题问题处理坏直接影响软件规格说明书质量进影响软件产品质量需求致源视点角度分析需求分析员利益相关者事物描述相导致致产生参者事物前描述出现致现象
211 需求致相关研究
关需求致问题已研究关需求致研究方面：
基定理方法：定理证明方法形式化验证方法方法思想需求描述形式化逻辑表达式然利定理证明中常方法：纳总结方法然演绎法基表方法等方法找出需求描述中蕴含矛盾方法旦检测出矛盾表示需求描述中出现致现象基定理方法优点严谨具部分动推理力年
NASA等基定理方法动实现航天软件正确性缺点基定理证明方法十分强调逻辑性验证导致需求描述形式化难普通需求分析利益相关者掌握定理证明效率高阻碍技术身发展
基模型检验方法：模型检验方法利状态搜索原理种半形式化方法模型检验基思想需求等价系统状态变量状态变量取值表示系统处状态然设定性质规约通遍历系统状态出预先设定性质规约致方基模型检验方法优点完全动化速度快基定理方法样具良定检测程模型检验方法检测致存状态空间急剧增长影响身方法效率法准确定位问题文第三章详细说明改进方法
基目标方法基目标方法认需求阶段务确定系统想实现目标实现目标需约束条件通建立需求阶段目标服务约束规格说明系统实现作目标断分解精化抽象关系中两目标实现果具阻碍（thwarting）破坏（break）损害（hurt）负影响（some）关系时认出现两目致问题中较代表性工作时KAOS框架NFR框架i*语言等基目标方法优点便表达处理突需求
基图描述方法：基图描述方法种半形式化方法原理利面象图形形式UML中图相结合需求致检测策略通常根转换图特性语义检测出部致性优点图描述方法便表示理解缺点推导程逻辑性足
外某特定需求致问题采工检测方法
22 需求突消解问题概述
需求突消解需求致问题续步骤需求致实际需求分析中需求突检测需求突消解提供消解方法需求突消解功性分分成功性需求突消解非功性需求突消解模态形式分静态消解动态消解处理方法分直接法修正突法需求优先级划分法基协商方法等
221 需求突消解相关研究
关需求突消解处理方法分方面：
直接突：种方法突消解中直接快方法种方法强调需求分析者续新功增加时发现两存突需求时根系统特殊求直接某需求删例某软件系统中强调某项核心功时旦遇核心功致需求直接删掉需求保证没突发生种方法实际操作中常加较考虑情况直接删需求实际系统整体功削弱
修正突：种方法思想出现需求突时发生突两需求采修正改进策略通常会采弱化分解合需求方式两突需求减突甚完全消解掉种方法较复杂消解方式消解程中保证消解效性保证通弱化分解合新需求原需求间没突
基优先级策略：种方法强调种方法需求设定优先级序需求突出现时根预先设定需求优先级优先级低需求舍弃优先先实现优先级高需求样消解掉突需求基优先级策略较效方法相直接删修正突方法种方法权衡利弊做出决定关需求优先级分类例：基风险需求优先级排序基需求性优先级排序基属性决策需求优先级排序等方法外种方法常结合APH（层次分析法）Delphi法（专家调查法）等方法定性定量考虑决策方法避免素带观影响种方法通常缺乏优先级协商决策调整机制般出较单优先级方案
基协商消解策略：基协商突消解思想通分析利益相关者（stakehold）间利益体现消解需求突需求出现致时基协商消解策略出现突两需求进行识找出需求利益相关者然矩阵公式逻辑表达式等利益相关者进行协商处理种方式修正突方式区基协商方法更加考虑需求背利益相关需求认需求突质利益相关者需求求
23 研究整体框架
文前研究基础提出新研究框架图21示框架包含两部分第部分需求致研究鉴模型检验思想建模准备阶段然语言需求进行描述便理解采相似度算法模型检验提供定位策略提供系列转换规转换模型属性规约交模型检验验证终出属性规约致者致结果第二部分需求突处理部分部分中通发现需求进行分类分成功性需求非功性需求功性需求提出需求关联度方
法进行消解突中关联度需求进行舍弃者精化非功性需求继续分解度量策略度量策略度量策略提出基验方法进行消解度量策略
结合优先级策略协商策略改进代价权衡策略
24 结
节分析现需求致研究方法需求突消解方法建立新基模型检验需求致研究框架提出相应需求突消解方法通突类型分采消解方法外模型检验实现定位问题通相似度方法进行定位完善基模型检验需求致方法
图21研究架构图
第三章 基模型检验需求致研究
文第二章介绍研究架构方法章根前文框架解决需求致确定问题章首提出然语言模型检验相结合方法确定需求致问题提出需求子句相似度模型根模型然语言描述需求进行相似度较确定存需求致方模型检验提供定位策略时然语言描述需求中提取动机模型提出套模型转换方法然语言描述需求转换成模型检验工具够识模型然转换模型提出属性规约起模型检验工具进行验证出属性规约致者致方相应反例
31 基然语言需求描述转换
311 需求子句相似度模型
需求描述程中表达力较强然语言常常需求描述然语言描述需求更需求相关者参中需求更加全面完善然语言描述需求中参者视角描述需求避免存致现象Spanoudakis[23]认两需求描述元素间存重叠关系种重叠关系四种包含重叠关系完全重叠关系包含性重叠关系部分重叠关系重叠关系出现三种时候会导致需求描述致性现象发生说需求重叠现象出现需求致根原考虑需求描述重叠情况文提出相似度方法计算然语言需求描述两然语言需求描述相似度越高说明重叠概率越存需求致概率越种方法文模型检验提供定位策略
节然语言需求子句结点构建种需求子句模型图31示句子相似度算法表征句子间相似性处理程中节然语言描述需求划分需求子句(sentence)然需求子句进行分词处理程中统计需求子句中词语词频(F)词性(N)利相似度算法计算出需求子句相似度具相似度需求子句放组里中词频(F)表示需求子句中某词出现次数统计量初始值1着断切词累加词性(N)组枚举值取值范围分名词（n）动词（v）形容词（adj）副词（adv）数量词（nq）代词（pro）介词（pre）连接词（con）解决部分词语规范问题换义词
(T)表示需求领域某名词通规范法
图31需求子句相似度模型
算法31出需求子句相似度计算程相应算法伪代码表示：
算法31需求子句相似度算法
Input Requirement Description
Output Similar Sentence
begin
Requirement Description(DS) ∉∅需求描述
Requirement Sentence(RS) ∈ ∅需求子句空
n* RS ← DS 需求描述转换n需求子句
i0j0设置变量ij初始化
forall the Ai∈ RSi do
n*Ai*Fi+n*Ai*N RSi divided 遍历子句子句进行分词处理划分成词频词性
newAi n*Ai *Fi +n*Ai*N+T 出现规范词专业词换
foralltheFiinnewAndo 重复遍历分词处理结果
ji
forallthe Fj in newAn2 do 意两间做较
ji
if(SimFreq(FjnewAn2)>05) 相似度05
then
add Fj∪newAn2 join Similar Sentence[ ]相似放组
n++ 继续循环
i++ 继续循环
end
需求描述里关键词信息够直观反应关键词文中重程度[24]某需求关键词文档中出现次数越说明关键词整文档中占例越占权重越高求两需求子句间相似度文鉴传统VSM[25]计算方法基量空间模型算法两量夹角表示出两量间相似度程中词成维度词频率成值量样两需求子句相似度句子词频率构成空间计算程公式3(1)示
公式3(1)
SimFreqFSF·SF×S
i1n(xi×yi )i1nxi2×i1nyi2
通公式3(1)计算两需求子句间相似度 中FS分两需求子句量形式xiyi量值
文首先根文提需求子句进行分词处理然进行词频计算形成特征量样两需求子句种非结构化数抽象量表现形式 便然语言表述需求问题转换成数学量夹角问题时需求关键词词频数量定程度够反映重程度需求描述文规模较时方法效快速找出需求相似方解决需求致提供定位策略示例
程示：
假设两需求描述子句表31示
表31需求相似度计算示例
编号
然语言描述
1
客钮电梯响应请求运行
2
客钮电梯响应请求运行
需求子句分词处理：
需求子句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需求子句特征量{1110111110}B需求子句特征量 {1101111101}
根公式31计算两需求子句相似度
SimFreqFSF×SF×S 23
中
F1110111110S{1101111101}
F×S6
F12+12+12+02+12+12+12+12+12+024
S12+12+02+12+12+12+12+12+02+124
计算结果23说明需求描述中两需求子句较相似根需求重叠理需求越相似方存致概率越首先定位两句需求描述位置两句基础结合文进行建模分析
312 动机模型
动机限状态机(FSM)数学模型 表示限状态状态间转移动作等行模型限状态机五元组：（ΣQΔq0F）
中：
Σ限字母表
Q限状态集合
Δ⊆Q×Σ→Q代表变迁关系
q0⊆Q起始状态
F⊆Q终止状态集合
图32动机模型
动机发系统交互式系统建模简单动机模型图32示q0表示系统起始状态q2q3属终止状态Fq1程状态属状态集合Q余状态变迁状态Q字母表Σ表示建模系统状态集合
313然语言提取动机模型
节中需求定义组动作序列控制状态变迁关系[26]刻画动机模型具分解规范然语言指定事件(Event)状态(State)动作列表(Action)组成结构种类型规范结构描述动作事件驱动状态改变结构中Event指导致系统表现出预测行动作程State表示某时刻系统某行Action表示系统操作列表会导致状态改变简单状态变迁图图33示
图33Event事件状态变迁图
节结合方法BDL方法Error Reference source not found模型进行改进改进表述电梯模型描述行表2示
表2 具分解规范然语言分解程
FSM中元素
元素
分类
提取
源
Event
Subject
电梯
n
Behavior
空闲升
v adv
q0QF
State
State
载升
v adv
Agent
客
n．
ΔΣ
Action
Activity
v
Object
钮
n．
表格分解规范时需施加规中Action中Agent表示代理参动作中系统交互系统行执行者Activity者系统执行操作会导致状态改变行身Object受原子动作中代理资源作影响系统行执行者电梯模型中Action导致整系统改变开始时电梯楼空闲状态客进入电梯电梯空闲变载等行指令客钮时客作代理操系统导致系统状态改变电梯载状态变升状态根文提表格具分解规范然语言描述需求分解成动机模型图34示
图34电梯空闲事件动机模型
图描述然语言渡动机模型例子图中出整
Action行导致系统状态变迁符合BDL中描述行执行者软件功执行者实施操作程
32 基模型检验需求致
模型检测种基状态搜索形式化验证技术采动化技术遍历状态空间检查遍历状态空间否满足提出性质规约果发现预期性质致方会动定位错误位置模型检测项技术已成功应计算机硬件通信协议控制系统安全认证灯方面模型检验方法优点模型检验方法动化方法检测程较快提供属性规约模型检测工具动出属性规约致方通常说反例说明什满足方便查找检测需求分析设计中缺陷
模型检验早ClarkeEmersonQuielleSikakis针时态逻辑实际验证算法时提出目前系统安全性致性方面应广[27]模型检验种动验证系统模型否具特定性质方法简单说先系统建模限状态转移系统利时态逻辑描述验证规范整系统行空间进行动化遍历搜索定理证明步步展开严格证明推导模型检验具动化高效化特点
模型检测般包含三步骤系统建模性质描述性质验证
系统建模（modeling）：模型检验方法形式化方法首先需测系统进行形式化测系统中提取出Kripke结构者穷状态变迁系统结构中增加初始状态集终止状态集通常需建模时候利抽象技术进行剪枝减少模型状态爆炸问题
性质描述（specification）：通常建立系统总期该系统满足定性质安全性致性等性质描述已建立模型通常采模态逻辑时态逻辑公式动机形式表示性质称属性规约
性质验证（verification）：性质验证工作里利现模型检验工具属性规约动验证肯定者否定结果肯定表示属性规约符合开始预期说明性质验证否定表示属性规约符合预期出反例会产生错误路径帮助分析者设计者踪发生源
模型检验中系统状态变换等价变量值变化变量值改变体现状态迁移利状态间约束关系状态转移关联关系构成动机模型状态图[29]模型检验中文动机模型系统检测性质种方式表示检验程图35示
文需求描述系统模型动机图转化模型检验问题然语言描述需求问题转换模型检验中状态达存条路径等类似性质进行验证[30]
图35模型检验程
通建立测系统状态行模型CTL时态逻辑描述系统验证性质模型检验工具NuSMV检测终出条反例反例出现首先表明性质规约验证模型次反例出现加模型理解发现模型足基增加模型验证部分包括达性前致性陷阱性质验证中达性表述次状态变换中总少存条路径达目标状态前致性表述果某状态S1出现该系统模型续变换中定够出现预见状态S2例事件S1表示电梯系统启动事件S2表示客行钮事件S3表示电梯达目标楼层事件S1事件S2满足前致性陷阱性质描述某性质进行取反操作模型检验工具进行检测通检测性质出预期致方通产生反例帮助构建更完整需求模型
321 模型检验相关定义
定义：Kripke结构：令AP原子命题集合APKripke结构M三元组M(SRL)中S状态限集合R完全变迁关系L标记函数标记该状态真原子命题集合
Kripke结构图中圆圈表示事件弧线表示事件关
系标记函数圆圈图36示
图36 Kripke结构
CTL*种离散分支时间命题时态逻辑系统状态变化性表示树状结构CTL*公式原子命题布尔运算符时态算子路径量词构成CTL*公式两种类型：状态公式路径公式路径量词作表
述计算树逻辑结构AE两种构成
A表示前开始未路径符合某性质E表示前开始未少
条路径符合性质
时态算子5基运算符直观意义：
X(Next)说明某状态起始路径第二状态开始性质满足
F(Finally)刻画路径中某状态开始终性质满足
G(Global)说明性质路径状态满足
U(Until)表示状态前路径状态第性质满足
R(Release)表示前状态开始满足第性质状态结束第二性质
直保持成立
总根语法规CTL*状态公式集合描述反应式系统状态间转换序列形式化方法
定义2：计算树逻辑（computation tree logic）CTLCTL*子逻辑限制时态算子XFGUR必须前面加路径量词
定义3线性时态逻辑LTL：LTLCTL*子逻辑公式具形式Af中
f路径公式包含f里子状态公式仅仅原子命题
区：
图 37状态迁移系统
CTLLTL两系统例考虑图37状态迁移系统T：
显然T⊨FGp考虑路径ppppppp…该路径意节点AGp均成立T⊭AFAGp两性质样存状态转移中公式
成立成立描述非性质CTL*逻辑CTLLTL组合逻辑模型检验中常运
322模型检验实现
文简单例子说明模型检验算法例：房间加热器处四种状态中：Idle——空闲状态End——结束Heat——开始加热达某温度Warning——系统警告图38出房间加热器Kripke结构清楚起见状态该状态真原子命题该状态假原子命题否定形式标记出带箭头弧标记表示引起状态变迁动作名称
根图描述结构提出性质规约CTL公式描述：AG(Idle→AFIdle)该公式等价EF(IdleEGHeat)满足原子公式状态集合开始标记进复杂子公式令S(g)表示子公式g标记状态集合
S(Idle){2567}
S(Idle){12356}
计算S(EGIdle)首选出S’S(Idle)中非强联通分量集合SCC{{1235}}续步骤求EGHeat标记状态集合SCC中元素集初始时
T{1235}S’中没状态着S’中条路径达T中意状态计算中止
S(EGIdle){1235}
接计算S(IdleEGIdle){25}
计算S(EF(IdleEGIdle))时首先令TS(Idle
EGIdle)接着变迁关系逆关系标记满足公式状态
S(EF(IdleEGIdle){1234567}
S(EF(IdleEG Idle))
结果集合中没包含初始状态1出结：Kripke结构描述系统满足定性质规约
图38房间加热器Kripke结构
323 模型转换
采模型检验方法需测系统进行建模分析时序逻辑描述系统结构性质利模型部状态迁移关系验证整模型部某特定性质否正确文模型检验中SMV语言描述描述测系统CTL时态逻辑描述系统
性质模型部中系统状态达性进行分析
文提动机图提取状态元素转换成SMV模型供模型检验工具识SMV模型包含变量声明模块VARIVAR关键字定义模块MOUDE
ASSIGN模块定义系统初始状态INIT定义系统初始状态变量
值应转换规表32示
表32 动机图中元素SMV应关系
图中元素
SMV模型
说明
State
VARIVAR
变量声明状态集合
（源状态初始状态
目标状态）
ASSIGN(init)
定义约束集合
Event
Next
表示状态改名前状态收题代理影响准备迁移状态
Action
case…esac
系统状态变量受触发引起确定状态
表32描述文中动机图SMV语法表达出示
MOUDULE main
VAR
state：{IDLEUPDOWN}
button_F1boolean
ASSIGN
init(state)IDLE
init(button_F1)false
next(state)case
stateIDLE&button_F1UP
esac
出提取出图中元素应关系文提动机模型逐步转换成模型检验工具识SMV模型
324反例作
节典山羊河问题说明模型检验反例应问题描述：带着狼山羊白菜条河左岸条船正装三者行物带岸次带样东西摆渡河
狼羊留岸顾狼会羊吃掉样羊白菜岸顾羊会吃白菜中MGCWEmpty表示初始状态—左边符号表示应符号左岸—右边服务表述应符号右岸
M表示G表示羊goatC表示白菜CabbageW表示狼wolf
箭头表示表示次船运输物品种类详细描述参见附录1
图39 农夫河问题限状态机
安全河条件
TLSPEC
E [( ((goatwolf)> (goatferrymen)) & ((goatcabbage)>(goatferrymen)))U ((cabbageTRUE)& (goatTRUE) & (wolfTRUE) &(ferrymenTRUE))]
图310 模型检验正例验证
验证条件图310示显示true说明提出安全河性质规约建立模型说正确模型检验工具NuSMV会提供符合性质例子反例反例安全河条件取反
TLSPEC
E [( ((goatwolf)> (goatferrymen)) & ((goatcabbage)>(goatferrymen)))U ((cabbageTRUE)& (goatTRUE) & (wolfTRUE) &(ferrymenTRUE))]
表示存样条路径然交模型检验工具NuSMV验证验证结果图311示结果显示出性质规约false出条反例反例出现说明出现属性规约致方直接出条路径
图311 模型检验反例验证
33 结
节模型检验研究容通然语言相似度算法模型检验提供定位策略然语言描述中提取出动机模型进模型转换方法变成模型检验工具够识语言通样例说明模型检验工作原理说明模型检验反例作
第四章 需求突消解研究实现
章中模型检验然语言相结合方法研究需求致问题需求分析程者系统升级增加新功等导致需求致问题发生应该消掉发生需求致章需求突消解问题章首先突需求进行分类分解成功性需求非功性需求针两种类型需求突采消解方式功性需求采关联度方法进行消解非功性需求鉴济学中生产理成分析法提出代价权衡策略综合考虑非功需求达消解突目
41 概述
针型软件复杂系统开发获取更加全面需求防止需求信息遗漏需视点利益相关者（stakeholder）角度进行考虑分析中视点利益相关者需求避免存突需求突消解成需求分析中法回避重问题种方法消解掉需求描述中突
突消解问题般需求优先级权重两角度分析需求优先级权重需求优先级解决需求突问题时般结合具体方法层次分析法（Theanalytichierarchy process）简称AHP基思路建立系统层次结构模型关某项需求素属性分解成目标层指标层方案层然通构造矩阵判断矩阵中某元素标度分计算单次组合权量决定出元素优先级高元素优先级低外AHP方法进行组合做改进方法基ISM（InterpretativeStructuralModelMothod）AHP方法相结合基SAHP方法基Topsis（Technique for Order Preference by Similarity to an Ideal Solution ）AHP结合方法等类方法确定优先级方法KNAO模型KANO模型户需求分基型期型兴奋型差异型反型分析户需求户满意度影响体现户需求满足程度户满意间非线性关系部分优先级方法较单缺乏动态调整决策机制种解决突方法确定需求权重权重衡量总体中单位标志值总体中作数值表示某项指标系统中重程度表示指标项变情况指标项变化结果影响权重赋值方法常见三类：观赋权法客观赋权法组合赋权法中观赋权法通常专家调查法（Delphi法）层次分析法（AHP
法）二项系数法客观赋权法包括成分分析法熵值法目标规划法离差方差法等客观赋权法结合观客观思想客观赋权法包括折衷系数综合权重法线性加权单目标优化方法熵系数综合集成法外权值确定属性决策方法例DEMATEL方法C2R方法等属性决策方法通常结合需求优先级综合考虑权重问题
突stakeholder角度分析分业务突目标突情感突节指目标类突目标类突指系统需求般包含功性需求非功功性需求中功性需求求规定开发员必须产品中实现软件功户利功完成务满足业务需求系统中必须具备功软件非功需求称质量需求者质量属性实际软件属性者功需求约束非功需求软件产品满足户业务需求必须具功性需求外特性影响着产品否够持续高效提供服务非功性需求非功性需求重功性需求描述系统想完成功务非功性需求通常描述软件需满足某属性程度非功需求难量化手段表示满足需受时间成风险等种素影响
42 功性需求突消解
421 需求关联性致化程度
定义：需求关联性：基文然语言模型划分划分需求元素间否联系情况判断两者需求元素间否关联性
定义：需求关联度：需求关联度L针需求原集A需求突集B例关系公式1示
LiA∩BiA 公式4(1)
中：A需求原集文提出然语言分解需求集
B突集两部分部分原需求描述中突部分部分升级者增加新功导致原需求突部分
Bi突集中具体某突Bi⊂B
图41需求关联度
422 基需求关联度突消解
针功性需求间突节提出基需求关联度消解方法针复杂系统建模时消解流程概括：
（1）结合第三章划分成需求子句提取需求原集A
（2）根模型检验结果提取出两具突集BiBj
（3）根公式4(1)计算出突集BiBj需求原集A关联度
（4）分析较两突需求元素间关联度关联度更低
需求进行精化者舍弃
功性需求突消解中需求关联度重判断相直接根需求优先级方法需求关联度综合考虑需求元素间联系系统
状态图分解图42示
图中需求分解成干子需求子需求刻画成状态模式出确定系统说状态变迁关系应该唯确定现假设突需求集B加入需求原集A中新需求q10原集中q3突会引起系统确定等问题提取出q3需求图43示突集B需求原集存关联性示意图44示出突集B中包含元素中需求原集重叠重叠部分取出进行发现q3需求需求原
集4关联q10需求原集3关联关关联
图42 系统需求分解
根节式4(1)出q3需求关联度 Lq3A∩BiA41040q10需求关联度Lq3A∩BiA31030根需求关联度理应该q10需求进行舍弃者精化
图43 突集提取
图44新突集
43非功性需求消解
431 代价权衡分析
文针非功需求难量化问题鉴济学理改进非功性权衡代价分析方法改进目保证两非功需求发生突时总代价损失整体保证软件质量软件非功需求突质利益相关者策略执行避免引入果策略执行会导致突情况提升某非功性需求必须执行特定策略例软件会安全性响应时间作非功需求需考虑素情景中考虑安全性
强制实施密码策略增加密码复杂度认证程序程中复杂度增加势必导致响应时间增加说针两非功性需求提升安全性时必然会损害响应时间者说提高响应时间代价降低系统安全性必须找非功需求间佳权衡点系统整体代价损失
文鉴济学中代价权衡理济学中生产理需求工程相结合综合权衡非功性代价代价损失更表达非功需求文讲非功需求分两类类度量策略类度量策略
432 度量策略
度量策略通常现量化方式非功需求进行量化处理说难采数学方法非功需求进行代价权衡例Stacey Matrx模型
中图45示
图45 STACEY矩阵模型
问题没确定时果关系明显垂直（Y）轴团队团队组织间问题决策达成致程度频谱端果问题存高度确定性致性决策容易领域称（理性简单）传统方法（瀑布）方法效范围没该问题达成致意见没确定果关系区计划通常慷慨混乱政府状态盛行区极端稳定稳定性逆转极端应该避免混沌区域频谱两极端间存称复杂区区域里传统方法情感复杂区域中系统预测区域提前指定产品详细信息准确度方面详细信息达成致条件需户开发员间协作环境佳方法敏捷需高度创造力创新产生解决方案敏捷开发中软件项目构建切分成子项目子项目成果测试具备集成运行特征简单说敏捷开发追求前期完美设计完美编码力求短周期开发出产品核心功早发布出版然续生产周期新需求断迭代升级完善产品敏捷开发中强调作单功入手遇需求突时难
权衡量化针度量策略基验方法进行突消解基验需求突消解：
（1）型团队开始发挥作单位组建
（2）发现突时先进行部讨果员部讨解决突案例放策略库中备
（3）果部讨没解决问题进入调解程序 调解程序目员开发验进行决策解决策略放策略库中
433 度量策略
度量非功需求突采济学中生产理非功需求进行权衡分析例信软件中认果软件行总预期相致称信信软件应该软件结果预期够预期解决采取度量策略
定义1：策略代价Ps：策略S代价Ps实施策略S引发非功需求集合R策略代价P成PM函数关系中
（1）S满足非功需求必须实施某策略
（2）R策略S引发突非功需求集合∀r∈R 具体非功需求
（3）PM策略S时产生工作量成代价
定义2：成代价PM：PM策略S产生成公式：
PMA×（SIZE）E×i1nEMi(i123…17)
中：
（1）PM总工作量策略S时成
（2）A生产率常数COCOMOⅡ中A通常取值298
（3）SIZE估算软件功单元代码行数
（4）E指数子反应项目规模济性
（5）EMi成驱动子获取影响完成项目需工作量软件开发特征成驱动子模型系数COCOMOⅡ中定义17成驱动子
中指数子E计算公式：
E091+001j15SFj
式中j123…5指数子E体现5例子SFj作说明规模软件项目具相规模济济性SFj 例子项目工作量指数变化生产率变化重成规模子登记变动范围低极高
济学生产理中生产函数Q劳动L资K函数关系
Qf(LK)生产理描述两非功需求突时LK两突素r1r2Q产生策略代价度量P然度量值构造代价线图43示PM两突素中中变量产生成代价线图44
示n1n2分指策略S实施产生需权衡非功需求突策略S实施时r1度量值x1时r2应度量值y1r1取x2时r2取y2次类推产生策略S策略代价线P成代价线PMn1变量时r1非功需求取值x1确定时产生成代价y1r1非功需求取值x2时确定成代价y2类推产生策略成代价曲线PM策略代价线Pxiyi决定代价点描述策略S实施非功需求r1r2间反应权衡关系策略成线PM反应策略S实施阶段成代价权衡关系视r1r2间弹性代关系图4x见果r1取高点x4n2取低点y4类似r1降低求时取x3时n2达y4高y3r1r2间视消彼长代关系关系描述非功需求间相互代代价成代价线图x示需求r1取值x1时产生成y1需求r1取值x2时产生成y2
图43策略代价
图44成代价
优权衡代价决策图43出某策略实施非功性需求增强会导致非功需求降低者减弱动态程基思想需非功需求增加必约束样找利益相关者优权衡代价 图43示策略代价增加两约束条件利益相关者非功需求优先级约束便某非功需求低约束基线优先级约束线利益相关者非功需求间突权衡关系图45示干条直线表示非功需求
优先级约束斜率r1r2说明两非功需求r1优先级r2高利益相关者更需r1效率R1R2说明两非功需求R1优先级R2低利益相关者更需R2低约束基线利益相关者某项非功需求低限制图4x中阴影部分非功需求中低限制容分享网站中显示容量响应时间突量项调查显示户愿意等6秒超6秒会失耐心样系统说响应时间非功需求低约束基线6秒样容量低约束
基两约束条件出约束条件优策略代价图46阴影部分示R1min表示非功需求R1低约束基线R2min表示非功需求R2低约束基线(R1R2)1(R1R2)2分表示非功需求R1R2两种优先级两非功需求R1R2说首先排范围策略X1剩余两策略X2X3优策略需继续引入成代价线PM图47示图中出根前文R1PM关系成代价线策略代价线融合坐标系中出成代价线阴影部分交点PM1表示需求R1成变化关系需考虑X2X3应Y2Y3PM1绝距离保留距离成代价曲线点PM1策略X3非功需求R1R2代价权衡策略已出
图45约束策略
图46基约束策略代价
图47优权衡代价
44 结
节建立发现需求突基础需求突进行分类功性需求采需求关联度方法进行消解非功性需求采代价权衡策略进行消解终实现需求致性
第五章 案例分析
完整系统模型庞复杂文通精简电梯模型[31]Error Reference source not found选取电梯模型述研究方法进行验证
51电梯模型描述建模
电梯功分行行报警显示开关门电话机报警等该模型部分然语言描述：
行：电梯初态停楼客行钮电梯响应客请求运行达客楼层开电梯门客进入电梯电梯检测客重量否超标果超重报警否关闭电梯门然客电梯目标楼层电梯系统判断目标楼层前楼层电梯运行达客开电梯门客离开电梯停该楼层重新处静止状态
行：客行钮电梯响应客请求运行达客楼层开电梯门客进入电梯电梯检测客重量否超标果超重报警否关闭电梯门然客电梯目标楼层电梯系统判定目标楼层前楼层电梯运行达客开电梯门客离开电梯停该楼层重新处静止状态
报警：客电梯报警钮者电梯出现障紧急停止报警
显示：显示面板会直显示电梯状态(运行状态前楼层)果发生障者客报警钮显示面板显示
开关门：客电梯外开关门钮电梯响应开关闭电梯门
然语言21节中相似度算法进行分析描述行行需求描述相似度约095说明两需求描述存重叠方定位两需求描述位置位置开始进行建模分析避免遇规模需求描述法快速找潜致需求情况发现具相似性需求描述根
312节中分解规范提取动机模型分解程表51示
表51 分词提取结果
项
需求描述
根分解规范提取
应元素
#1
电梯初停楼
停（电梯楼）
State
#2
客行钮
（客钮）
Action
#3
电梯响应客请求运行
（电梯客）
State
#4
客达楼层客进入电梯
达进入（客楼层电梯）
Action
#5
电梯检测重量否超标
检测（电梯超标）
Action
#6
达客开电梯门客离开
开离开（客电梯门）
Action
#7
客行钮
（客钮）
Action
#8
电梯响应客请求运行
（电梯客）
State
#9
…
…
…
…
…
…
…
根表格提示结合文补充必节点生成动机模型便观察转换成动机形式图52示根文表32方法结合图34简单生成电梯系统SMV模型该模型表述示：（篇幅限选取部分关键代码）
图52 电梯模型模型描述
MODULE main
VAR
state{UpDownHoldIdleWaitingWarningStopFault}
position{F1F2F3}
button_F1boolean
……
door_F1{OpeningOpenedClosingClosed}
door_F2{OpeningOpenedClosingClosed}
door_F3{OpeningOpenedClosingClosed}
passenger{NoneInOut}
weight{NoneNormalOverload}
arrivedboolean
emergencyboolean
ASSIGN
init(state) Idle
init(passenger)None
……
next(position)case
positionF1&stateUpF2
positionF2&stateUpF3
positionF2&stateDownF1
positionF3&stateDownF2
door_F1Closed&(button_F1)&positionF1
&stateUpF2
door_F3Closed&(button_F3)&positionF3
&stateDownF2
door_F2Closed&(button_F2)&positionF2
&stateUpF3
door_F2Closed&(button_F2)&positionF2
&stateDownF1
TRUEposition
esac
next(state) case
stateIdle&(door_F1Opening&passengerIn
&weightNormal) Waiting
stateIdle&(passengerIn&weightOverload) Warning
stateWaiting&(passengerIn&weightNormal&(button_F2|button_F3)) Up
stateWaiting&(passengerIn&weightNormal& button_F1|button_F2) Down
stateWaiting&emergencyStop
……
esac
述代码电梯模型描述代码中处省略部分中第处button_F2button_F3
request_F1request_F2request_F3数类型boolean型第二处weightbutton_F1button_F2
button_F3door_F1door_F2door_F3arrived初始化描述第三处省略部分电梯状态state钮状态door_F1door_F2door_F3条件选择结构
52 属性规约提取验证
属性规约系统运行程中必须满足规范保证系统致性安全性针文提模型方面进行验证
(1)安全性系统运行首先保证安全性验证：未意时刻电梯系统会客困电梯中
(2)前致性电梯系统运行需满足前致性验证电梯初始状态空闲状态时客进入时未某状态会超重导致电梯报警
(3)达性验证电梯系统动机模型否达图中描述状态
(4)陷阱性质根动机图中描述状态变迁增加条某行需求描述相似变迁进行取反操作观察模型检验否检测出相似致行验证客楼行钮电梯会出现行状态检测结果表52示
表52 性质验证结果
验证性质
CTL性质描述
验证结果
安全性
SPEC AF (passengerIn>AG passengerOut)
true
前致性
SPEC AF(stateIdle&passengerIn>EF state Warning)
true
达性
SPEC AF(stateIdle > AG stateWarning)
false
陷阱性质
SPEC AG (position F1&state Up >AX position F2)
false
表属性规约性表述图53 54NuSMV验证结果面NuSMV验证结果进行分析
(1)安全性CTL描述正常情况中客困电梯中结果显示true证明该电梯模型具安全性质
(2) 前致性结果显示true表示模型转换程中状态前变迁关系正确说明文转换规然语言转换动机模型信
(3)达性表述需求定义功判断整系统中某状态否达结果显示false反例出现说明预期致行帮助构建更完善需求模型
(4)陷阱性质结果显示false表示够检测出需求描述致行反例出现首先说明够检测出描述致行次根反例提供路径信息进步分析模型联系帮助构建更全面需求模型
图 53验证结果1
图54验证结果2
事实变换越面状态越时需遍历路径越仅工作量容易忽略状态变换模型检验动遍历状态遇预期性质致情况时动生成条反例通分析反例出通然语言建立模型足处供继续分析完善模型方面模型状态空间变足够时工方法已法解决状态遍历问题动者半动方法模型检验优势
53 需求突消解
51节中出电梯系统模型基础假设电梯系统时需求改变增加条新需求全动化更加智化增加电梯操作均通智声控设备完成
原文中加入新需求增加SMV描述：
autostate{upDownHoldStop}
next(autostate)case
autostateup&(arrived&door_F1Opening|door_F2Opening|door_F3Opening)&passengerOut)Hold
autostateDown&(arrived&(door_F1Opening|door_F2Opening|door_F3Opening)&passengerOut)Hold
autostateHold&emergencyStop
TRUE autostate
esac
提出属性规约：
SPEC AF(state Stop & handleFALSE&emergencyTRUE > EG state Idle )
通模型检验工具出条反例图55示
图55模型检验结果
反例出条路径分析路径出出repairhandle状态均标记false关联状态stopfault 解释动化操作法处理电梯状态状态根
423节提出需求关联度方法autostate状态关联4原集8状态根文公式4(1)关联度12stopfault关联状态6根公式4(1)关联度23根需求关联度方法应该autosate需求进行重新考虑考虑删者精化
54结
节电梯系统实例基础文提出电梯系统需求进行致性验证验证文提方法行性外需求突消解类问题电梯系统中文提需求突消解方法进行分类相应方法进行消解达预期目标
第六章 总结展
61 总结
文研究种基模型检验需求致需求突消解方法通分析目前现需求致方法提出新基模型检验然语言相结合需求致研究框架提出模型框架进行致性验证外需求突消解问题提出需求关联度方法解决功性需求突非功性需求提出权衡策略解决突度量非功需求基验方法解决突度量方法代价权衡策略方法综合较出优代价策略文通电梯系统实例验证行性分析效验证
通文研究完成目标容：
（1） 分析现需求致建模方法应提出新基模型检验需求致研究框架
（2） 然语言进行分解提取利相似度算法计算出然语言描述相似性解决模型检验定位问题
（3） 提出套完整模型提取转换方法基然语言描述进行分类提取转换成动机模型然动机模型转换成模型检验够动识语言模型检验工具进行动识
（4） 突消解文出两种类突消解方法功性需求突消解问题需求关联度思想关联度低进行舍弃者精华消解掉需求突
（5） 非功需求突提出代价权衡策略进行分析综合考虑策略代价成代价济学生产理进行分析考虑消解非功需求突
（6） 结合电梯模型实际案例证实基模型检验需求致模型效意义电梯模型基础实现文提致性验证需求突处理问题验证文研究行性效性
62 展
文基模型检验需求致问题研究需求突消解然取定成果然存定局限性需进步进行研究：
（1） 文提出基模型检验需求致问题研究文中涉然语言相应模型基础进行分析步应该继续完善改进模型具更高普遍性
（2） 文需求突消解较合理方法发生需求突进行分类采方法进行消解考虑方面够例文没详细说明模型检验然语言功性需求非功性需求分类步考虑然语言处理中引入属性分解模型检验中引入时间动机等概念更表示非功性需求外某度量非功需求约束低约束高约束步工作约束进行更加深刻研究
（3） 文电梯实例相较简单没包含更加复杂系统功步工作研究更加复杂系统文研究容应复杂实际项目中更验证方法行性
参考文献
[1] Leffingwell D Widrig D Management Software Requirements：A Unified Approach[M] New JerseyAddisonWesley 2000 6572
[2] Pandey D Suman U Ramani A K An effective requirement engineering process model for software development and requirements management[C]2010 International Conference on Advances in Recent Technologies in Communication and Computing IEEE 2010287291
[3] 毋国庆等软件需求工程[M]北京机械工业出版社20088
[4] urkiewica J Nawrocki J Ochodek M et alHAZOPbased identification of events in use cases[J] Empirical Software Engineering 201520(1)82109
[5] Nuseibeh B Easterbrook S Russo A Leveraging inconsistency in software development[J] Computer 2000 33(4) 2429
[6] Walter B Hammes J Piechotta M et al A Formalization Method to Process Structured Natural Language to Logic Expressions to Detect Redundant Specification and Test Statements[C] Requirements Engineering Conference IEEE 2017(38) 263272
[7] Heitmeyer C L Jeffords R D Labaw B G Automated consistency checking of requirements specifications[J] Acm Transactions on Software Engineering & Methodology 1996 5(3)231261
[8] Van Lamsweerde A Letier E Handling obstacles in goaloriented requirements engineering[J] IEEE Transactions on Software Engineering 2000 26(10) 9781005
[9] Glinz M A lightweight approach to consistency of scenarios and class models[C] Requirements Engineering 2000 Proceedings 4th International Conference on 20004958
[10] K Lee and S Lee Applying Game Theoretic Approach to GoalDriven Requirements TradeOff Analysis for SelfAdaptation 2015 IEEE 39th Annual Computer Software and Applications Conference Taichung 2015 pp 330335
[11] Applying fuzzy preference relation for requirements prioritization in goal oriented requirements elicitation process [J] International Journal of System Assurance Engineering and Management 2014 5(4) 711723
[12] Suhaib M Ohnishi A Potential Conflicts Identification among Sub Goals in Goal Oriented Requirement Analysis Using Matrix[J] International Journal of Progressive Sciences and Technologies (IJPSAT) 2018 10(2)
[13] Gulzar K Sang J Ramzan M et al Fuzzy approach to prioritize usability requirements conflicts An experimental evaluation[J] IEEE Access 2017 5 1357013577
[14] Hassine J Amyot D An empirical approach toward the resolution of conflicts in goaloriented models[J] Software & Systems Modeling 2017 16(1) 279306
[15] Zhang W Deng Y Combining conflicting evidence using the DEMATEL method[J] Soft computing 2019 23(17) 82078216
[16] 朱雪峰 金芝 关软件需求中致性理[J] 软件学报 2005(07)2838
[17] 张建 吴俊 方景龙 模型动转换致性验证方法[J] 计算机工程设计 2017(9)
[18] 周宇 黄延凯 et al 种开放环境软件线演化致性验证方法[J] 软件学报 2015 26(4)747759
[19] 张璇 王旭 李彤 et al 软件非功需求权衡代价[J] 软件学报 2017(5)
[20] 李瑞轩 鲁剑锋 李添翼 et al 种访问控制策略非致性突消解方法[J] 计算机学报 2013(06)88101
[21] 湛浩旻 印桂生 赵蕴龙 基ISMAHP组合需求优先级排序方法Method of Prioritizing Requirements Based on the Combination of ISM and AHP[J] 计算机科学 040(3)225227243
[22] 王守堰 金英 张晶 Nash equilibrium strategy choosing method for resolving inconsistencies of requirements解决需求致纳什均衡策略选取方法[J] 计算机应研究 2015 000(002)466469474
[23] Spanoudakis G Finkelstein A Till D Overlaps in Requirements Engineering[J] Automated Software Engineering 1999 6(2)171198
[24] Xu Haoguang Wang Ning Liu Jiaming et al Comprehensive Computation Algorithm of Similarity for Natural Language Retrieval [J] Computer system application 2017 26(6)170175
[25] Cong Y Chan Y B Ragan M A A novel alignmentfree method for detection of lateral genetic transfer based on TFIDF[J]Scientific Reports 2016 6(30308)113
[26] Rui S Deming Z Translating software requirement from natural language to automaton[C]
International Conference on Mechatronic Sciences IEEE 201424562459
[27] Jin Huan Huang Qing Requirement formal modeling and quality characteristics verification based on scene behavior [J] Computer Applied Research 2016 33(5)13841398
[28] Huang Wudan Chen Zhe Model Checking of Security Issuses in Border Gateway Protocol [J] Journal of Chinese Computer Systems
201738(6)11881191
[29] Li Jiali Chen Yongle Li Zhi et al RTSP protocol vulnerability mining based on protocol state graph traversal [J] Computer Science 2018 45 (9) 171176
[30] He Yang Hong Mei Qi Linying et al Functional test case generation method based on model checking tool NuSMV [J] Computer application 2015 (A02) 155159
[31] Li Xin ASchedulingStrategy of TargetLayerReservationElevatorGroupBasedonModelCheckingMethod [D]NanchangJiangxi University of Finance and Economics 20181154
致 谢
研究生生活接尾声三年时间里导师xxx教授学生活中种指导帮助xxx老师步步引导做研究选择文献样精读文献样泛读文献引导中发现问题进步指引提出解决办法魏老师悉心指导完成篇文
做研究外导师教会做名研究生样更杜工研究生时代合理安排时间学余研究生生活证丰富彩教会处事道理工作学子中收益终身衷魏老师说声谢谢
完成该文程中师哥师姐帮助师哥师姐帮助查文献提供参考书籍分享验教训文撰写中少走弯路感谢帮助外研究生生活必少班学研究生生活变更意义
感谢直支持鼓励父母家培养父母付出遇什困难坚强盾希身体健康
感谢评阅位老师感谢位老师文提出宝贵意见指导谢谢
文档香网(httpswwwxiangdangnet)户传
《香当网》用户分享的内容，不代表《香当网》观点或立场，请自行判断内容的真实性和可靠性！
该内容是文档的文本内容，更好的格式请下载文档
