Communicating Finite State Machines 系统的安全组合

参与者即接口（PaI）方法建议系统的参与者可被视为接口。给定一组系统，选择每个系统的某个参与者作为接口角色。当系统组合时，接口参与者被替换为进行消息转发的网关。PaI方法针对异步通信有限状态机（CFSM）的二进制组合在文献中已被利用，仅使用（必然唯一的）转发策略。本文我们考虑多系统组合的情况，当转发网关无法唯一确定且其相互作用取决于符合特定连接模型的连接策略时。我们将连接策略表示为CFSM系统，并证明了一系列相关通信属性（如死锁自由性、接收错误自由性等）通过PaI多组合成时被保留，前提是所使用的连接策略也满足所考虑的通信属性。