一种嵌套中断系统的建模和分析方法

来源：软件学报杂志2018年第6期北京时间：

作者：崔进,段振华,田聪,张南

单位：崔进，ISN 国家重点实验室(西安电子科技大学), 陕西 西安 710071;西安电子科技大学 计算理论与技术研究所, 陕西 西安 71007111,段振华，ISN 国家重点实验室(西安电子科技大学), 陕西 西安 710071;西安电子科技大学 计算理论与技术研究所, 陕西 西安 71007102,田聪，ISN 国家重点实验室(西安电子科技大学), 陕西 西安 710071;西安电子科技大学 计算理论与技术研究所, 陕西 西安 71007103,张南，ISN 国家重点实验室(西安电子科技大学), 陕西 西安 710071;西安电子科技大学 计算理论与技术研究所, 陕西 西安 71007104

摘要：在嵌入式系统和各类操作系统中，中断机制是确保实时响应各类异步事件的重要方法.通常在处理一个中断事件的过程中，往往会有更紧迫的中断事件请求响应，因而发生中断嵌套.建模并验证嵌套中断系统是具有挑战性的工作.提出一种建模和验证嵌套中断系统的方法.首先，提出基于投影时序逻辑（projection temporal logic，简称PTL）的定义，并将这种定义推广到包含任意多中断事件的中断系统上，从而得出嵌套中断系统基于投影时序逻辑的形式化模型；其次，使用投影时序逻辑定义的基本中断语句扩充建模仿真和验证语言（modeling，simulation andverification language，简称MSVL），并扩展MSVL语言的解释器，使其可以对嵌套中断系统进行建模仿真和验证；最后，通过一个实例展现所提出方法的正确性和实用性.

关键词：嵌套中断系统;投影时序逻辑;MSVL (modeling,simulation and verification language);形式化建模与验证

基金资助：国家自然科学基金（61420106004，61732013，61572386）