基于通信顺序进程的并发DEDS的规范和证实

在实时通信顺序进程 ( TCSP)的基础上对离散事件动态系统 ( DEDS)进行建模、规范和证实 .介绍了 TCSP中与 DEDS相关的一些研究成果 ,根据离散事件的特点作了符号语义上的改进 ,就两个具体的例子——自动导引小车 ( AGV)和火车道口系统建立了 TCSP模型 ,给出了它们需要满足的特性 。