| 摘要: |
| Scade是一种广泛用于安全攸关嵌入式控制软件开发的著名商业工具, 其建模语言是从同步数据流语言Lustre扩展而来的同步语言. 包括Lustre在内的同步语言的正确编译近年来备受关注, 并在许多研究中通过形式化验证方法来解决. 对此类语言构建形式化验证的编译器, 实践中常见的做法是先将源程序编译为类C程序, 然后使用形式化验证的后端编译器(如CompCert编译器)将其编译为机器相关的低级代码. 其中, 时态算子的正确编译是至关重要的. 介绍一种形式化验证的类Scade时态算子编译并将其应用于形式化验证的编译器项目中, 该项目将Lustre扩展的同步语言翻译成CompCert编译器的前端中间语言Clight. 时态算子的编译和形式化验证分为两个核心阶段, 在交互式证明辅助器Coq中实现. |
| 关键词: 形式化验证 编译 时态算子 同步数据流语言 Lustre Scade CompCert Coq |
| DOI：10.13328/j.cnki.jos.007536 |
| 分类号:TP314 |
| 基金项目:国家重点研发计划(2022YFB3305204) |
|
| Formally Verified Compilation of Scade-like Temporal Operators |
|
GAN Yuan-Ke, WANG Sheng-Yuan
|
|
Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China
|
| Abstract: |
| Scade is a well-known commercial tool widely used in the development of safety-critical embedded control software, whose modeling language is a synchronous language extended from Lustre, a synchronous data-flow language. Correct compilation of synchronous languages, including Lustre, has attracted much attention in recent years, and has been addressed in many studies through formal verification. To build a formally verified compiler for such a language, it is a common practice to compile the source program into a C-like program first, and then to compile it into low-level machine-dependent code using a formally verified backend compiler such as the CompCert compiler, where the correct compilation of temporal operators is crucial. In this study, the formally verified compilation of Scade-like temporal operators is introduced, which is used in a formally verified compiler projects, where a Lustre-extended synchronous language is translated into the front-end intermediate language Clight in the CompCert compiler. The compilation and formal verification of temporal operators are divided into two key stages, which are implemented in the interactive proof assistant Coq. |
| Key words: formal verification compilation temporal operator synchronous data-flow language Lustre Scade CompCert Coq |
