基于偏序简化的并发系统验证

摘要

构件交互风格和交互协议的描述与验证是基于构件的分布式系统开发的基础和关键,而构件交互协议是一种典型的分布式并发系统.传统的方法难以解决系统建模和验证中的所谓的状态爆炸问题.偏序简化是应用迹的概念,对模型进行化简并且对模型进行死锁验证.但这样的验证重点放在了Petri网模型上,而没有涉及进程代数模型,所验证的只是模型是否有死锁状态.而以通信系统演算CCS为代表的进程代数,因其概念简洁,可用的数学工具丰富,在分布式并发系统的规范、分析、设计和验证方面获得了广泛应用.对此,提出将偏序规约应用于进程代数模型,给出基于进程代数模型的偏序简化算法,并提出利用进程代数模型偏序简化算法来验证安全性的方法.