基本信息来源于合作网站,原文需代理用户跳转至来源网站获取       
摘要:
在嵌入式系统和各类操作系统中,中断机制是确保实时响应各类异步事件的重要方法.通常在处理一个中断事件的过程中,往往会有更紧迫的中断事件请求响应,因而发生中断嵌套.建模并验证嵌套中断系统是具有挑战性的工作.提出一种建模和验证嵌套中断系统的方法.首先,提出基于投影时序逻辑(projection temporal logic,简称PTL)的定义,并将这种定义推广到包含任意多中断事件的中断系统上,从而得出嵌套中断系统基于投影时序逻辑的形式化模型;其次,使用投影时序逻辑定义的基本中断语句扩充建模仿真和验证语言(modeling,simulation and verification language,简称MSVL),并扩展MSVL语言的解释器,使其可以对嵌套中断系统进行建模仿真和验证;最后,通过一个实例展现所提出方法的正确性和实用性.
推荐文章
一种有效的中断输入和LED动态显示方法
中断输入
动态显示
全零状态
搜索状态
嵌套分割算法:一种新的并行随机优化算法
嵌套分割算法
系统优化
算法综述
一种高性能 DS P中断系统的研究与设计
中断系统
数字信号处理器
中断向量表
中断优先级
外设控制处理器
一种基于领域分析的面向Agent需求建模方法
agent-oriented
特征
领域分析
软件复用
内容分析
关键词云
关键词热度
相关文献总数  
(/次)
(/年)
文献信息
篇名 一种嵌套中断系统的建模和分析方法
来源期刊 软件学报 学科 工学
关键词 嵌套中断系统 投影时序逻辑 MSVL(modeling,simulation and verification language) 形式化建模与验证
年,卷(期) 2018,(6) 所属期刊栏目 形式化方法的理论基础专题
研究方向 页码范围 1670-1680
页数 11页 分类号 TP311
字数 7417字 语种 中文
DOI 10.13328/j.cnki.jos.005472
五维指标
传播情况
(/次)
(/年)
引文网络
引文网络
二级参考文献  (0)
共引文献  (0)
参考文献  (7)
节点文献
引证文献  (1)
同被引文献  (5)
二级引证文献  (0)
1969(1)
  • 参考文献(1)
  • 二级参考文献(0)
1994(1)
  • 参考文献(1)
  • 二级参考文献(0)
2007(1)
  • 参考文献(1)
  • 二级参考文献(0)
2008(2)
  • 参考文献(2)
  • 二级参考文献(0)
2016(2)
  • 参考文献(2)
  • 二级参考文献(0)
2018(0)
  • 参考文献(0)
  • 二级参考文献(0)
  • 引证文献(0)
  • 二级引证文献(0)
2020(1)
  • 引证文献(1)
  • 二级引证文献(0)
研究主题发展历程
节点文献
嵌套中断系统
投影时序逻辑
MSVL(modeling,simulation and verification language)
形式化建模与验证
研究起点
研究来源
研究分支
研究去脉
引文网络交叉学科
相关学者/机构
期刊影响力
软件学报
月刊
1000-9825
11-2560/TP
16开
北京8718信箱
82-367
1990
chi
出版文献量(篇)
5820
总下载数(次)
36
总被引数(次)
226394
论文1v1指导