一种分布式事务通信有限状态机模型及其验证方法

摘要

一种分布式事务通信有限状态机模型及其验证方法：(1)分布式事务通信有限状态机模型可以用一个七元组表示；(2)分布式事务协议有限状态机验证方法是从TCFSM的初态开始，采用深度优先的方法，生成每个节点的所有可能后继结点，从而描述一个协议所有进程的所有可能的执行过程。本发明提出的分布式事务通信有限状态机模型通过增加终态集、匹配终态集以及内部事件等方式提高模型的描述力，可以较好的描述分布式事务协议；同时提供了该模型的验证方法。