面向过程的设计和并发系统的实现具有重要的好处。 但是,并发流程通信固有的复杂性带来了挑战,例如验证面向流程的设计与并发系统的实现之间的一致性。 为了应对这一挑战,我们使用Galois连接,故障和类别理论来构建用于设计,实现,分析和验证并发系统一致性的正式框架。 为了说明该框架,通过通信顺序过程设计了一个运行中的并发系统,该过程由面向过程的编程语言Erasmus实现。