一种基于形式化语言与概率模型的中断程序验证方法

本发明公开一种基于形式化语言与概率模型的中断程序验证方法，所述方法包括如下步骤：建立形式化语言模型语法；建立形式化语言模型语义；使用Maude编程语言对形式化语言模型实例化，进而建立验证系统；将待验证的嵌入式系统软件进行形式化编程；将待验证的嵌入式系统软件输入验证系统并得到验证结果。与现有技术相比，本发明通过建立一种形式化语言模型，并结合概率模型，能够对嵌入式系统软件运行进行形式化推导，全流程具备自动化能力，适用于所有嵌入式系统软件，运行分析结果全面准确，且能够计算出不同运行结果概率，从而能够推导、检验嵌入式系统软件的可靠性。