实时系统可预测性形式化验证中时序异常的定义和检测过程

实时系统可本杰明·宾德引用此版本：本杰明·宾德实时系统可预测性形式化验证中时序异常的定义和检测过程。嵌入式系统巴黎萨克雷大学，2022年。英语NNT：2022UPASG086。电话：03959710HAL Id：tel-03959710https://theses.hal.science/tel-039597102023年1月27日提交HAL是一个多学科的开放获取档案馆，用于存放和传播科学研究文件，无论它们是否已这些文件可能来自法国或国外的教学和研究机构，或来自公共或私人研究中心。L’archive ouverte pluridisciplinaire博士论文集NNT：2022UPASG086的定义和检测程序实时系统可预测性形式化验证的时序异常温度系统预测形式验证的温度异常巴黎萨克雷大学博士论文École doctorale n 1580：Sciences et technologies de博士学位：信息学研究生院：Informatique et sciences du NumériqueRéférent：Faculté des sciencesThèse préparée àParis-Saclay，CEA），le co-encadrement deBelgacem BEN HEDIA，ingénieur-chercheur，LIST（université Paris-Saclay，CEA），et le co-encadrementdeFlorian BRANDNER，enseignant-chercheur，LTCI（institut polytechnique deParis，Télécom Paris）Thèse soutenue à Paris-Saclay，le 13 décembre 2022，par本杰明·宾德陪审团组成陪审团成员的自由发言Alain FINKEL总统巴黎-萨克雷大学校长Stephan MERZ特别报告员de Lorraine）Christine ROCHANGE报告员图卢兹三世（Paul Sabatier）Claire PAGETTI研究工程师，ONERA（ISAE-SUPAERO）用于实时系统可关键词：时序异常，实时系统，形式化验证，模型检测，无序流水线，TriCore翻译后摘要：实时系统的定时行为-这些TA。我们还提出了一个专门的实例项目往往是通过时序分析，无序管道的概念进行验证。我们评估了在我们随后的对illustra-（TA）的检测过程中由于定时异常而受到危害的时间。 一个反直觉的TA表现在 示例和标准基准，显示 局部加速最终导致全局减慢，这允许精确地捕获TA。当局部减速时，系统的复杂性要求它们的减速导致更大的全球减速。时序分析能够处理大的结果，而反直觉的TA则威胁着可靠的状态空间。一种解决方案是执行时序分析的一致性/可扩展性，系统分析的工具，特别是受到自动检测威胁的工具不存在。我们设立了一个联络小组。我们推进他们的研究，通过显示-统一的正式框架，系统地评估- ING如何一个专门的抽象可以适应TA的定义，得出结论，缺乏一个工业处理器，通过建模的时间-一个实际的定义，主要是由于缺乏这样的硬件的相关功能与appropri-本地和全球的时序效应之间的关系。 减少吃。 我们还说明了从这个类，我们解决这些关系，通过因果关系，TAs如何验证策略可以用来-我们进一步使用，以修订病房的形式化获得TA模式。标题：温度异常检测的定义和程序，以验证温度系统的预测性Mots-clés ： Anomalies temporelles ， systèmes temps-réel ， vérification formelle ， vérification demodèles，pipeline out-of-order，TriCoreRésumé：Les systèmes temps-réel sont souvent instance des notions spécialisée pour les pipelinesvalidés par des analyses temporelles，whi sont mises out-order. Nous évaluons notre procédure de enpéril par desanomalies temporelles（AT）. Une détection subséquente sur des applicles illustrat-ATcontre-intuitivea lieu quand une accélération ifs et bancs de tests，montrant qu在是的，他是重要的选举人。由于AT的反直观性意味着Une solution est de realiser des analysescom-bien-fondé ou la flexibilité des analyses，il我们要不断学习数学。我们提出了一个结构形式，在montrant评论一个抽象的专门统一，以评估AT的定义，可以适应一个工业过程，cluant au manque我们照亮了本地和全球的温度。 Nous yrépondons aussi à partir de cette classe d我们也建议获得AT图案的西蒙·科曼德（英语：Simon CORMAND）（1930 - 2011）O推荐产品我知道这是一种与灭亡隔绝的阶段的同义词如果我能勇敢面对困难，做出前进的决定，我永远不会放弃，不会前进在法庭上，法官认为自己的想法是错误的我非常感谢我的校长马修，他为我保存了三年来最迫切的需要当然，我希望能找到一个这样的导演，因为他有能力提到你的作品;我有机会得到一个最好的导演，而且一直都可以没有米哈伊尔，我的导师，我也不会想到这一点，我知道我可以用科学和技术来帮助我的朋友：我知道我可以像晚上一样计算他的日子。他允许我把他的证词说出来让我把一个无辜的嫌疑人的证词说出来我的助手弗洛里安的规矩对我的工作有很大的好处。我们在一起工作的时候有很多时间，从我开始的时候：我做了一个真实的模拟。我对他的意见和他对我的调查结果的质疑感到非常满意。我很感激比利时人我的同伴我相信我们会相遇我也会无怨无悔地重新开始他陪同我参加了所有的活动，让我在准备食物时到达CEA，然后让我继续吃下去我也想到了我的同学和朋友，他们都做出了巨大的贡献。这三年都是在CEA度过的。点菜游戏 le midi，nombreuses discussions -我也会向所有能帮助我并允许我做好工作的CEA人员表示感谢我特别想到了DSCIN的实验室主任和秘书。我非常感谢Christian Gamrat，也是负责科学研究的部门，为了让他获得更多的机会。我很感激奈敏对他的支持，以及他对我的不信任，因为他说了，我就走了谢谢她我以前见过两次。Les derniers mois de rédaction puis finalisation de ma thèse sont doublés dema charge d'enseignement en CPGE.我非常感谢我的同学们，他们给我提供了资源，我没有帮助他们，或者他们没有做我临时雇员的工作5我 记 得 M. Alain FINKEL de m'avoir l'honneur de présider mon jury ， mereports Mme Christine ROCHANGE et M.斯蒂芬·梅尔兹让我注意听嗯，我认识我的父母，我的兄弟和我的祖母，他们都很有能力，而且基本上都是这样，只是在后勤方面。我得把注意力集中在我的工作和我的工作上7L法国音乐会aproblématique de la correction est importante lors du déspèmes temps-réel.在功能校正之外，温度相关系统的温度孔的作用是非常重要的，因为温度校正的结果在时间内会发生变化，执行条件。在我们的执行流水线程序中，温度控制产生组合材料，在我们的指令序列形成程序中，产生逻辑组合材料由于现代微体系结构主要包括各种性能优化机制，由于程序中没有明确的时间概念，因此需要确定入口和初始材料的执行时间，因此在同一微体系结构上同一程序的可能执行时间存在一个重要的离散性是的。此外，通过分析严格的温度，确定温度系统的作用是有效的，一般来说，目的是确定一个材料循环中的程序的执行温度。现有多种用于分析的方法，其中包括统计分析的一般方法;还可以引用基于测量或概率分析的方法。所有这些方法都是通过执行异常时间（AT）现象而在péril中使用的UneAT semanifeste au niveau我们区分AT的两种类型UneATcontre-intuitive a lieu quandune accélération locale （ sucès de cache par cample ） conduit à unrelentissement global，tandis quAT的理解和检测对于温度相关系统的分析至关重要重要的是，处理器标准在系统中使用，而这些处理器也是如此，通过各种优化机制，为了提供AT，它在检测过程中非常重要我们在这一领域的研究成果：微体系结构中的时间调节，方法的formelles pour la vérification matérielle，la littérature portant sur les outils demodélisation et vérification formelles，et enfin nous mettons特别是，我们建立了一个AT对比直观的不同定义的分类，这是AT+文件的分类，只有多个标准• 确定（形成）潜伏期和变异的标准;• 对时间分析中可能产生的结果的解释• l’existence d’une définition complémentaire pour les• et enfin我们的观点是，各种定义本质上是不同的，它们需要适当和比较，但同时也需要大量的既有理论著作，而不是具体的应用– d’où尽管存在反直觉的AT威胁到分析的良好基础或灵活性，但它并不存在用于系统检测的方法在外部，leurs定义formelles sont souvent incomplètes etillustrées applies- ment à travers des partiels。我们提出了一个统一的结构，以评估管道故障的一般模型中AT的现有定义Les principales contributions sontalors：• 一种系统的方法，加上精确的假设;• 一种材料混凝土模型（TLA+专用）;• uneévaluation comparative des différentes definitions par vérification demodèle（model checking）.我们可以通过以下方式来确定：任何定义都不适用于其他人，也不适用于检测各种各样我们的最大优势在于，我们主要解释了局部和全局的时间效应之间的关系。Nous y répondons par le concept important decausité，que nousutilisons pour revoir la formalisation de cesAT.我们提出了一般概念的系统，但也提出了管道故障的特殊概念的实例。Nous évaluons notre procédure dedetection subséquente sur des applications tests et bancs de tests，montrant qu此外，分析所产生的重要结果空间的制度本身就很复杂一个解决方案是真正的分析组成，在这样的条件下，温度控制系统得到partirdescontributionsindividuellesdedifférentscomposants. 通 过ATd'amplification对成分进行分析Nous faisons progresser作为对这种抽象的处理的预测，微体系结构beau-coup plus-cheap（双管道和层次记忆）需要一个通道到l 'échelle，这是一个功能模块化的空间。此外，工业标准的加工过程并不像一个可预测的加工过程那样容易被AT替代：问题并不在于排除AT，而在于探索AT变化的不同可能来源Les principales contributions sont alors：• 对我们研究案例的特殊抽象的结构和功能的扩展• 建立一个支持国家空间结构的系统，并考虑到微结构的特殊性（尤其是• 重新评估我们的程序复杂性;• une illustration，à partir de cette classe d'AT在此基础上，我们对我们工作的两个分支之间的相互作用和双向作用的优势进行了反思，以了解AT反直观概念的形式化（加上文件）以及在反测量中的验证策略，11R介绍实时系统受制于时间要求，这要求它们是可预测的。这意味着它们的定时行为必须在离线时可以很好地估计，然后才能运行。时序异常是一种阻碍实时系统可预测性的典型现象。 在理想的情况下，实时应用程序应该依赖于可预测的，无TA的体系结构。然而，COTS（商用现成）处理器越来越多地被采用的实时应用，以降低成本，并在混合关键系统中，从他们的性能增强器中受益。这些增强子很可能引入TA并危及可预测性。因此，在实时系统中可靠地检测TA是至关重要的。只有形式化的验证才能对TA的不存在提供安全保证或准确地识别它们的出现。由于实时系统运行专用软件，并且分析是针对执行的软件进行的，我们必须正式验证给定程序的执行是否没有TA，或者在默认情况下，准确地识别TA。在这种特定于代码的方法中，系统被视为硬件和软件组件的组合。因此，我们需要整合这两个方面的正式模型。 本文第一部分详细介绍了微体系结构的背景和案例研究，然后建立了形式化验证框架，并介绍了相关的工作。我们介绍了两种类型的TA，即反直觉TA，这是更多的文档，放大TA。在这部分之后，我们更具体地我们将在论文的下一部分讨论这些问题。实现TA的可靠检测的一个自然步骤包括处理该现象的正式定义。然而，对“时序异常”一词的通常解释仍然相当口语化，对潜在影响的理解往往只通过简单的例子来说明，这些例子给出了一些直观的理解。 现有的工作往往提供抽象的概念， 很难将这些定义应用到具体的应用中，更不用说对TA进行推理了。在本论文的第二部分，我们开发了一个无序管道的形式化模型[1]，并且我们根据这个具体的硬件模型仔细阅读了现有的反直觉TA的定义，展示了它们的局限性[2]。从这项工作的结果，我们提出了一个精确的和适用的形式定义的反直觉TA。从这个定义，我们实现了一个TA检测过程的实时系统。在本文的第三部分，我们提出了我们的新定义的反直觉TA和相关的检测程序[3]。不管TA的基本形式定义如何，我们已经研究了如何对架构进行适当的建模，以验证亲的时序特性gram执行，以及如何利用正式工具来导出TA模式，以插入对策。这项工作首先涉及扩增TA，对此不存在精确的检测程序-仅已知化学方法来检测它们-，但它也可能涉及反直觉TA，对此可以利用我们的新检测程序-该程序仅限于判决，并且可能是显示TA的单个反例。在本论文的第四部分，这是独立于前两个，我们说明了检测放大TA的工业案例研究[4]，我们提供了通用的算法来推导TA模式[5]。本文的最后一章总结了全文并展望了未来的工作。13贡献[1]Benjamin Binder等人 第11届欧洲嵌入式实时系统大会（ERTS）2022年[2]Benjamin Binder等人 将时间异常的定义付诸测试IEEE27thInternational Conference on Embedded and Real-Time ComputingSystems and Application（RTCSA）. 2021年，第102页。139-148。DOI：10. 110 9/RT CSA5285 9.2021.00024。[3]Benjamin Binder等人，《时序异常的正式定义中因果关系的作用》。IEEE第28届嵌入式和实时计算系统与应用国际会议（ RTCSA ） 。 2022 年 ， 第 22 页 。 91-102.DOI ：10.1109/RTCSA55878.2022。 00016。[4]Benjamin Binder等人 In：Formal Methods for Industrial CriticalSystems-25th International Conference ， FMICS 2020 ， Vienna ，Austria，September 2-3，2020，Proceedings.卷一二三四。计算机 科 学 讲 义 施 普 林 格 ， 2020 年 ， 第 151-169. DOI ：10.1007/978-3-030-58298-2_6。[5]Benjamin Binder等人，“Formal Modeling and Verification forAmplification Timing Anomalies in the Superscalar TriCoreArchitecture” 。 In： International Journal on Software Tools forTechnol-ogy Transfer（STTT）24（2022），pp. 第415-440页。ISSN：1433-2787。DOI：10.1007/s10009-022-00655-1。15内容I背景. 171背景. 212微架构案例研究333正式验证454相关工作59问题陈述79II反直觉时间异常的现有定义的局限性815定义的解释和建模6对定义的评估103III反直觉定时异常1137一个新的正式定义1178检测程序139IV定时异常模式检测的启发式方法1619扩增TA的检测16510 软件相关模式185展望201参考书目20317第一部分背景19N其次，介绍了本文的研究背景。我们目前的背景下，论文下降，硬件案例研究，我们保留，正式的方法和工具，我们使用的相关工作。所有这些因素使我们能够准确地说明我们在报告中概述的问题我们将在论文的下一部分详细阐述。内容1背景. 211.1实时系统211.1.1微处理器211.1.2从嵌入式系统到安全关键系统221.1.3可预测性231.1.4时间分析241.2管道271.2.1原则271.2.2危险和失速，静态/动态调度271.2.3单一问题/超标量管道281.3微架构中的时序异常291.3.1直观的定义291.3.2时序异常与时序分析311.4摘要：论文312微架构案例研究332.1经典有序流水线332.1.1管道描述332.1.2扩增指南示例TAs352.2TriCore微架构概述362.2.1TriCore微架构362.2.2计时行为372.3代表性的无序流水线模板412.3.1管道概述412.3.2执行功能422.3.3反直觉的传统模式