同步建模语言代码生成器的高可信构造及其形式化验证方法

本申请涉及软件安全技术领域，特别涉及一种同步建模语言代码生成器的高可信构造及其形式化验证方法、装置、电子设备和介质，其中，方法包括：获取代码生成器生成的同步建模语言源程序；将同步建模语言源程序翻译至抽象语法树；将抽象语法树变换为中间表示，将当前中间表示变换为下一个中间表示；对于各变换过程本身进行形式化验证，直到同步建模语言源程序的所有语言特征的翻译过程验证完成，其中，形式化验证包括：每个中间表示形式化定义有满足语义确定性的操作语义，对当前中间表示变换过程证明语义保持性。由此，解决了相关技术仅支持部分语言特性，编译架构设计简单，形式化验证范围有限，难以满足对完整建模能力和高可信性的要求等问题。