删除或更新信息,请邮件至freekaoyan#163.com(#换成@)

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

本站小编 Free考研考试/2022-01-02

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



Abstract:The interrupt mechanism is a commonly used means to ensure real-time response to various asynchronous events in embedded systems and various real-time operating systems. Nested interrupts are likely to occur when the request of more urgent interrupt event arise while processing a less urgent one. Modeling and verifying such systems are challenging tasks. This paper proposes an approach to modeling and verifying systems with nested interrupts. First, MSVL (modeling, simulation and verification language) is extended to model such systems by defining an interrupt statement using projection temporal logic (PTL). Then, methods of modeling different nested interrupt systems using the interrupt statement are studied. Next, the MSV toolkit is extended to model, simulate, and verify MSVL programs with nested interrupts automatically. Finally, a case study is given to demonstrate how the proposed method works.



PDF全文下载地址:

http://jos.org.cn/jos/article/pdf/5472
相关话题/系统 逻辑 语言 操作系统 工作

  • 领限时大额优惠券,享本站正版考研考试资料!
    大额优惠券
    优惠券领取后72小时内有效,10万种最新考研考试考证类电子打印资料任你选。涵盖全国500余所院校考研专业课、200多种职业资格考试、1100多种经典教材,产品类型包含电子书、题库、全套资料以及视频,无论您是考研复习、考证刷题,还是考前冲刺等,不同类型的产品可满足您学习上的不同需求。 ...
    本站小编 Free壹佰分学习网 2022-09-19
  • 机器人关节通信总线系统的建模与验证
    摘要:高速串行现场总线(controllerareanetwork,简称CAN)被广泛部署到机器人通信系统中.而服务机器人任务具有并发性和高实时性的特点,因此,如何根据总线协议规范和应用需求精化设计模型,保证系统设计的正确性和实时性要求,避免设计阶段的漏洞十分必要.针对传统方法的局限性,提出使用形式 ...
    本站小编 Free考研考试 2022-01-02
  • 医学影像计算机辅助检测与诊断系统综述
    摘要:计算机辅助检测/诊断(computer-aideddetection/diagnosis,简称CAD)能够提高诊断的准确性,减少假阳性的产生,为医生提供有效的诊断决策支持.旨在分析计算机辅助诊断工具的最新发展.以CAD研究较多的四大致命性癌症的发病医学部位为主线,按照不同的成像技术和病类,对目 ...
    本站小编 Free考研考试 2022-01-02
  • 基于同态加密系统的图像鲁棒可逆水印算法
    摘要:同态加密技术可用于保护数据隐私并允许对密文数据进行算术操作,在云计算安全上有着很好的应用前景.针对云计算中的隐私保护和数据安全等问题,提出了一种基于同态加密系统的图像鲁棒可逆水印算法,主要思想为:(1)对原始图像进行分块和利用Paillier加密系统进行加密得到密文图像;(2)在加密域中,通过 ...
    本站小编 Free考研考试 2022-01-02
  • 基于创意序列学习的艺术风格学习与绘制系统
    摘要:在众多传统艺术绘画形式中,笔触是被现代计算机绘画工具(GIMP、Photoshop和Painter)普遍采用的形式之一.创新性地提出了服务于非真实感渲染AI辅助艺术创作系统(A4).系统能够实现自动生成特定艺术家风格的笔触效果.该系统在强化学习框架下,主要进行以下研究工作:(1)提出基于PGP ...
    本站小编 Free考研考试 2022-01-02
  • 分布式图处理系统技术综述
    摘要:图作为一种基本的数据类型,是对现实世界中对象及其关联关系的一种抽象.现实中,许多科学问题都可以被模型化为图的问题,因此,对图数据进行分析非常重要.图数据分析在语义Web分析、社交网络、生物基因分析以及信息检索等领域有着广泛的应用.随着移动互联、物联网等信息技术的发展,图数据的规模处于持续增长的 ...
    本站小编 Free考研考试 2022-01-02
  • 经验研究中情景感知需求获取与建模系统文献综述
    摘要:情景感知(contextaware)的应用是当前的一个研究热点,但是,由于情景的复杂性和不确定性,如何获取这些应用的需求面临着巨大挑战,需求工程领域出现了大量的研究来解决这一挑战.使用系统文献综述(systematicliteraturereview)的方法首先分析了不同情景维度对需求获取与建 ...
    本站小编 Free考研考试 2022-01-02
  • 近16年暖季青藏高原东部两类中尺度对流系统(MCS)的统计特征
    摘要摘要:利用日本高知大学提供的逐小时分辨率静止卫星云顶黑体亮温(TBB)资料,使用模式匹配算法对2000~2016年(2005年除外)暖季(5~9月)青藏高原东部的两类中尺度对流系统(MCS)进行了识别和追踪,并利用人工验证订正了结果。基于此,利用NOAA的CMORPH(ClimatePredic ...
    本站小编 Free考研考试 2022-01-02
  • 基于慢特征分析对连续系统的外强迫提取
    摘要摘要:外强迫随时间的变化对于非平稳系统的影响十分重要,如何从该系统中重构或提取外强迫信息则成为研究其中动力学特征的关键所在。本文基于慢特征分析方法(SlowFeatureAnalysis,SFA)以连续系统(改变的Lorenz系统)为参考模型,分别讨论在周期型强迫、减弱的周期型强迫、指数衰减型强 ...
    本站小编 Free考研考试 2022-01-02
  • 一个适用于地球系统模式(<bold>CAS-ESM</bold>)的在线气溶胶与大气化学分量模式(<bold>IAP-AACM</bold>)的发展与评
    摘要摘要:地球系统模式是研究全球气候与生态环境变化问题的重要工具,气溶胶与大气化学模式负责为其中的大气环流模式提供与气候效应有关的气态化学物质和气溶胶成分。本文在全球嵌套网格空气质量预报模式系统的基础上发展了一个适用于中国科学院地球系统模式(CAS-ESM)耦合计算的气溶胶与大气化学分量模式(IAP ...
    本站小编 Free考研考试 2022-01-02
  • 地球系统模式中植被净初级生产力百年尺度时空变化及其与气候的关系
    摘要摘要:利用6个地球系统模式模拟的植被净初级生产力(NPP)对1901~2005年NPP时空变化进行了研究,并结合气候因子分析了NPP的变化与气温和降水的关系。结果表明:(1)近百年来全球NPP呈现上升趋势,模式集合平均的趋势系数为0.88,通过了99.9%的信度检验;北半球的趋势比南半球明显。( ...
    本站小编 Free考研考试 2022-01-02