Abstract:Synchronous data-flow languages have been widely used in safety-critical industrial areas such as airplanes, high-speed railways, nuclear power plants, and so on. However,the safety of development tools themselves for this kind of languages has become one of the potential safety problems which have been highly focused on. It has proved to be successful to implement the construction and verification of a conventional language compiler using an assistant theorem prover, and it is expected to have the opportunity in solving the miscompilation problem to the utmost extent. Based on such an approach, the key technologies for a trustworthy compiler from a synchronous data-flow language (Lustre as the prototype) to a sequential imperative language (C as the prototype) have been studied. The challenge lies in the great difference between the source and target languages, where the source language has the features of clock synchrony, data-flow, concurrency, stream data object, etc., while the target language is instead with the sequential and control-flow features. Among the similar researches, there is no reported result so far for the key translation stages. Recently, this research completed a formal verification for the whole compilation stages in the case of single clock. The related technologies will be taken into the development of a safety-level compiler in the country’s nuclear power system. The paper presents a survey on the trustworthy compiler with the research background, the architecture, the key technologies, the current status, and the future work.