基于多方会话的多时钟同步规范合成与验证机制的研究

Synchronous languages have been widely used in the design of safety-critical cyber-physical systems in recent years. Existing mainstream imperative synchronous languages are not yet capable of supporting multi-clock semantics, and thus may generate a large amount of redundant communication when deployed directly in a distributed environment. The multi-clock specifications commonly used in dataflow synchronous languages are based on clock calculus and cannot be easily applied to imperative synchronization languages. This project proposes the concept of multi-clock sessions in the form of synchronous cummunicating automata. In particular, we translate imperative synchronous programs into Extended Finite State Machines (EFSM), and then extract multi-clock sessions from these EFSMs. For a multi-party session system consisting of multiple synchronous processes, we study the algorithm that verifies the consistency of its multi-party sessions. The consistency of the synchronous multi-party sessions ensures clock consistency of the synchronous system. Combined with the existing desynchronization theory, we can prove the consistency between the behavior of the system after desynchronization and the behavior of the original synchronous system, so as to avoid the occurrence of deadlock as well as other problems in concurrency. This project also introduces the concept of synchronous global session which uniformly describes the global communication of the synchronous system. We study the automatic synthesis of a global session from multiple multi-clock sessions as well as the projection from a global session into multi-clock sessions in order to support both bottom-up and top-down design flows respectively. This project provides new ideas and methods for both the theory and practice of distributed deployment of synchronous systems.

同步语言近年来在安全攸关信息物理系统的设计中得到了广泛应用。现有的主流命令式同步语言尚无法支持多时钟语义，因而在分布式环境下会产生大量的冗余通信。而普遍应用于数据流同步语言的多时钟规范基于时钟算子，无法适用于命令式同步语言。本课题提出多时钟会话的概念，将命令式同步程序翻译为扩展状态机，并提炼其多时钟会话。对于多个同步过程组成的多方会话系统，我们研究验证其多方会话一致性的算法。同步系统多方会话的一致性可保证系统时钟一致性。结合现有的去同步理论，我们可以证明经过去同步后的系统行为与原始同步系统行为的一致性，从而避免并发中的死锁等问题的发生。本课题还引入同步全局会话的概念，对同步系统的全局通信进行统一描述。我们研究从多个过程会话到全局会话的自动合成方法以及从全局会话到多个过程会话的映射方法，从而分别支持自底而上或自顶而下的设计流程。本课题为同步系统分布式部署的理论与实践均提供了新的思路与方法。

近年来在安全攸关信息物理系统的设计中，同步语言得到了广泛应用。现有的主流命令式同步语言尚无法支持多时钟语义，因而在分布式环境下会产生大量的冗余通信。而普遍应用于数据流同步语言的多时钟规范基于时钟算子，无法适用于命令式同步语言。在此背景下，本项目进行了以下研究：.• 通过将分布式系统中多方回话类的概念与同步系统中扩展状态机的概念相结合，提出同步通信状态机并实现了单时钟同步系统的多时钟抽取，通过去同步技术实现了同步模型的分布式部署。.• 针对异构数据流网络提出了基于输入/输出模式（I/O Pattern）的综合设计优化方法。.• 通过同步守护动作模型实现深度神经网络的等价表示。.本项目重要结果包括：.• 建立并完善了多时钟去同步理论、多时钟一致性验证算法，研发了基于单时钟命令式同步语言Quartz的去同步综合设计流水线，实现了OpenCL目标代码的自动化综合设计，为基于同步模型的分布式信息物理系统的设计与部署建立了完整的工具链，并通过实验初步验证了方法的有效性。.• 针对异构数据流网络提出了基于输入/输出模式（I/O Pattern）的综合设计优化方法，进一步完善了去同步理论与设计流程。.• 初步实现了深度神经网络的同步模型等价表示。.本项目实现了基于命令式同步语言的去同步任务，为解决命令式同步建模系统的分布式部署提供了新的方法。通过本项目提出的基于输入/输出模式的综合设计优化方法，可有效地实现异构系统的建模与分布式部署。本项目所提出的深度神经网络等价表示方法，初步验证了联合建模的可行性，并且为联合建模提供了初步的思路。