毕业设计：文献参考（3）
一、基本信息
- 标题：基于UML的系统需求形式化分析方法
- 来源：北京交通大学
- 作者：刘心钰
二、研究背景
Unified Modeling Language ( UML，建模语言或标准建模语言)始于1997年的一个OMG (Object Management Group，对象管理组织)标准，是一个支持模型化和软件系统开发的图形化语言，为软件开发的所有阶段提供模型化和可视化支持，包括由需求分析到规格，到构造和配置。UML允许添加类级和系统级约束，但其中并没有定义如何检查这些约束的正确性。大多数UML规范是描述性的，容易理解，但由于不是形式化的描述语一言缺乏精确的语义，这使得对其中的约束进行正确性检验十分的困难。为保证系统的正确性并降低其开发的成本和之后的运行风险，尽早对系统进行安全验证就显得尤为重要。特别是需求规范中如存有潜在缺陷，会对系统的开发过程带来重大的影响，如果在系统开发阶段不能及时发现，很可能会导致系统在运行阶段失效从而带来灾难性的后果。
本文主要探讨系统需求分析阶段的形式化分析方法，通过模型检测来验证UML规范的约束，并给出了一个实例的规范及转换验证UML规范的过程。通过对需求阶段实例进行分析得到需求的UML建模模型，选取模型中的类图、状态图和)I}序图，设计了将UML模型图例转换为SMV C Symbolic Model Verifier，符号模型检验器)描述的转换规则和对转换规则进行代码实现后的具体化工具，使得转换后的UML模型可以被符号模型检验器NuSMV ( New Symbolic Model Verifier,新型符号模型检验器)接受以验证系统的性能，并可查看到验证返回的反例和验证过程中检测到的错误和位置，为对其错误信息的分析和修改完善提供了方便。
最后，基于Enterprise Architect软件对需求进行建模，并在此环境中对实例进行测试和验证规则及实例的正确性。测试表明本文提出的方法可有效实现对根据需求进行分析进而得到的UML类图、状态图和顺序图进行的转换，并使转换实现自动化，使其更加方便的进行形式化验证。
三、具体内容
本文共分为以下几章：
第一章：引言。介绍了模型检测和建模的相关知识，阐述了形式化验证在建模和实例中的应用和在其中存在的一些问题，同时介绍了相关内容的研究现状和本论文的主要工作，最后介绍了本论文的港本结构。
第二章:面向需求分析的UML建模。主要介绍了需求分析的定义、对需求分析进行验证的原因，并给出需要对其进行研究的实例的问题描述和对其进行的建模。
第三章:面向NuSMV的UML语义转换。主要介绍了形式化方法，以及本文应用的验证工具一一一NuSMV和UML的语义转换，并给出从UML转换到SMV的转换规则。
第四章:语义转换的实现。主要介绍了使得语义得以转换的工具的设计和转换规则的代码实现。
第五章:基于NuSMV的属性验证。介绍了验证属性所需的CTL逻辑公式，同时详细分析了实例中所需验证的属性和通过验证得出的错误的分析。
第六章:总结与展望。首先对全篇论文所做的工作进行总结，阐述论文研究的意义，并指出一些不足之处和将来的改进。
四、参考文献
[1]刘心钰. 基于UML的系统需求形式化分析方法[D].北京交通大学,2015.