The synchronous dataflow language Lustre is commonly used in the development of safety-critical systems. However, existing official code generators and the SCADE KCG code generator have neither been formally verified nor are they transparent to users. In recent years, translation validation methods that indirectly verify the correctness of compilers by proving the equivalence of source and target codes have been shown to be successful. This paper proposes a trusted compilation method for the Lustre language, based on a pushdown automaton compilation approach and a semantic consistency verification method. It successfully implements a trusted compiler from Lustre to C and rigorously proves the correctness of the translation process using Isabelle.
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.