基于加权下推系统的中断验证系统

摘要

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