【摘 要】
：
近年来,嵌入式软件被广泛应用在一些安全关键领域中,嵌入式软件的需求也日益复杂,其中最为关键的就是需求中包括的实时规范。传统的时序逻辑语言如LTL、CTL等无法处理连续时间上实值信号的变化情况。因此,可以描述实值信号特性的STL成为了必要的选择。但是由于缺乏支持STL的工具,自动验证系统是否满足STL性质十分困难。另一方面,Simulink已被广泛应用于模型驱动的设计与开发中。但Simulink本身
论文部分内容阅读
近年来,嵌入式软件被广泛应用在一些安全关键领域中,嵌入式软件的需求也日益复杂,其中最为关键的就是需求中包括的实时规范。传统的时序逻辑语言如LTL、CTL等无法处理连续时间上实值信号的变化情况。因此,可以描述实值信号特性的STL成为了必要的选择。但是由于缺乏支持STL的工具,自动验证系统是否满足STL性质十分困难。另一方面,Simulink已被广泛应用于模型驱动的设计与开发中。但Simulink本身的验证能力十分有限,不支持验证STL性质。为了解决上述两个问题,我们研究了Simulink模型中STL性质的自动抽取和验证方法,以保证模型的安全和可信。本文主要的工作和贡献如下:1.首先我们提出了一个基于自然语言处理技术的从自然语言需求中自动抽取STL性质的方法。我们制定了一套详细的抽取规则,并设计实现了自动生成STL公式的算法。该部分工作可以保证需求和时序性质的一致性。2.基于UPPAAL时间自动机我们提出一个自动验证Simulink模型中STL性质的方法。我们对Simulink模型进行形式化建模,然后将STL性质和Simulink模型转换为UPPAAL时间自动机,由UPPAAL完成自动验证。我们基于符号执行设计的算法可以有效避免转换后的时间自动机出现状态爆炸问题。3.我们在两个工业Simulink模型案例上应用了我们的验证框架,实验结果表明了我们验证框架的可行性和有效性,从而为Simulink模型上STL性质的验证工作提供了重要参考。
其他文献
随着科学技术的发展以及在“中国制造2025“的工业化革新的背景下,精密制造业技术突飞猛进,各种设备制造朝向精密化发展,这就对各种设备关键工件的制造精度要求越来越高,如何对工件进行高精度质量检测成为一个亟待解决的课题。本课题针对通用工件的表面轮廓高精度实时测量的需求展开研究。本论文设计搭建了一个通用工件轮廓测量平台,控制系统采用A3200运动控制器,数据采集方面选用STIL光谱共焦传感器,并使用双频
随着互联网的发展网络上的信息越来越多,尝试从海量的冗余信息中挖掘出对用户来说有价值的信息,可以提高用户获取有用信息的效率;同时,从大量非结构化数据中获取结构化的知识,构建知识图谱,可以方便用户准确高效的查询相关信息。实体关系联合抽取技术可以有效的解决这个问题,将实体识别与关系抽取任务结合,减少两个任务间的误差传播造成的损失。对于具体运用来说,从文本中识别出实体和关系构建三元组,在知识图谱、信息检索
癌症是一个世界性的重大公共卫生难题,而肺癌在所有癌症中占比最大,严重威胁着人类健康。对肺癌进行早筛,进而对确诊的肺癌进行早期干预,可以有效降低癌症死亡率。因此,研究较为精确的计算机辅助检测系统用于辅助放射科医生进行肺结节筛查,提高诊断效率及准确率显得至关重要。高效精确的计算机辅助检测可以有效帮助放射科医生快速准确地发现肺结节区域,进而缓解医疗资源急剧紧缺的问题,提高肺癌患者的五年生存率。本文在3维
三维人体形状补全是计算几何分析和计算机视觉中的一个重要问题,随着三维形状捕获设备的发展,三维形状数据变得易于获取,但由于设备精度等因素的限制,得到的形状往往是破损的。在计算机动画设计过程中,若可以对破损的人体形状进行快速补全,则可以基于现实人体形状进行快速建模;同时,快速补全人体形状可以让自主无人系统以更高的精度感知人类的存在,提升人机协同效率。传统过程化补全方法依赖手工建立的几何和概率模型对破损
剩余污泥（waste activated sludge,WAS）是城市生产生活过程中产生的大宗有机固体废物,其产量年年攀升,给城市环境管理带来了巨大压力。剩余污泥兼具污染属性和资源属性特征,其科学处理与处置对于生态文明建设具有重大意义。因此,本论文针对“污泥处理与处置过程中脱水难度大、新兴污染物丰度高和资源转化效率低等”技术难题,系统开展了硫氧自由基（oxysulfur radical,OSR）预
纠错码使得通信系统具有检错和纠错的能力,从而保证了通信的可靠性。在纠错码理论的相关研究中,自正交码是一项十分重要的研究课题,在通信、数据存储以及密码学等领域有着广泛的应用。随着量子通信技术的发展,自正交码还被发现可以用于量子纠错码的构造,引起了诸多学者的研究兴趣。通常情况下,自正交码可以由线性码的正交包来构造。BCH码作为一类特殊的线性码,其结构清晰,纠错能力强,且构造方式较为灵活。因此,本文对B
硬件模型检查器是保证计算机硬件设计正确无误的工具之一。然而,硬件模型检查器本身作为一种软件,他自身也有可能存在着一些缺陷。这些缺陷或导致程序崩溃,或导致验证结果与实际不符。而使用人工撰写测试用例的方式去检查这样的缺陷,效率极其低下。因此,我们需要一种自动化的测试方法,来对硬件模型检查器进行测试。模糊测试是软件测试领域非常重要的自动化测试方法之一。它能够自动化生成随机的测试用例。模糊测试已经在多种类
三维电极生物膜反应器（3D-BERs）是一种新型的氢自养反硝化脱氮技术,无需额外投加电子供体,避免了二次污染。由于氢自养微生物在粒子电极界面挂膜时间较长,导致反应器启动较慢,初期脱氮效率不高,因此我们前期的研究中在3D-BERs中投加纳米α-Fe2O3,使之与微生物在粒子电极界面自组装形成纳米杂化生物膜,从而促进反硝化微生物的富集,加快反硝化的启动过程。目前仍有一些问题有待解决,如3D-BERs的
实体提取是指从文本中识别出具有特定意义的实体,关系提取是指判定实体与实体之间存在某种关系,最近热门的实体和关系联合提取的本质是在同一个模型当中同时对这两个任务进行训练。在生物医学上,实体和关系的提取对于疾病的治疗研究具有很大的应用价值。本文依托以“COVID-19爆发”为基础构建突发公共卫生事件医疗综合决策智能辅助平台课题,目的是从生物医学文本中提取出与某种疾病或病毒相关的基因通路,为疾病的治疗方
随着印制电路板（PCB）行业的蓬勃发展,传统的PCB质量检测方法的检测效率已经很难适应现在的PCB生产需求,近年来,基于机器视觉技术的自动光学检测系统（AOI系统）逐渐成为主要的PCB质量检测方法。常见的PCB缺陷分为两类,第一类缺陷包括划痕、异物、元件贴反等2D范围内的缺陷;第二类缺陷包括走线弯曲偏移、走线交叉等3D范围内的缺陷。为了检测第一类缺陷,AOI系统使用高分辨率但视野非常有限的工业相机