嵌入式系统中代码移动性研究

嵌入式系统中的代码移动性盖伊·拉赫卢·吉肯引用此版本：盖伊·拉赫卢·吉肯。嵌入式系统中的代码移动性。自动化。东巴黎大学;雅温得第一大学，2018年。法语。NNT：2018PESC1112。电话号码：02123855HAL ID：电话-02123855https://theses.hal.science/tel-02123855提交日期：2019年HAL是一个多学科的开放存取档案馆，用于存放和传播科学研究论文，无论它们是否被公开。论文可以来自法国或国外的教学和研究机构，也可以来自公共或私人研究中心。L’archive ouverte pluridisciplinaire巴黎大学-东克雷泰伊数学与STIC博士学院算法、复杂性与逻辑实验室计算机科学博士论文吉肯·盖伊·拉卢嵌入式系统中的代码移动性由Fabrice Mourlin教授和Laure Pauline Fotso教授陪审团组成报告员：Pommereau Franck IBISCBobda Christophe TBA考官：Cervelle Julien LACL -东巴黎大学主任：Fabrice Mourlin LACL -东巴黎大学YAOUNDE I大学科学、技术和地球科学数学、计算机科学、生物信息学和应用I谢谢你。我很高兴终于完成了这篇论文的手稿。这也是一个机会，感谢所有的人谁帮助，支持或支持我在这个项目的整个过程中。我首先要感谢我的博士生导师Laure Pauline Fotso教授和FabriceMourlin教授。我特别感谢Fabrice Mourlin长时间的工作，他的工作充满挑战，而且总是很有回报。他对研究的热情是无穷无尽的。谢谢你把这篇论文真的很欠他。如果没有Sharif Mahmoudi博士的帮助，这项工作就不会成功。他的思想常常把我从我冒险进入的死胡同里拉出来。我知道我欠他很多，请我想对所有评审团成员表示最热烈的感谢。他们对这篇论文的仔细阅读以及他们的评论和建议有助于提高其质量。本论文分别在法国巴黎东克雷泰伊大学和喀麦隆雅温得第一大学的两个LACL和LIRIMA实验室进行。最重要的时刻是在LACL实验室的经历。LACL实验室提供了一个有利的研究环境，结合了卓越的科学质量和极大的用户友好性。因此，我要感谢还要感谢Cyril Dumont医生多次最重要的是，我感谢我的父母和朋友，他们支持我，支持我，鼓励在我的论文期间。最后，我要感谢她，她现在是我的妻子，她同意做出一些牺牲，使我能够在这些良好的条件下完成我的论文，也要感谢我的儿子卡尔·阿什尔和戈蒂埃·吉肯，他们尽了最大的努力，使我能够专注于我的工作II献给我已故的母亲Yona DelphineIII摘要近年来，随着为了提供与能耗和服务质量相关的问题的解决方案，我们将Cloudlet的概念定义为可以虚拟化设备及其嵌入式应用程序的本地云。然后，我们设计了一个基于这种与云计算和资源虚拟化相关的架构模式的分布式架构。这些定义使我们能够将我们的工作与其他移动应用程序驱逐方法进行比较D’autre part, un réseau de Cloudlets permet la protection de l’activité effectuée sur un périphériquemobile par la déportation d’applications embarquées dans une machine virtuelle s’exécutant dans laCloudlet, ainsi que le suivi des usagers dans leur这些定义指导我们通过高阶过程代数编写形式化规范它们允许基于Cloudlet概念计算不同案例研究的操作语义这些规范描述了适用于所有设备、传感器或致动器的虚拟设备组成的新视图。L’ensemble des équations obtenues constitue une définition formelle de référence non seulement pourle prototypage d’une Cloudlet mais aussi pour la construction de modèle基于我们的规范结构，我们为Cloudlet网络构建了一个定时自动机模型通过使用这项工作导致了技术选择，通过使用OSGi服务器，产生了这种分布式体系结构的原型 D’autre part, nousmettons en œuvre le principe de migration 这些结果验证了我们最初的选择，它们允许采取措施来定义在运行期间迁移到Cloudlet的成本，以及在用户移动期间对其进行监控。关键词：云计算，Cloudlet，迁移，驱逐，软件架构，OSGi，模型检查，原型IV摘要近年来，随着移动设备、虚拟化和云计算的出现，生态问题、能源管理、服务质量、安全标准和与我们的社会相关的许多其他方面都出现了新的问题。为了解决这些问题，我们将Cloudlet的概念定义为一个本地云，其中虚拟设备和嵌入式应用程序可以虚拟化。然后，我们基于与云计算和资源虚拟化相关的这种架构模式设计了一个分布式架构这些概念使我们能够将我们的工作与其他将移动应用程序卸载到Cloudlet中的方法进行比较。另一方面，Cloudlet网络通过将嵌入式应用程序卸载到Cloudlet中运行的虚拟机中，帮助保护移动设备上的活动，并在用户移动时对其进行监控。这些定义引导我们通过代数的高阶过程编写形式规范。它们基于Cloudlet概念促进了不同案例研究的操作语义的计算。这些规范为设计适用于所有设备、传感器或致动器的虚拟设备提供了新的愿景。这组方程构成了一个正式的定义，它不仅适用于Cloudlet的原型制作，也适用于构建定时自动机系统。根据我们的规范结构，我们为Cloudlets网络构建了一个定时自动机模型。利用模型检查技术，我们建立了临时属性，表明移动设备上移动应用程序的任何执行都可以卸载到依赖于给定软件体系结构的Cloudlet中这项工作导致了使用OSGi服务器的分布式体系结构原型的技术选择。第一个结果引导我们定义了移动应用程序的软件体系结构。第二，我们简单地介绍了迁移到Cloudlet邻居的原则。我们的测试验证了我们最初的选择，并证实了我们工作的假设。它们允许采取措施来评估在运行时卸载到Cloudlet的成本，以及在用户关键词：云计算，Cloudlet，迁移，卸载，软件架构，OSGi，模型检查，原型。V材料表感谢我摘要三摘要四图九表表十二列表引言1I.动机和贡献1II.论文内容3第1章：最新技术水平I.移动计算5.1.1.移动性的好处61.2.移动性的限制151.3.移动性需求19II.本地云222.1.定义和概念222.2.不同本地云的比较282.3.移动设备与Cloudlet之间的通信 29III.虚拟化333.1.移动设备和服务器的虚拟化343.2.数据存储的虚拟化353.3.网络设备的虚拟化353.4.应用程序虚拟化363.5.虚拟化解决方案系列36IV.合成38第2章：Cloudlet 40的监控体系结构I.Cloudlet 40的结构1.1.Cloudlets 41环境中的监视1.2.移动软件监控面临的挑战43II.软件监控的挑战442.1.使用2.2.监控设备48III.用于监视Cloudlet 52的体系结构VI3.1.四层架构533.2.基于资源分配器的监控553.3.建立VOR和执行驱逐出境IV.Cloudlet 59监控的技术限制4.1.监测框架594.2.纠正和具体发展604.3.监测系统的组成部分61V.个案研究645.1.与移动设备安全相关的5.2.试验665.3.我们的实验结果68VI.资产负债表70第3章Cloudlet 72I.复合虚拟设备视图的描述1.1.模块和资源的授权731.2.移动设备和传感器的表示75II.Cloudlet 75中的虚拟化范例2.1.虚拟化和Cloudlet 762.2.π-计算78III.Cloudlet 80中虚拟设备的表示3.1.VDR80的组成3.2.虚拟网络的编排和管理87IV.基于Cloudlet 92的4.1.Cloudlets 93网络的技术方面4.2.我们体系结构组件的描述944.3.ACID 95属性的投影V.案例研究975.1.移动设备975.2.系统985.3.结构一致性99VI.报告105第4章：应用于Cloudlets网络的模型检查 106I.导言106II.自动机中的形式规范108VII2.1.动机1082.2.自动化系统2.3.时间逻辑1122.4.作为验证工具的UPPAAL114III.创建3.1.第121章章3.2.122型的结构3.3.将DDR迁移到型号138IV.验证1404.1.方法1404.2.驱逐和迁移的执行情况核查4.3.本地执行检查V.第146章第一次见面第5章：原型设计和结果148I.导言1481.1.动态组件服务器1491.2.MOCP 151的定义II.移动嵌入式应用的软件体系结构1532.1.基于OSGi 1532.2.MOCP 156协议的移动实现III.Cloudlet 162的软件架构3.1.基于OSGi Karaf 1623.2.用于构建OSGi 164IV.案例4.1.配置174的说明4.2.176名义情景的发展4.3.措施说明和关键分析178V.180年后第六章结论与展望182I.贡献1821.1.软件体系结构的形式化定义1.2.基于组件的框架开发1831.3.测量工具的开发II.前景184VIII2.1.驱逐期间的时间优化1842.2.新物业研究1842.3.衡量出版物列表186会议论文186期刊文章186参考书目187IXX图表图1.1标准和标准生成之间的趋同8图1.2无线网络的发展[13] 8图1.3PhoneGap 12的图1.4Xamarin 13的图1.55G无线网络生态系统 15图1.6第24层中图2.1Cloudlet 41的图2.2Cloudlet 42的图2.3应用程序堆栈比较44图2.4Linux 46监控图2.5 Nagioscheck_ps.sh插件47图2.6Sensu 48服务器图2.7将监控集成到Android 49图2.8无线网络51图2.9NCAP 52应用程序的图2.10分布式监控的图2.11分层图2.12过滤和加权过程56图2.13设备虚拟化58图2.14虚拟化传感器58图2.15部署图61图2.16检测算法的伪码67图3.1VDR81的图3.2VDR81之间图3.3事件总线82图3.4SVDR85的图3.5全球架构93图3.6 Cloudlet的结构和网络图3.7DVDR96图3.8所用系统99图4.1 UPPAAL 116的概述图4.2UPPAAL 116的体系结构XI图4.3Cloudlets网络的全局变量声明示例 117图4.4XML 118中XII图4.5UPPAAL 118图4.6全局变量的声明123图4.7系统及其组件的声明124图4.8自动机模型Orchestror 125图4.9供应自动机模型126图4.10自动启动器127的模型图4.11运行127图4.12自动化模型配置129图4.13监控自动机模型130图4.14前端自动机131图4.15后端自动机模型132图4.16SVDR133图4.17VirtualSensor 134图4.18DevId 134图4.19DVDR135图4.20VirtualDevice 136图4.21CVDR137图4.22CompositeDevice 137图4.23过程自动化模型138图4.24管理员自动机模型139图4.25用户139图4.26财产审计概览1141图4.27所有权审计概览2 143图4.28所有权审计概览3 144图4.29在没有驱逐出境的情况下核查当地处决的概况145图4.30检查intra= cx 146的图5.1MOCP 152图5.2 OSGi层（来源：OSGi联盟，2007年）154图5.3OSGi 155的动态图5.4移动应用程序的软件架构图5.5应用程序迁移请求158图5.6 RDP和SVR之间的相互作用 159图5.7 Cloudlet和Cloud之间的交互 160图5.8在两个Cloudlet之间迁移PDR 161XIII图5.9Swagger UI 165图5.10POST/标识方法166图5.11GET/notify方法 167XIV图5.12POST/vdir/{vdrId}/migrate方法 167图5.13图5.6相互作用的组件图 169图5.14用于聚合测试用例的简单测试套件171图5.15试验结果173图5.16案例研究175图5.17评估阶段支持图5.18移动设备日志178图5.19迁移对性能的影响179图5.20分销流程迁移180XV表的列表表2.1组件编排说明62表2.2设备/传感器组件描述62表2.3Sensu 63的表2.4按平台划分的恶意代码65表2.5恶意代码的作用66表2.6我们的解决方案的结果68表2.7CAPSA 69的表2.8结果比较69表3.1圆周率演算78的表3.2圆周率演算规则79表5.1POST 171操作的引言互联对象在我们的生活和城市中的地位只会越来越大。新的技术极限已经达到，我们正在寻求超越它们。最明显的是能源消耗这些问题之所以出现在今天，是因为IT已经取得了相当大的进步，为我们提供了新的可能性：在软件架构、网络通信和虚拟化方面。因此，云计算是一个现在熟悉的术语，指按需交付资源和服务。它提供了一种通过互联网存储和访问数据的解决方案I.动机和贡献我的论文工作的主要目标是为当前问题的现实解决方案做出贡献，从而推动今天限制我们使用的移动性的限制。此外，面对我们的移动设备的计算、存储和能源资源有限的问题移动应用程序为移动行业带来了各种新服务和巨大的创新潜力。对于企业来说，移动应用程序可以促进业务流程的转型，优化旅行，同时使移动员工能够提高工作效率，简化在家工作，这是留住人才的一个来源。类似地，移动设备的用户在任何时候都将移动应用它们还为信息服务、公共服务扩展和替代服务等移动服务提供了多种可能性。然而，所有这些新兴技术都有许多局限性，特别是在移动设备方面，而不是在云方面。L’usager est amené à se déplacer d’un environnement à un autre sans se préoccuper du transfert d’unedonnée 因此，在云级别上存在通信或访问资源的问题，通过2例如，在两个不同的云上，同一个服务可能有不同的接口。为了在更好的条件下继续传输，必须有一个云或Cloudlet的缓存。通过使用Cloudlets网络，可以确保在移动过程中被移动的组件的服务连续性。为此，所有Cloudlets必须共享相同的形式规范，并且与验证工具相关联的时间逻辑允许验证时间属性。Cloudlet使用与云相同的原理，Cloudlet网络的定义Cloudlets网络允许突出显示一组互连的组件。这使我们开发了一个基于组件的框架，该框架提供了一组工具，用于在这样的网络中集成移动应用程序从公司中的Cloudlets网络开始可能会重新导入对这样的网络的监视它还允许收集和分析数据，因此需要数据安全和基础设施。为此，我们制定了一项政策，以管理员工流动期间的数据和应用程序权限此外，虚拟化Cloudlets网络中的设备和每个基础架构也很有用。这允许通过设备的虚拟表示继续网络上可用的所有设备、传感器和致动器都使用虚拟设备的这种视图，但设备可以由GPS、气压计、速度指示器和接近传感器组成在这种情况下，复合表示通过允许以协调的方式组合多个设备来为虚拟设备增加价值在急救干预的情况下为了克服这一限制，必须降低移动设备的能耗另一个动机是定义智能移动设备和Cloudlet之间的迁移协议（MOCP -面向云的迁移协议）。我们定义MOCP协议的方法是将所有API定义为Cloudlet网络中不同实体之间交换的请求/响应消息对。这种方法遵循一个迭代过程，其步骤（分析3如果发生变更，则必须审查定义过程这确保了一个随着时间的推移而发展的方法，我们的MOCP协议在http协议之上使用二进制协议，并被视为实现我们方法的基础通过验证我们的目标，我们可以强调移动应用程序的本地执行与将其驱逐到Cloudlet网络之间的相似性II.论文内容L’organisation du document est la suivante第1章介绍了移动性和三层虚拟化概念（设备-应用程序-网络）的最新技术水平。我们讨论了移动性和云计算的使用，云计算为移动性的需求或限制提供了解决方案。我们介绍了虚拟化，并概述了当今分布式移动应用程序的软件体系结构需求。第2章描述了一个基于Cloudlet监控系统的体系结构模型。在本章中，我们将介绍云计算环境中Cloudlet的虚拟化体系结构第3章提供了一个用π-微积分语言编写的正式规范，它定义了Cloudlet中虚拟设备在本章中，我们将MOCP通信协议定义为迁移过程中组件和/或服务之间交互的核心。我们提出了一个案例研究，显示了移动应用程序的驱逐和本地执行之间的结构一致性，同时说明了Cloudlet网络中本地术语和驱逐术语之间语义树的相似性第4章介绍了如何为我们基于Cloudlet的架构创建时间模型，并验证了与从移动设备迁移应用程序在本章中，我们将介绍与模型检查工具相关联的TTTL逻辑的贡献，时间逻辑中系统的这种规范是由时间自动机系统构造的。每一个都提供了一个组件随时间推移的严格描述，该组件符合与其评估环境相关的约束。此信息丰富了我们的模型，并添加了在实现中要保留的属性。我们还介绍了在最终用户移动性的情况下，在Cloudlet中跟踪虚拟化应用程序第5章介绍了它讨论了用于评估解决方案的工具