文献类型：期刊文章

作　　者：崔进[1,2] 段振华[1,2] 田聪[1,2] 张南[1,2]

CUI Jin;DUAN Zhen-Hua;TIAN Cong;ZHANG Nan(ISN State Key Laboratory （Xidian University）, Xi＇an 710071, China;Institute of Computing Theory and Technology, Xidian University, Xi＇an 710071, China)

机构地区：[1]ISN国家重点实验室(西安电子科技大学),陕西西安710071 [2]西安电子科技大学计算理论与技术研究所,陕西西安710071

出　　处：《软件学报》

基　　金：国家自然科学基金(61420106004,61732013,61572386)

年　　份：2018

卷　　号：29

期　　号：6

起止页码：1670-1680

语　　种：中文

收录情况：AJ、BDHX、BDHX2017、CSA、CSA-PROQEUST、CSCD、CSCD2017_2018、EI、IC、INSPEC、JST、MR、RCCSE、SCOPUS、ZGKJHX、ZMATH、核心刊

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

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

分 类 号：TP311]