一种基于语法变异的Lustre差分测试方法

本发明公开了一种基于语法变异的Lustre差分测试方法，属于软件工程和形式化验证技术领域，其技术要点是：首先识别Lustre语法中的不变量，例如逻辑表达式的等价变换，然后对Lustre语法树进行语义等价的变异操作，生成多个等价但语法结构不同的Lustre模型。接着，将原始Lustre模型和变异模型转换为C代码，并通过仿真测试对比输出结果的一致性，以判断Lustre模型在转换前后的行为一致性。该方法能够有效检测Lustre到C的转换过程中的潜在不一致或错误，利用Lustre语法树的语义等价变换来实现对Lustre模型的差分测试，以提高Lustre模型转换为C代码过程中的可靠性和测试效率。