基于模型检测结果的CSP并发系统调试技术研究

摘要

目前，主流的CSP（Communicating Sequential Processes：通信顺序进程）模型检测工具普遍采用三层模型进行性质验证，但三层模型在表达方式上具有较大的差异性，从而使得在底层实现模型上进行性质验证时发现的错误，难以通过两次逆向变换准确地定位到高层模型中，增加了调试系统错误的难度；而且在性质验证成立时，难以获取保证性质成立的部分系统结构，在模型发生部分改变后需要对所有性质重新验证，增加了系统开发成本。本课题组开发了一套基于ASP（Answer Set Programming）的 CSP并发系统性质验证统一框架，该框架仅需两层模型即能完成对性质的验证，并且利用 ASP的纯声明特性使得两层模型间的差异性较小，同时也减少了多层模型间的转换开销，但该框架还缺乏对 CSP并发系统的调试功能。本文在课题组前期工作的基础上，提出一种采用两层模型的、基于模型检测结果的 CSP并发系统调试方法，可实现方便地找出原始 CSP模型中的错误，并能避免模型改变后对依然成立性质的重复验证。主要研究内容如下： （1）支撑原因分析技术的功能扩展。扩展现有ASP程序的支撑原因分析技术，使其能够给出某原子成立或不成立时的完整原因，从而提取原子相对于某回答集成立或不成立的所有相关信息，进而实现对模型检测结果以及性质规则的分析。 （2）性质成立或不成立原因的生成。首先依据模型检测结果将非实例化性质规则实例化，然后利用扩展的支撑原因分析技术分析实例化性质规则以及模型检测结果，最后可生成性质成立或不成立的原因。 （3）基于反例迹的系统错误调试。对性质不成立的原因中导致性质不成立的系统状态进行反向分析，生成对应的反例迹，并通过拆分反例迹，获取组成并发进程的所有子进程的执行迹，最后演示子进程运行执行迹时的行为帮助开发人员理解错误原因，从而定位原始CSP系统模型中的错误。 （4）系统模型修改后已验证性质影响分析。首先提取性质成立的原因中所包含的系统状态集，获取保证性质成立的部分系统结构，然后在此基础上，判断模型修改后该部分系统结构是否发生改变，最后实现了避免对依然成立的性质的重复验证。

目录

封面

声明

中文摘要

英文摘要

目录

第一章 绪论

§1.1 研究背景

§1.2 研究现状

§1.3 本文的主要内容

§1.4 本文的结构

第二章 相关基础知识概述

§2.1 CSP基础概述

§2.2 ASP回答集编程语言

§2.3 哲学家就餐问题的CSP描述及性质验证

§2.4 本章小结

第三章 基于模型检测结果的CSP并发系统调试框架

§3.1 框架设计基础

§3.2 框架设计思想

§3.3 框架模块介绍

§3.4 系统调试流程

§3.5 本章小节

第四章 支撑原因分析技术的功能扩展

§4.1 性质规则的实例化

§4.2 支撑原因分析技术的功能扩展

§4.3 性质规则的支撑原因实例分析

§4.4 本章小结

第五章 CSP并发系统的调试

§5.1 反例迹的生成算法

§5.2 基于反例迹的错误调试

§5.3 系统修改后已验证性质依然成立的判断

§5.4 基于模型检测结果的CSP调试实例分析

§5.5 本章小节

第六章 总结与展望

参考文献

致谢

作者在攻读硕士期间的主要研究成果