A Formally Verified Clock Checker For The Synchronous Data-flow Language Lustre*

Synchronous data-flow languages are widely used in safety-critical industrial areas,such as aerospace,high-speed rail and nuclear power.The Scade tool based on a Lustrelike language is suitable for the modeling and development of real-time control systems in these fields.The safety of compilers,for these languages,has also received a high degree of attention.In recent years,the implementation of a trustworthy compiler based on formal verification has made great progress,for example,the C-based Compcert project implements a product-level trustworthy compiler.Tsinghua University L2 C Group also used this formal verification method to develop a trustworthy compiler based on an extended Lustre language.The compiler uses Lustre* as the source language,and uses Clight as the target language.Clight is the subset of the C programming language,which is used as input to the Compcert compiler.Because programs written in the Lustre* language have the feature of the nested clock,the process of static checking is divided into two aspects.On the one hand,traditional type checking on Lustre*'s abstract syntax tree is performed without considering the clock of expression and variable.On the other hand,clock checking on the abstract syntax tree is performed,that is,check whether the clocks of the expressions and variables in the Lustre* program match.This paper mainly introduces the clock check of the static check in the L2 C compiler.This paper introduces the following work: First,the clock calculus rules are defined.The clock calculus rules specify what the clock checker checks.Second,the clock checker of the L2 C trustworthy compiler is implemented by the Coq Proof Assistant.Finally,It turns out that the Lustre* program that passes the clock checker must be well-clocked.