软件学报

作者：于涛，王珊珊，徐芊卉，董晓晗，胡代金，罗杰，杨溢龙，吕江花，马殿富

单位：于涛，北京航空航天大学 计算机学院, 北京 10019111,王珊珊，北京航空航天大学 计算机学院, 北京 10019102,徐芊卉，北京航空航天大学 计算机学院, 北京 10019103,董晓晗，北京航空航天大学 计算机学院, 北京 10019104,胡代金，北京航空航天大学 软件学院, 北京 10019105,罗杰，北京航空航天大学 计算机学院, 北京 10019106,杨溢龙，北京航空航天大学 软件学院, 北京 10019107,吕江花，北京航空航天大学 计算机学院, 北京 10019108,马殿富，北京航空航天大学 计算机学院, 北京 10019109

关键词：同步数据流语言;经过验证的编译器;形式化验证;Lustre语言

基金：国家重点研发计划(2022YFB4501900)

同步数据流语言Lustre是安全关键系统开发中常用的开发语言, 其现存的官方代码生成器和SCADE的KCG代码生成器既没有经过形式化验证, 对用户也处于黑盒状态. 近年来, 通过证明源代码和目标代码的等价性间接证明编译器的正确性的翻译确认方法被证明是成功的. 基于下推自动机的编译方法和基于语义一致性的验证方法, 提出Lustre语言可信编译方法, 能够将Lustre语言转换为C语言并进行形式化验证以保证编译的正确性, 并使用Isabelle对翻译转换过程进行严格的正确性证明.

来源：2025年第8期

《软件学报》期刊编辑部

查看软件学报杂志2025年第8期