This paper focuses on formally specifying and verifying the chain of formal semantics of the Esterel synchronous programming language using the Coq proof assistant. In particular, in addition to the standard logical (LBS) semantics, constructive semantics (CBS) and constructive state semantics (CSS), we introduce a novel microstep semantics that gets rid of the Must/Can potential function pair of the constructive semantics and can be viewed as an abstract version of Esterel's circuit semantics used by compilers to generate software code and hardware designs. Excluding the loop construct from Esterel, the paper also provides formal proofs in Coq of the equivalence between the CBS and CSS semantics and of the refinement of the CSS by the microstep semantics.

翻译：本文重点研究使用Coq证明辅助工具对Esterel同步编程语言的形式语义链进行形式化规约与验证。具体而言，除了标准的逻辑（LBS）语义、构造语义（CBS）与构造状态语义（CSS）外，我们提出了一种新颖的微步语义，该语义摆脱了构造语义中Must/Can势函数对，可视为编译器用于生成软件代码与硬件设计的Esterel电路语义的抽象版本。在排除Esterel循环结构的前提下，本文还提供了CBS与CSS语义等价性、以及微步语义对CSS精化关系的Coq形式化证明。