一种扩展的并发传值进程抽象模型

论文摘要

形式化方法中的模型检测技术是近三十年来最为成功的自动验证技术之一。对并发传值系统进行模型检测需要建立相应的抽象模型,带赋值的符号迁移图是一种广为使用的抽象模型。 对于并发传值系统抽象模型的选取直接影响其模型检测的效率。由于带赋值的符号迁移图(STGA)可以用有穷状态图表示具有无穷数据实例的进程,因而得到了广泛的关注。但是在STGA中,同一个带参进程定义体可能会产生多块子图,这影响了模型检测的空间和时间效率。为了解决这一问题,本文提出了STGA的一种扩充。其基本思想是在符号迁移图中,输入/输出动作的前面和后面都引入赋值,从而保证在所产生的符号迁移图(称为STGA~2)中,每个带参进程定义体只对应于一块子图,而不是像STGA那样对应于多块子图,因此使生成的符号图更为紧凑。 本文提出了扩展带赋值的符号迁移图的方法,主要工作如下: ● 定义了带双赋值的符号迁移图STGA~2及其操作语义。 ● 证明了STGA~2与STGA的语义等价性。 ● 提出了STGA~2上的简化规则,并证明这些规则保持语义。 ● 实现了STGA~2的操作语义和简化规则。通过实例研究比较了STGA~2与STGA的优劣。

论文目录

• 摘要
• Abstract
• 目录
• 第一章 引言
• 1.1 研究背景
• 1.2 论文主要工作
• 1.3 论文的组织
• 第二章 形式化方法和并发传值系统
• 2.1 形式化方法
• 2.2 并发系统
• 2.3 并发系统描述语言
• 2.4 模型检测
• 2'>第三章 STGA的一种扩展-STGA²
• 3.1 纯CCS和传值CCS
• 3.1.1 传值CCS符号
• 3.1.2 传值CCS语法
• 3.2 符号迁移图
• 3.3 带赋值的符号迁移图
• 2'>3.4 带双赋值的符号迁移图-STGA²
• 2的基本定义'>3.5 STGA²的基本定义
• 3.5.1 赋值与动作
• 2的定义'>3.5.2 STGA²的定义
• 2的生成规则'>3.5.3 STGA²的生成规则
• 2图的并发合成'>3.5.4 STGA²图的并发合成
• 2的操作语义'>3.5.5 STGA²的操作语义
• 3.5.6 互模拟
• 3.5.7 消除“void”动作
• 第四章 其它STGA的相关工作
• 4.1 加后赋值的STG
• 4.2 后赋值的STGA—STGA′
• 4.3 STGLA
• 2工具实现'>第五章 STGA²工具实现
• 5.1 μ演算
• 5.1.1 模态逻辑
• 5.1.2 时序逻辑
• 5.1.3 命题μ演算
• 5.1.4 谓词μ演算
• 5.2 工具的结构与实现
• 第六章 检测实例与数据结果
• 6.1 实例说明
• 6.1.1 数据缓冲器
• 6.1.2 交错位协议
• 6.1.3 CIM协议
• 6.1.4 TMR协议
• 6.2 实测结果
• 第七章 结束语
• 附录A 互模拟、模型检测脚本
• A.1 Bag3
• A.2 ABP协议
• A.3 CIM
• A.4 TMR
• 附录B 程序源码
• 参考文献
• 发表文章目录
• 致谢