科研之友
微信
新浪微博
Facebook
分享链接
摘要
本发明公开了一种利用在线模型检验的嵌入式实时操作系统验证方法,首先在基于事件总线的嵌入式实时操作系统的源代码中进行插桩,并从源代码中抽象出其行为模型；当操作系统在运行时触发监控点,将监测到的具体状态通过映射函数转化为抽象状态,该抽象状态用来指导行为模型的运行,从而实现了操作系统的实现层和模型层的相结合,通过即时检验算法检验操作系统在运行期间的行为模型是否满足抽取的性质,并预测未来k步行为模型的正确性；若检查出错误,则表示当前执行路径中存在潜在错误,并立即通知正在运行的操作系统。本发明应用到操作系统的形式化验证中,模型层的错误预示着在系统执行层可能也会产生错误,从而确保操作系统在运行中的正确性。
- 单位
