本文通过量子互模拟性检测对由量子进程代数描述的量子程序,主要是量子通讯协议,进行正确性验证。量子进程代数是用于量子程序形式化验证的技术之一,是经典进程代数在量子计算场景下的扩展,可以形式化地描述量子系统。基于这项技术,只要有合适的对行为等价性的定义以及对应的等价性检测方法,就可以通过判断一个协议的实现与其需求归约是否一致来验证协议的正确性。本文中考虑的基互模拟对量子程序来说是便于使用的行为等价性关系之一。量子程序以及量子协议的建模则得力于量子通信系统演算qCCS。qCCS由Feng等人提出,是为描述复杂量子系统中的通信以及并发行为而提供的一个通用的形式化框架,是通信系统演算CCS在量子计算框架下的一个扩展。模型的行为可以很容易地通过概率标号迁移系统来解释,而模型之间的等价性可通过互模拟来表示,因此可参考概率互模拟检测算法来进行量子互模拟检测算法的设计。本文的主要工作为设计并实现算法以检测下面三个版本的基互模拟:-基于状态的量子程序强基互模拟检测算法。量子强基互模拟是由经典的基互模拟引申到量子计算场景下得到的,在经典的基互模拟定义上加入了对量子寄存器以及量子程序上下文环境的约束。根据量子强基互模拟的定义,本文设计并实现了一个on-the-fly算法用以检测两个给定的由qCCS编写的量子程序是否是互模拟的。此外在匹配状态分布时,引入了lifting操作来将状态之间的互模拟关系转换到状态的分布之间,同时也带来了更多约束需要验证是否满足。在算法的设计中,状态分布之间的匹配问题被视为一个二分匹配问题,并通过最大流算法来解决。-基于状态的量子程序弱基互模拟检测算法。量子弱基互模拟是在量子强基互模拟的基础上,将匹配两个迁移替换为匹配一个迁移与一个弱迁移的情况。与之前的迁移不同,弱迁移允许在动作的前后添加若干内部动作τ。由于匹配的对象变成了弱迁移,弱迁移的目标可以是若干个状态或状态分布的组合,因此迁移的匹配成为了一个新的问题。在量子程序弱基互模拟检测算法的设计中,本文同样是设计一个on-the-fly算法,并将迁移的匹配问题归约到一个线性规划问题上,从而进行求解。-基于分布的量子程序基互模拟检测算法。基于分布的量子基互模拟与上述的基于状态的量子基互模拟不同,匹配的迁移并不是状态之间或是状态到分布,而是分布到分布的迁移。甚至与经过lifting操作之后的基于状态的互模拟也不相同。本文设计了两个基于分布的量子程序基互模拟检测算法,分别为一个on-the-fly算法,以及一个基于互模拟矩阵的算法。算法验证的对象都存在一定的约束。前者仅限于验证有限树状的pLTS。后者可验证有限非树状的pLTS,但仅限于验证封闭的量子系统,且系统不可有与外部的量子通信。其首先构造一个表现了两个系统之间互模拟关系的一个特征矩阵,然后对系统中的状态分布对进行遍历,验证两个状态分布之差与矩阵每列的乘积是否都为0,判断分布是否是互模拟的。本文证明了各个算法的可终止性与正确性,并分析了算法的时间复杂度。并且基于上述算法的实现,开发了工具QBisim,用于验证各种量子协议。在输入需要的信息后,整个验证的过程都是自动化的。本文使用QBisim对一些量子协议进行了验证,主要为各种利用量子纠缠态特性设计的量子通信协议,例如量子隐态传输协议,以及量子密钥分发协议,例如BB84量子密钥分配方案。实验结果表明工具是有效的。