并发系统的形式化技术研究

论文摘要

随着计算机技术在尖端领域的应用,为了提高系统的安全性与可靠性,形式化方法得到长足的发展,也出现了许多优秀的形式化工具,例如,B、VDM、Z语言,还有诸如Petri网、CSP、CCS、时序逻辑语言(TSL)等工具。但是这些形式化工具功能单一,只适合描述系统的某些方面。针对这种情况,计算机科学界开始进一步研究各种不同的形式化方法的特点,并将它们综合起来,于是集成形式化方法成为现代形式化方法研究的一个重要方向。本文提出一种集成B语言和进程代数CCS的方法,构建一个混成模型:BCCS。这个模型借助B方法及语言来扩展CCS在数据和操作定义方面的能力,同时保留了CCS在描述并发系统方面的能力,因此混成后的形式化方法可以描述和分析系统的不同方面(结构,控制,数据和功能)和不同类型的系统(顺序,并发和分布式)。基于模型的需求和基于行为的需求是信息系统的两个重要刻面,和传统功能单一的形式化方法相比,BCCS模型统一了信息系统中这两个重要的刻面。为了给传值CCS提供丰富的表达式和通用的语法,在模型中我们还给出一个轻量级的描述语言,并通过其操作语义来保证这个描述语言的完备性和一致性,同时为在同一个模型内描述基于行为的需求和基于模型的需求提供了理论基础。另外,由于B方法的引入,其模块化技术使BCCS模型还可以描述大型复杂的系统。总之,BCCS模型实现了一种更具表达能力的形式化描述工具,可以从更多的刻面来描述大型复杂的系统。

论文目录

• 论文摘要
• ABSTRACT
• 第1 章 绪论
• 1.1 研究背景及现状
• 1.2 研究的意义和目的
• 1.3 论文的组织结构
• 第2 章 形式化方法与并发系统
• 2.1 形式化方法
• 2.2 并发系统
• 2.2.1 进程
• 2.2.2 并发系统描述语言
• 2.3 小结
• 第3 章 混成形式化模型：BCCS
• 3.1 BCCS 模型概述
• 3.2 B 方法
• 3.3 通信系统演算（CCS）
• 3.3.1 CCS 概述
• 3.3.2 传值CCS 的裁剪及其操作语义
• 3.4 BCCS 的语法
• 3.4.1 BCCS 语法元语言
• 3.4.2 BCCS 定义的基础
• 3.4.3 BCCS 的语法
• 3.4.4 用BCCS 模型描述的极坐标到直角坐标转换系统
• 3.5 BCCS 的操作语义
• 3.5.1 环境与抽象机
• 3.5.2 动作和参数
• 3.5.3 环境的初始化
• 3.5.4 语义域
• 3.5.5 语义推理规则
• 3.6 BCCS 和几种集成方法的比较
• 3.7 小结
• 第4 章 基于BCCS 的应用实例
• 4.1 实例背景介绍
• 4.1.1 EJB3.0 的有状态会话 Bean
• 4.1.2 容器（Container）
• 4.1.3 生命周期（life cycle）
• 4.2 基于BCCS 模型的SFSB 生命周期规范
• 4.2.1 SFSB 的生命周期模型
• 4.2.2 基于BCCS 的SFSB 生命周期规范
• 4.3 小结
• 第5 章 结束语
• 5.1 本文主要研究成果
• 5.2 进一步的工作
• 参考文献
• 致谢