基于场景和属性的需求引出及形式化建模

论文摘要

场景是一种分析与验证需求的有效工具,因此基于场景的分析与设计受到广泛关注。场景提供预期系统的行为实例,也就是说场景中的交互行为一定是预期系统要出现的行为。一个场景一般情况下不能完整的描述整个系统的行为,所以基于单个场景构建的行为模型只是最终预期系统的一个下界。属性是描述系统行为必须要满足的一种状态说明,基于属性的构造的行为模型包含所有不违反属性的可能轨迹。因此基于属性的行为建模为预期系统提供了一个上界。如何基于场景构造预期系统的下界和基于属性构造预期系统的上界,以及在上界行为模型和下界行为模型之间得到最终的预期系统便是本文的研究重点。本文首要解决是如何进行基于场景和属性的需求引出。消息序列图（Message Sequence Charts, MSC）,一种场景的表示方法,用于描述场景中构件之间的通信、交互行为,因此本文首先介绍MSC的基本概念。3-值流体线性时序逻辑公式是一种描述系统属性的有效方法,因此在介绍3-值克莱尼逻辑（Kleene logic）和流体之后,文中给出了3-值流体线性时序逻辑公式的概念。然后通过一个论坛发帖系统的实例,根据场景的描述将需求引出,生成MSC图,然后又将需求形式化为属性描述。基于场景合成的标号迁移系统只能描述场景给出的行为,不能描述场景没有给出的可能行为。基于属性合成的标号迁移系统不能区分哪些是为了满足安全属性必须发生的行为和不违反安全属性的可能发生的行为。针对现有合成算法存在的问题,并在现有合成算法的基础上,我们给出了合成模态迁移系统的算法。在现有基于场景合成LTS算法的基础上,提出一个算法使得LTS变成MTS,得到一个预期系统必然行为的下界,同时合成的MTS模型可以表达除场景描述之外的可能行为。在基于属性合成LTS算法的基础上,提出了合成MTS的算法,得到预期系统的一个上界,合成的MTS模型可以区分必然行为和可能行为。最后通过合并操作将这两个MTS模型合并为一个MTS,该模型保留下界的必然行为和上界的可能行为。合并之后,系统行为可以进一步精化,模态迁移系统的精化不仅保留了初期的属性和场景,而且支持新的属性和场景的抽取。

论文目录

• 摘要
• ABSTRACT
• 目录
• 第1章 绪论
• 1.1 研究背景
• 1.1.1 需求工程的过程和定义
• 1.1.2 基于场景的需求工程
• 1.2 国内外研究现状
• 1.2.1 基于场景的需求工程的研究现状
• 1.2.2 形式化方法的研究现状
• 1.3 研究内容
• 1.4 论文结构
• 第2章 基于场景和属性的需求引出
• 2.1 引言
• 2.1.1 场景的基本概念
• 2.2 用于场景描述的MSC介绍
• 2.2.1 MSC的基本概念
• 2.2.2 MSC的主要元素
• 2.3 基于场景和属性的需求引出
• 2.3.1 3-值流体线性时序逻辑（3-value FLTL）
• 2.3.2 场景和属性的需求引出描述
• 2.4 本章小结
• 第3章 行为建模技术研究
• 3.1 研究背景
• 3.1.1 标号迁移系统的概念（LTS）
• 3.1.2 模态迁移系统的概念（MTS）
• 3.1.3 FLTL在迁移系统中的模拟和实现
• 3.2 现有模型存在的问题
• 3.3 基于属性的合成
• 3.3.1 基于属性的标号迁移系统的合成
• 3.3.2 基于属性的模态迁移系统的合成
• 3.4 基于场景的合成
• 3.4.1 基于场景的标号迁移系统的合成
• 3.4.2 基于场景的模态迁移系统的合成
• 3.5 基于属性和场景的合成
• 3.5.1 基于场景和属性的模态迁移系统的合成
• 3.6 本章小结
• 第4章 结束语
• 4.1 主要工作
• 4.2 未来工作
• 参考文献
• 致谢
• 攻读学位期间取得的研究成果