实时执行生成方法的研究与应用

一种实时执行生成方法卡布兰·杜桑·戈蒂埃·蒂戈里引用此版本：卡伯兰·杜桑·戈蒂埃·蒂戈里。实时执行程序生成方法。自动化/机器人。南特中央学校，2016年。法语。NNT：2016ECDN0019。电话：02990618HAL ID：电话：02990618https://theses.hal.science/tel-02990618提交日期：2020年HAL是一个多学科的开放存取档案馆，用于存放和传播科学研究论文，无论它们是否被公开。论文可以来自法国或国外的教学和研究机构，也可以来自公共或私人研究中心。L’archive ouverte pluridisciplinaire博士论文为获得以下文件而提交的备忘录南特中央学院博士学位布列塔尼卢瓦尔大学印章下卡伯兰·杜桑·戈蒂埃·T·伊戈里博士学院：信息科学与技术学科：计算机科学与应用，CNU 27科研究单位：IRCCyN，UMR65972016年11月24日支持一种实时生成执行者的方法陪审团主席：M. Gilles MULLER，INRIA-LIP 6研究总监，报告员：Claire PAGETTI女士，图卢兹ONERA HDR研究工程师M. Emmanuel GROLLEAU，大学教授，ISAE-ENSMA，普瓦捷考试员：M.Hervé MARCHAND，雷恩INRIA研究员M. Jean-Luc BÉCHENNEC，南特CNRS-IRCCyN研究员博士生导师：M. 奥利维尔·H. ROUX，南特中央学院大学教授-IRCCyN，南特3致我的母亲Hélène EBA，致我的女儿Emmanuella TIGORI，致Ursule Korandji，致我的兄弟姐妹，也致我已故的5谢谢你首先，我衷心感谢我的主管Jean-Luc BÉCHENNEC和Olivier- Henri ROUX，他们为本论文的完成做出了巨大贡献。更不用说塞巴斯蒂安·福库了，他的相关想法使他他们的建议，他们的支持，特别是他们先进的科学知识，使我既获得了信心，并获得了所有必要的技能，这篇论文的顺利进行我要感谢巴黎LIP6的研究主任Gilles Muller先生，感谢他让我有幸担任我的论文评审团主席还要感谢图卢兹ONERA的研究工程师和HDR Claire PAGETTI女士我还要感谢雷恩INRIA的研究员Hervé MAR- CHAND先生我要感谢我的论文伙伴路易斯-玛丽·吉维尔、阿梅尔·曼吉安、贝特朗·米安奈和路易斯·菲波·菲蒂梅，以及IRCCyN的所有其他博士生，我与他们分享了美好的我还要感谢IRCCyN实时系统团队的所有成员，感谢他们让我感谢我所有的朋友的支持和所有的美好时光。我感谢我所有的家庭成员，特别是我的母亲，她的精神支持和我的兄弟，她的建议。最后，我要感谢我未来的妻子厄休拉，她愿意和我一起踏上这段旅程。目录一般介绍15第一章操作系统的配置1.1定义201.1.1范式201.1.2粒度为211.1.3完整性211.2配置类型211.2.1静态配置221.2.2动态配置241.3发展范式251.3.1面向对象编程261.3.2面向主题的编程281.3.3面向方面的编程291.3.4专用语言（DSL）311.4结论32第二章蹦床，一个实时操作系统2.1OSEK/VDX标准362.1.1OSEK 36操作系统的体系结构2.1.2任务管理372.1.3调度策略2.1.4应用程序2.1.5中断的处理402.1.6事件的机制412.1.7资源管理422.1.8警报452.2AUTOSAR：软件体系结构标准2.2.1软件体系结构462.2.2AUTOSAR46中的配置2.3蹦床462.3.1演示文稿462.3.2单核蹦床48的结构2.3.3多核蹦床架构512.4结论528目录第三章建模3.1形式主义的工具563.1.1有限自动机563.1.2扩展有限自动机563.1.3扩展有限自动机网络3.1.4使用扩展有限自动机抽象3.1.5可达性和边界583.2建模原则593.2.1分支机构的建模593.2.2循环建模593.2.3函数调用的建模3.3适用于UPPAAL603.3.1UPPAAL：用于实时603.3.2时间的处理623.3.3使用UPPAAL63的建模规则3.4用于单核64架构的蹦床模型3.4.1对象和变量643.4.2内核建模653.4.3服务建模683.4.4与定时器70相关的硬件中断建模3.5用于多核架构的蹦床模型713.5.1内核建模713.5.2服务建模723.6应用程序模型3.7型号73的特性3.8结论75第四章操作系统的形式化综合4.1方法784.1.1模型794.1.2形式综合794.1.3代码81的生成4.2开发的工具834.2.183型合成器4.2.2代码生成器844.3案例研究854.4结论88第五章正式核查5.1正式验证技术905.1.1型号检查905.1.2静态分析915.1.3测试91目录95.2OSEK/VDX92合规性的正式验证5.2.1测试用例935.2.2测试序列935.2.3测试套件945.2.4示例945.3使用通用观察员对OSEK/VDX合规性进行正式验证.........................................................5.3.2观察员985.3.3案例研究1025.4结论105一般结论和展望107出版物109参考书目110图表1从蹦床操作系统代码中提取，包括用于编译时配置的预处理器指令。.............................161.1不同配置类型的说明[Frö01]221.2以类图的形式表示蹦床调度程序. ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...... ... ... ... ... ... ...271.3受试者组成281.4基于面向对象编程的模块化301.5基于方面30编程的模块化1.6从专用语言到通用语言的转换1.7通过专用语言实现操作系统的专业化2.1扩展任务的状态图2.2基本任务的状态图2.3先发制人的订购..................................................................................................................... 392.4非优先排序。..................................................................................................................................402.5按事件同步422.6优先级反转示例2.7使用信号量的互锁示例2.8在任务调度中使用资源......................................................................................................... 452.9软件体系结构472.10 Trampoline47的装配和配置2.11 单核蹦床结构[BBF15]482.12 系统调用管理器的结构[BBF15]492.13 报警管理的数据结构502.14 准备好的任务列表的结构512.15 多核蹦床架构522.16 在多核蹦床53上执行任务的场景3.1用扩展有限自动机表示......................................................................................................... 593.2由扩展有限自动机表示的3.3函数调用的描述（左边是函数a，右边是函数b）：共享变量x允许调用自动机被阻塞，直到被调用自动机完成执行。对函数a建模的自动机在对函数b建模的自动机的执行结束之后恢复其执行。行动h!和H？ 转换两个自动机的同步点.................... 603.4模型65中任务的静态和动态描述符3.5模型中指针的表示................................................................................................................. 653.6内核函数tpl_Terminate66的建模12图表3.7仪表管理器型号683.8模型（左）和蹦床（右）中的tpl_get_proc函数代码693.9 TerminateTask API模型3.10 任务终止服务模型3.11 计时器型号703.12 多核71情况下的tpl_Terminate函数模型3.13 多核72中tpl_Terminate_task_service函数的模型3.14 应用程序的建模4.1我们的方法在蹦床编译链中的定位。784.2操作系统的形式化综合4.382型合成4.4根据tpl_Terminate83函数的简化模型生成的代码4.5操作系统的合成器体系结构4.6任务的类型：Task_ACC_IDM875.1模型检查过程905.2符合性测试925.3测试序列模型955.4测试序列观察器模型5.5正式验证流程975.6测试用例（属性）t98的一般观察器Obs（t）5.7对tpl_Terminate_task_service函数的初始模型的更改995.8观察器模型示例5.9与中断相关的测试用例示例1015.10 摄像机控制和跟踪系统型号104图片列表4.1ADAS 86应用程序的优先级、启动和任务周期4.2操作系统的综合结果5.1测试用例935.2测试序列93一般简介一般背景在过去的三十年里，嵌入式系统极大地提高了人类的生活质量它们的重要性在工作生活和工业环境中都能感受到。从智能手表、家用电器等小型互联对象到根据定义，嵌入式系统是用于执行特定任务的自主电子和信息技术系统的集合例如，在汽车领域，作为一种安全措施，车辆配备有自动制动系统考虑到它们的发展，这些系统需要越来越多的软件和硬件功能，这取决于开发的新应用，这导致复杂性的增加然后，嵌入式系统必须实现所有期望的功能，在计算时间方面更有效，并且在给定时间内执行分配给它们的任务（例如，实时系统在汽车领域新车在70个电子控制单元（ECU）中集成了约270种功能，随着自动驾驶汽车的发展，这一数字将在未来继续增长所有这些复杂性的管理都是由嵌入式系统的一个组件来完成的，该组件充当操作系统由于嵌入式系统通常是小型的并且具有有限的资源，因此操作系统不能集成用于广泛应用的然而，要做到这一点，这种大小限制的一个解决方案是在操作系统中只嵌入给定应用程序实际需要的所有这样做的优点是优化了操作系统占用的存储器空间，提高了嵌入式系统的性能，并降低了错误行为的可能性操作系统的16一般简介FUNC（Stt ttusType，OS_CODE）tpl_actvate_task_service（CONST（tpl_task_id，AUTOMATIC）task_id）{...# ifTask_COUNT > 0IF_NO_EXTE NDE D_ERR OR（result）result=tpl_activate_task（task_id）;if（result==（tpl_status）E_OK_AN D_SCHE DULE）{tpl_scheddle_from_running（）;#ifWITH_SY STE M_CAL==NOif（tpl_kern. NEED_SWITCH! =NO_NEE D_SWITCH）{tpl_switch_contex t（&（tpl_kern.s_old->context），&（tpl_kern. s_running->context））;}#endifIF_NO_EXTE ND ED_ERR OR_E N D（）#endif...}— 可配置：以便仅嵌入给定应用程序— 可扩展性：在给定应用程序需要新功能的程度上（避免在实现新功能时完全重新实现有问题由于前面提到的原因，操作系统被开发为可配置的。资源有限的嵌入式系统的操作系统配置这种相对简单的配置大量使用了操作系统源代码中的预处理器指令L’extrait du code de la fonction图1在例如，如果Task_COUNT变量的值大于0，则在编译时操作系统将考虑函数的完整代码由于几个原因，这种类型第一个原因是预处理器因此，条件表达式中可能存在错误，并且在编译过程中选择了错误的代码，这可能会17第二个原因是在这对于诸如Frama-C [CKK + 12]之类的静态分析工具来说也是一个此外，预处理器指令表达式中的错误因此，必须在操作系统的验证和确认阶段检测到这些错误然而，只有静态分析技术才操作系统代码的正确性证明死代码很难被检测到，不应被视为无害的，因为它会影响D’un目标L’objectif为此，我们提出了一种基于正式模型的操作系统配置在这种类型由于几个原因，这样的方法是有首先，该模型是可执行的，并且提供了模拟操作系统的可能性。其次，如果模型设计正确，则可以使用该模型的静态分析来确定在操作系统运行时不需要遍历的所有分支。这使得删除实际上翻译死代码的所有分支变得更容易。因此，所得到的（修剪的）模型可用于生成操作系统的源代码因此，配置或合成的操作系统第三，模型验证技术可用于证明修剪模型的正确这种类型的检查提供了操作系统行为在配置过程中不受影响的证据这将贡献论文的贡献包括两个主要方面。第一个轴处理基于其模型的操作系统的配置或合成，第二个轴处理操作系统的操作系统的正式配置或合成18一般简介用于应用程序的专用实时从此模型支持相应操作系统的所有特征，L’application在所获得的模型（应用程序+操作系统）上，执行可访问性搜索以检测所有未覆盖的路径和不可访问的状态。这些路径实际上表示永远不会为该应用程序执行的操作系统代码部分。所有这些路径都将自动从模型中删除。在此之后，获得仅包含可行路径的专用模型，并且该模型描述执行应用程序所需的代码最后，从专用模型，通过代码生成器生成对应的专用操作系统的完整代码这种方法加快了专门操作系统的开发过程，并允许在部署之前对其操作系统的正式验证第一种方法是根据OSEK/VDX规范证明操作系统的一致性该方法使用OSEK/VDX一致性测试的原理，其中在操作系统上运行测试序列以观察其行为。 在这种方法中，所有的测试序列都被建模，然后应用于操作系统模型。在此检查之后，确定操作系统模型的OSEK/VDX符合性，并根据实际操作系统的OSEK/VDX符合性进行第二种方法允许验证OSEK/VDX操作系统的一致性，实际上，OSEK/VDX规范的所有因此，这些观察器观察给定应用程序的操作系统行为，并手稿的组织手稿组织如下：— 第1章首先定义了配置的概念以及不同类型的配置，即静态配置和动态配置最后，介绍了现有的配置技术。— 第2章介绍了蹦床操作系统的情况，我们在— 第3介绍了用于操作系统建模的形式体系结构，并介绍了— 第4章介绍了操作系统的综合过程以及驾驶员辅助应用程序的— 第5章介绍了在我们的工作过程中开发的两种验证方法，用于从正式模型验证操作系统是否符合OSEK/VDX规范第一章操作系统的配置总结1.1定义201.1.1范式201.1.2粒度为211.1.3完整性211.2配置类型211.2.1静态配置221.2.2动态配置241.3发展范式251.3.1面向对象编程261.3.2面向主题的编程281.3.3面向方面的编程291.3.4专用语言（DSL）311.4结论32Cechapitrepresenteteun状态的艺术t el 实际上，它提出了在系统配置期间要考虑的不同标准。d’exploitation, 最后，介绍了几种开发可配置操作系统的技术