| 题名 | 井发传值进程模型检测工具的数据类型扩展 |
| 作者 | 张轶 |
| 学位类别 | 博士 |
| 答辩日期 | 2003 |
| 授予单位 | 中国科学院软件研究所 |
| 授予地点 | 中国科学院软件研究所 |
| 关键词 | 形式化方法 模型检侧 并发传值进程 复杂数据类型 传值CCS 带赋值符号迁移图 |
| 其他题名 | Extending a Model-Checking Tool with Non-trivial Data Structures |
| 学位专业 | 计算机软件与理论 |
| 中文摘要 | 模型检测技术是近二十年来最成功的自动验证技术之一，目前被广泛的应用于有穷状态系统（包括电路设计和通讯协议等）的分析与验证。对于并发传值系统的自动分析与验证是模型检测研究的一个新的方向。随着并发系统规模的日益增大，对这类系统的模型检测面临着如何处理大规模状态空间问题的挑战，因此需要为实际的大规模并发系统精心选择计算模型，同时设计时空效率较高的算法。但是我们注意到并发传值系统的一个特点是其子系统间的通讯经常涉及复杂数据结构，包括数组、列表和记录等。以往处理复杂数据结构的做法是抽象掉数据信息或者将复杂数据结构打散，因而较大的影响了检测效率。解决这个问题的一个方案是：使用带赋值符号迁移图（STGA）作为并发传值进程的模型，使用谓词p演算作为刻画性质的逻辑，并采用动态实例化的算法对传值并发进程直接进行模型检测。本文提出了将复杂数据结构引入上述模型检测方案的办法，扩大了该解决方案可以应用的问题领域。主要工作如下：扩展传值CCS使其成为有严格类型规则的易于使用的系统描述语言、扩充了STGA的定义和生成规则使其适于作为实际系统的计算模型。提出了扩展STGA图的优化算法。扩充检测问题的定义语言一脚本语言的格式，使用SML语言实现了脚本语言的编译和扩展STGA图生成模块，并将该模块和检测算法核心连接，实现了整个工具。论文还结合应用实例证明了扩展工作的有效性并分析了工具的性能。 |
| 语种 | 中文 |
| 公开日期 | 2011-03-17 |
| 页码 | 65 |
| 内容类型 | 学位论文 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/7390]  |
| 专题 | 软件研究所_中科院软件所_中科院软件所 |
| 推荐引用方式 GB/T 7714 | 张轶. 井发传值进程模型检测工具的数据类型扩展[D]. 中国科学院软件研究所. 中国科学院软件研究所. 2003. |
| 个性服务 |
| 查看访问统计 |
| 相关权益政策 |
| 暂无数据 |
| 收藏/分享 |
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论