基于形式化方法的同步数据流语言可信编译方法

本发明提供一种基于形式化方法的同步数据流语言可信编译方法，涉及同步数据流语言的可信编译领域，所述方法能够对输入的Lustre程序进行词法分析，语法分析和语义分析，进而使用下推自动机模型生成目标C代码；在实现编译器的基本功能之外，对于输入的语法单元和对应的目标C代码语法单元的语义等价性使用基于文法的形式化方法对翻译正确性进行验证。本申请简化了验证过程，并且保证了编译器的正确性，解决了现有技术中编译结果的正确性无法保证并且验证过程复杂的技术问题。