OTN(光传送网,Optical Transport Network)技术在通讯领域的应用极大的提高了信息的传输速度,降低了误码率。OTN通过保护倒换系统来确保信息传输不被中断,因此保护倒换系统的可靠性需要得到保障。光传送网络中,保护倒换系统需要在满足APS(Automatic Protection Switching)协议的基础上,进一步满足不同应用场景的需要。这需要在系统设计阶段,就开始验证设计方案是否遵循了APS协议并满足相应的场景需要。但在保护倒换系统设计阶段,很少有人关注该阶段的形式化定义,而保护倒换系统未能按照需求和协议生效很大一部分原因是需求定义具有二义性或遗漏产生的。传统的建模方法,包括流程图、状态图、时序图等都不能解决需求定义的二义性和遗漏问题,使得在系统的后续开发中存在巨大的隐患。并且,对于日益复杂的系统,因状态空间爆炸问题,其验证也变得日益困难。本文提出一种基于二维表格结构的形式化方法来定义系统需求,可以最大程度上减少需求定义的二义性和遗漏问题。该方法的基本思想来源于状态迁移矩阵,表结构的第一行为源状态行,代表对应的系统所有的状态;第一列为目标状态列,代表系统从任一源状态出发,可能到达的目标状态;而源状态和目标交叉确定的位置,代表系统在当前源状态下,系统满足一定先决条件,会发生的动作。在文中,这种二维表结构被称为状态迁移表格(State Transition Form,STF).针对STF模型的验证,采用边界模型检测的方法。将STF模型和待验证的性质进行符号化编码,并输入到SMT求解器中进行验证。从而完成了保护倒换系统形式化建模和验证流程。接着本文依据已有的自动机状态压缩算法,提出了基于STF模型的状态压缩算法。该方法在STF模型的基础上,经过简单的矩阵行列变化,可以将较大的STF模型压缩成较小的STF模型,一定程度上缓解了状态空间爆炸问题,在压缩后的STF模型的基础上进行符号化编码和性质验证所花费的时间都有一定程度的减少。最后采用SMT求解器Z3和UPPAAL工具进行验证,说明算法有效性。