-
题名一种嵌套中断系统的建模和分析方法
被引量：7
- 1
-
-
作者
崔进
段振华
田聪
张南
-
机构
ISN国家重点实验室(西安电子科技大学)
西安电子科技大学计算理论与技术研究所
-
出处
《软件学报》
EI
CSCD
北大核心
2018年第6期1670-1680,共11页
-
基金
国家自然科学基金(61420106004,61732013,61572386)
-
文摘
在嵌入式系统和各类操作系统中,中断机制是确保实时响应各类异步事件的重要方法.通常在处理一个中断事件的过程中,往往会有更紧迫的中断事件请求响应,因而发生中断嵌套.建模并验证嵌套中断系统是具有挑战性的工作.提出一种建模和验证嵌套中断系统的方法.首先,提出基于投影时序逻辑(projection temporal logic,简称PTL)的定义,并将这种定义推广到包含任意多中断事件的中断系统上,从而得出嵌套中断系统基于投影时序逻辑的形式化模型;其次,使用投影时序逻辑定义的基本中断语句扩充建模仿真和验证语言(modeling,simulation and verification language,简称MSVL),并扩展MSVL语言的解释器,使其可以对嵌套中断系统进行建模仿真和验证;最后,通过一个实例展现所提出方法的正确性和实用性.
-
关键词
嵌套中断系统
投影时序逻辑
msvl(modeling
simulation
and
VERIFICATION
language)
形式化建模与验证
-
Keywords
nested interrupt systems
projection temporal logic
msvl （modeling
simulation and verification language）
formal modeling and verification
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
