毕业设计：文献参考（5）
一、基本信息
- 标题：列控系统需求规范形式化建模与验证方法研究
- 来源：北京交通大学
- 作者：谢雨飞
二、研究背景
在传统的工作中，为了消除系统需求规范中可能存在的各种缺陷，都要在系统开发实现完成后，对系统的可靠性和安全性进行分析和度量，这种方法得到的结果一般比较精确。具体来说，传统的安全保证方法是“渗透与补丁”:通过仿真测试等多种手段，一旦发现对系统的渗透或识别出被利用的漏洞，就删除或修改它们。然而，对多数系统而言，这种方法并不理想。因为每一次利用新的漏洞进行渗透时，都可能在漏洞被弥补之前就己经造成了重大损失。创建和发布补丁不仅需要费用，而且有可能会失去用户的信任。另外，补丁本身同样可能存在安全威胁。更为重要的是，如果在此阶段才发现系统未满足可靠性要求，修改的代价将十分巨大，对需求错误的事后处理费用要比提早处理所需要的费用高近200倍。因此，一个有效的系统设计开发过程必须在早期阶段，系统部署或实现之前，就认真地考虑系统需求规范的可靠性和安全性问题，进行安全分析。这样能够指导系统开发过程，确保最终构造出来的系统满足可靠性要求。在系统开发早期对系统需求规范的可靠性和安全性进行分析，一方面能够帮助系统设计人员对现有的设计方案进行评估，以检验设计是否满足用户需求;另一方面也能帮助系统设计人员对各种设计决策进行比较，从而选择更优的设计方案。因此，在系统开发早期对系统需求规范的可靠性和安全性进行预测评估具有重要的意义。
对系统需求规范进行形式化建模与验证，可以有效解决规范的表意模糊和逻辑缺陷问题，并且能够在系统开发的初期对规范中的漏洞进行排查，从而减小系统维护的代价。
三、具体内容
针对列控系统需求规范建模与验证当前E1}待解决的一些问题，本文对规范建模、规范与模型的一致性分析，以及模型转换等相关内容进行了深入探讨。论文章节安排如下:
第一章:引言。阐述了论文研究的选题背景，提出需要解决的问题。简要地回顾了规范建模与验证方法的演化过程以及相关进展情况。针对当前研究存在的问题，指明了论文的意义和目的。
第二章:列控系统需求规范建模与验证研究现状。详细介绍国内外针对列控系统需求规范建模与验证的研究现状，归纳并总结它们运用的理论、方法和工具等。通过比较和分析当前的研究情况，了解目前规范建模与验证的发展趋势，指出当前研究存在的不足，明确论文需要解决的问题。
第三章:列控系统需求规范建模与验证方法。论述本文给出的改进型列控系统需求规范建模与验证方法及其实现方式。
第四章:基于扩展UML的列控系统需求规范建模与分析。提出用UML的扩展机制建立列控系统需求规范模型的方法，这种方法将系统的安全需求融入到模型中，通过模板的形式定义安全需求，增加模型的可重用性。根据列控系统需求规范的特点，建立了规范建模及模型检查规则，明确定义了规范片段的分类以及规范与模型的映射方法。
第五章:列控系统需求规范模型转换及规则证明。形式化定义了列控系统需求规范建模与验证中与模型转换相关的若干概念。给出一种基于模板的模型转换方法，并建立由UML模型转换成CSP模型的规则。讨论了模型转换过程中特性的保持性判据，提出了一种基于关系代数的模型转换规则的正确性和一致性证明方法。
第六章:软件工具的开发与案例分析。开发了一款规范建模与验证集成软件工具CTCS Tool，介绍了软件的功能和使用方法。以CTCS-3级列控系统需求规范
四、参考文献
[1]谢雨飞. 列控系统需求规范形式化建模与验证方法研究[D].北京交通大学,2012.