模型检测技术是近二十年来最成功的自动验证技术之一，目前被广泛的应用于有穷状态系统(包括电路设计和通讯协议等)的分析与验证。对于并发传值系统的自动分析与验证是模型检测研究的一个新的方向。 随着并发系统规模的日益增大，对这类系统的模型检测面临着如何处理大规模状态空间问题的挑战，因此需要为实际的大规模并发系统精心选择计算模型，同时设计时空效率较高的算法。但是我们注意到并发传值系统的一个特点是其子系统间的通讯经常涉及复杂数据结构，包括数组、列表和记录等。以往处理复杂数据结构的做法是抽象掉数据信息或者将复杂数据结构打散，因而较大的影响了检测效率。解决这个问题的一个方案是：使用带赋值符号迁移图(STGA)作为并发传值进程的模型，使用谓词μ演算作为刻画性质的逻辑，并采用动态实例化的算法对传值并发进程直接进行模型检测。 本文提出了将复杂数据结构引入上述模型检测方案的办法，扩大了该解决方案可以应用的问题领域。主要工作如下： ·扩展传值CCS使其成为有严格类型规则的易于使用的系统描述语言、扩充了STGA的定义和生成规则使其适于作为实际系统的计算模型。 ·提出了扩展STGA图的优化算法。 ·扩充检测问题的定义语言—脚本语言的格式，使用SML语言实现了脚本语言的编译和扩展STGA图生成模块，并将该模块和检测算法核心连接，实现了整个工具。论文还结合应用实例证明了扩展工作的有效性并分析了工具的性能。