神经内分泌复杂系统的形式化研究

摘要

目前软件工业界面临着产品功能越来越复杂的压力。软件工程的一个主要目标就是在软件复杂性增加的情况下仍能构造正确可靠的系统，达到这一目标的途径之一是形式化方法。形式化方法是一种用于规范、设计和验证计算机系统的软件开发方法，它建立在严格的数学基础之上，使开发的模型得到证明，可以有效提高软件的可靠性。 需求获取是软件开发过程中最为困难也是最为重要的部分。已有的需求获取方法例如访谈法、问卷法、观察法和用户资料研究法等，这些都是简单的方法，但这些方法的效果与项目的风险是成反比的。对于一般系统的需求它们会产生很多的错误，复杂的系统它们更是无能为力。因此，迫切需要更加科学的方法来研究复杂系统，论文提出用复杂网络的度相关特性作为需求获取的方法。复杂网络就是对大量现实世界真实复杂系统的一种理想简化描述，相关性有可能带来复杂系统理论的新突破。 在获取了系统的需求后再用形式化B方法进行描述，以提高系统的可靠性，但是，B不是面向对象而是基于对象的并且B需求规格说明的可读性差。可读性差阻碍了在规格校验时用户的介入。而统一建模语言(UMI)已成为面向对象软件系统中描述分析和设计阶段模型的标准化记法。但UML缺乏精确的语义，因此对模型难以进行一致性检查和正确性分析，成为基于UML技术的严重缺陷。 针对以上问题，本文提出了形式化B方法到UML类图的转换思想，将形式化B方法转换后的UML类图更好地用于面向对象的软件开发中。其中B方法作为数学基础；UML作为支持建模语言，其图形表示直观易理解；将UML与形式化语言的的准确性、一致性结合起来，为模型的正确性证明、转换及一致性检查提供有力的理论方法。 主要做了以下方面的工作： 1、对现有的需求获取的方法进行了归纳总结，提出用复杂网络的度相关特性作为复杂系统需求获取的方法。 2、通过用复杂网络对神经内分泌复杂系统的研究，得到了这个系统的一些统计特性和部分重要细胞及介质。 3、使用研究得到的结果对神经内分泌复杂系统进行形式化B描述，然后用ProB工具对得到的B规格说明进行模型检测和一致性检测。 4、对已有的形式化B方法到UML类图的转换机制做了改进，克服了原有方法不能转换机器动态部分等缺点。 本文用复杂网络的度相关特性作为需求获取的方法，并提出形式化B方法到UML类图的改进转换方法，以神经内分泌复杂系统作为应用进行研究，使用B到UML类图的转换方法，得到类图，并最终用面向对象方法实现。

目录

文摘

英文文摘

声明

第一章引言

1.1研究背景

1.2国外研究现状

1.3论文研究意义

1.4章节安排

第二章相关知识介绍

2.1形式化方法

2.1.1形式化方法介绍

2.1.2 B方法

2.2 UML介绍

2.2.1 UML的建模机制和应用

2.2.2 UML的优劣

2.3复杂网络

2.4本章小结

第三章复杂系统的度相关特性需求获取

3.1需求获取的问题

3.2已有需求获取方法及比较

3.2.1传统需求获取方法

3.2.2现代需求获取方法

3.3复杂网络的度相关特性作为需求获取方法

3.3.1神经内分泌复杂系统

3.3.2神经内分泌复杂系统的度相关特性

3.4本章小结

第四章神经内分泌系统形式化需求描述、验证

4.1水痘病毒入侵神经内分泌系统

4.2神经内分泌系统B机器描述

4.3神经内分泌机器的工具验证

4.4本章小结

第五章B方法到UML转换研究及实现

5.1形式化B—UML类图转换的改进方法

5.2神经内分泌系统由B转换得到的类图

5.3系统的详细设计

5.3.1开发环境

5.3.2部分代码

5.4本章小结

第六章总结与展望

6.1本文工作总结

6.2进一步工作

参考文献

致谢

论文发表情况及参加科研项目、学术会议