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

Specification of DEDS Based on the Communicating Sequential Process

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

This paper did the model, specification and verification of Discrete Event Dynamic System(DEDS) based on the Timed Communicating Sequential Process(TCSP) and its improvement. First, some TCSP research results related with DEDS were introduced and several improvements of their semantic denotations were made. Then, two examples——autonomous guided vehicles and train & port system were showed and their models, specifications and verifications were given.