基于csp的面向方面状态图形式化描述方法研究

论文摘要

UML作为面向对象分析和设计建模语言的标准,有广泛的应用和扩展背景,通过UML的扩展机制使其支持面向方面状态图的建模,但UML建模的状态图采用的是自然语言描述及图表结构,缺乏形式化的精确语义,不利于系统的求精和验证,从而有必要引入形式化方法对其进行研究。本文首先说明了面向方面存在的优点,阐述了面向方面编程的核心思想,并通过形式化语言B的AOP扩充以及支持组件设计和AOP的形式化方法AO-RT-Z综述了最近几年在形式化面向方面的研究工作。然后通过UML扩展机制把面向方面状态图分成核心状态图和方面状态图,利用编织事件映射为织入方法将两者联系起来以实现面向方面状态图的建模,但原有的织入方法描述只适用于一个核心组件和一个方面。本文扩展了织入方法的描述,给出了一种描述多个方面同时织入核心组件或方面的方法,此方法说明了多个方面织入核心组件或者方面的次序,为复杂的面向方面状态图的建模奠定了基础。为了对面向方面的状态图进行进一步的求精和验证,本文给出一种通过CSP描述方面状态图的规则,通过规则对面向方面状态图中包含的6个典型的状态进行CSP定义,然后对有限缓冲和ATM自动取款两个实例进行面向方面状态图的建模和CSP的描述。为了检测描述的正确性,本文最后通过与CSP匹配的模型检测工具FDR对ATM自动取款机面向方面状态图的CSP描述进行验证,证明了CSP描述面向方面状态图的可行性和正确性。

论文目录

• 摘要
• ABSTRACT
• 第一章 引言
• 1.1 研究背景
• 1.2 国内外研究现状
• 1.3 论文研究内容和组织
• 第二章 面向方面UML状态图与形式化
• 2.1 AOP概述
• 2.1.1 AOP的发展及优势
• 2.1.2 AOP核心思想
• 2.2 面向方面与形式化
• 2.2.1 面向方面与形式化语言B
• 2.2.2 面向方面与形式化方法AO-RT-Z
• 2.3 扩展UML表示面向方面状态图
• 2.3.1 UML的扩展机制
• 2.3.2 UML状态图
• 2.3.3 面向方面状态图的UML描述
• 2.4 形式化UML状态图
• 2.4.1 形式化面向对象状态图
• 2.4.2 形式化面向方面状态图
• 2.5 本章小结
• 第三章 基于CSP形式化面向方面状态图
• 3.1 形式化CSP语言
• 3.2 面向方面状态图形式化规则描述
• 3.3 CSP形式化面向方面的状态图
• 3.3.1 初始状态CSP形式化
• 3.3.2 终止状态CSP形式化
• 3.3.3 简单状态CSP形式化
• 3.3.4 选择状态CSP形式化
• 3.3.5 历史状态CSP形式化
• 3.3.6 复合状态CSP形式化
• 3.4 有限缓冲面向方面状态图CSP形式化
• 3.5 ATM自动取款机面向方面状态图CSP形式化
• 3.6 本章小结
• 第四章 CSP的面向方面状态图的模型检测
• 4.1 模型检测
• 4.2 FDR模型检测工具
• 4.3 FDR验证基于CSP的面向方面状态图
• 4.4 本章小结
• 第五章 总结和展望
• 5.1 主要工作及创新点
• 5.2 进一步工作思路
• 参考文献
• 致谢
• 攻读学位期间主要的研究成果