本发明公开了一种基于加权下推系统的中断验证系统,该系统包括目标代码建模模块、可达格局获得模块、可达格局遍历模块、当前格局回溯模块、结果输出模块。本发明的系统可以将实时系统的中断验证与加权下推系统相结合,以形式化的方式对实时系统中断进行验证,提高了验证的可靠性和鲁棒性；同一个模型下同时验证有关中断的时序逻辑、优先级反转、内存访问冲突以及超时问题,具有高效性,同时也节约了成本。
科研之友
微信
新浪微博
Facebook
分享链接
