本发明公开了一种基于优化K归纳的机载控制软件形式化验证方法,实现步骤是,构建包括顺次连接的编译期特性代码剥离建模单元、传感器输入数据赋值单元、数据流依赖的形式参数消除单元和函数提取单元的抽象建模模块,并通过抽象建模模块构建机载控制软件源代码的模型函数,将机载控制软件建模为模型函数集,通过优化传统K归纳算法,并基于优化K归纳算法获取机载控制软件形式化验证结果。本发明可用于对机载控制软件进行安全性形式化验证,由此提高了机载控制软件的安全性。
科研之友
微信
新浪微博
Facebook
分享链接
