实时离散事件系统规范与证明方法

Research on Specification and Verification Methodsof Real-Time Discrete Event System

针对离散事件系统的规范与证明，给出了多种形式化方法，并且在这些形式化方法的基础上，将时间因子引入，从而解决实时离散事件系统的实时规范问题．虽然这些实时形式化方法是从不同角度提出的，但它们之间存在内在联系．通过对这种联系进行深入研究，为以后更加有效地使用这些形式化方法提供了理论依据．

According to the specification and verification of a discrete event system kinds of formal methods are presented.And the time factor is brought into these methods to solve the realtime specification problem of realtime discrete event system.Although these realtime formal methods were proposed from different aspects,there exists internal connections between them.The results of the research on these connections are given,which provide theoretical basis for the effective use of these formal methods.