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