SynQ：一种用于同步系统设计的嵌入式领域特定语言

系统设计自动化旨在管理日益复杂的嵌入式系统设计。对于系统设计自动化的成功而言，仍然缺乏系统化和形式化的设计流程，因为从系统规约到实现的整个设计过程必须处理系统不同方面的固有关注点，以及由此产生的固有语义鸿沟。这些鸿沟使得设计过程难以追踪或透明。特别是，保证所产生实现的正确性成为系统设计过程的主要挑战。SynQ（基于定量类型的同步系统设计）是一种嵌入式领域规约语言（EDSL），旨在设计遵循完美同步假设的系统。SynQ基于一个基于组件的设计框架，并通过利用定量类型理论（QTT）和语言嵌入，从设计上促进了语义一致性。SynQ实现了一个语义连贯的设计过程，包括形式化规约与验证、建模、仿真和代码生成。本文介绍了SynQ及其底层形式化方法，并通过一个案例研究展示了其在语义连贯系统设计方面的特性和潜力。