基于数据流的微分代数事件结构及其层次化理论研究

事件结构是一种主流高效的形式化方法，为并发系统的建模与验证做出了巨大的贡献。在计算机科学和控制工程领域，并发系统的组成与结构越来越复杂，并且对支撑建模与验证的形式化工具的要求水准也越来越高。比如，对同时存在离散行为和连续行为的混杂并发系统，如果使用传统的事件结构来建模，则难点主要是对“数据流交换过程”的处理上和对“连续的状态变化”的处理上，而数据流的交换过程和数据流的连续演化过程恰恰都是并发系统最重要的行为特征。因此对并发系统的设计和验证需要一套全新的形式化理论与方法。课题尝试基于传统事件结构，借助符号计算、微分方程的思想，建立一种新型的基于数据流的事件结构模型，进而给出新事件结构的等价判定计算方法，然后研究新事件结构的层次化方法以及在层次化下等价的可保持性等理论。目标是推动并发理论的形式化工具得到创新和发展，使得新事件结构在刻画复杂并发系统方面依然扮演着重要角色，有着重要的理论和实际价值。

As a mainstream and efficient formal method, Event structure has made great contributions for modeling and verification of concurrent systems for decades. In computer science and control theory, control engineering, composition and structure of concurrent systems are becoming more and more complex, meanwhile, the standard for formal tools used to support modeling and verification are also becoming higher and higher. For example, as far as hybrid concurrent systems with discrete behaviors and continuous behaviors exist at the same time be concerned, if traditional discrete event structure is used to modeling, the main difficulties are processing of "data flow exchange process" and processing of "continuous change of states". But exchange process and continuous change of data flow are precisely the most important two behavior characteristics of concurrent systems. Therefore, the design and verification of concurrent systems need a new set of formal theory and methods. This project attempts to firstly define a new event structure model based on data stream by means of symbolic computation, differential equation ,etc., then proposes its judgment method on equivalence, furthermore studies its refinement method ,and finally researches on what conditions refinement must satisfy, so that some equivalence properties of original event structure can also be preserved under refining. Our goal is to promote formal tools of of concurrency theory for innovation and development, make the new event structure still plays an important role in modeling and verification of complex concurrent systems.Therefore, the subject has important theoretical and practical value.