物联网应用组合与重构的模型与验证

物联网应用组合与重构的模型与验证引用此版本：Ajay Krishna Muroor Nadumane。物联网应用组合与重构的模型与验证。其他[cs.OH]。格勒诺布尔阿尔卑斯大学[2020-..]，2020年。英语NNT：2020GRALM 067。电话：03188299HAL Id：tel-03188299https://theses.hal.science/tel-031882992021年4月1日提交HAL是一个多学科的开放获取档案馆，用于存放和传播科学研究文件，无论它们是否已这些文件可能来自法国或国外的教学和研究机构，或来自公共或私人研究中心。L’archive ouverte pluridisciplinaireTHAPOSE为了获得等级格勒诺布尔阿尔卑斯大学博士专业：信息Arrêté ministériel：25 mai 2016Présentée parAjay Krishna MUROOR NADUMANEThèse dirigée parGwen SALAÜN，教授，格勒诺布尔-阿尔卑斯大学等由Inria Grenoble - Rhône-Alpes研究总监Radu MATEESCU和诺基亚贝尔实验室研究工程师Michel LE PALLEC共同赞助，法国Inria Grenoble - Rhône-Alpesdans l'École DoctoraleMathématiques，Sciences et technologies del'information，Informatique物联网应用组合与重构模型及验证基于对象网络的应用程序组成和重新配置的模式和验证这是十二月十日的出版物。2020年，陪审团组成如下：Olivier BARAISRennes第一大学讲师，考试讲师Didier DONSEZ格勒诺布尔-阿尔卑斯大学校长Pascale LE GALL女士，高级专员，特别报告员研究工程师，诺基亚贝尔实验室，共同参与者Radu MATEESCUInria Grenoble研究所所长、研究共同负责人Juan ManuelMURILLO RODRIGUEZ先生、埃斯特雷马杜拉大学研究所所长、特别报告员Gwen SALAÜNGrenoble Alpes大学讲师Farouk TOUMANIClermont Auvergne大学讲师，考官iii摘要物联网（IoT）应用程序是通过网络将日常物品互连而构建的 这些物体或设备感知周围的环境，它们的网络功能使它们能够与其他物体进行通信，以执行实用任务。在消费者领域构建物联网应用程序的一种流行方法是使用事件-条件-操作（ECA）规则组合不同的对象。这些规则通常以“如果发生了什么事，那么就做什么事”的形式出现物联网（WoT）是一组标准和原则，将Web的架构风格和功能集成到物联网中。 尽管WoT架构结合ECA规则在很大程度上简化了物联网应用程序的构建，但由于物联网系统的动态，反应和异构性，最终用户以简单而正确的方式开发高级应用程序仍然存在挑战。这项工作的主要目标是利用正式的方法，在设计时为物联网应用程序的最终用户提供一定程度的保证，即所设计的应用程序在部署时将按预期运行在这种情况下，我们提出了一个正式的开发框架的基础上的WoT。 这些对象使用来自WoT的事物描述规范的行为模型来描述。然后，应用程序的设计，不仅通过指定个别ECA规则，但也通过组合这些规则使用组合语言。该语言使用户能够构建更具表现力的自动化场景。 对象及其组成的描述被编码在一个正式的规范中，从该规范中可以识别应用程序的完整行为。为了保证正确的应用程序的设计，这项工作提出了一套通用的和应用程序特定的属性，可以在部署前的完整行为进行验证此外，所部署的应用可以在它们的应用生命周期期间被重新配置。 这项工作支持重新配置，通过指定重新配置的属性，允许一个定性比较的行为，新的配置与原始配置。所有建议的实现都是通过扩展MozillaWebThings平台来实现的已经建立了一套新的用户界面，以支持规则的组合和重新配置。模型转换组件将WoT模型转换为正式模型，并与正式验证工具箱集成，以实现自动化。最后，通过扩展WebThings API构建部署引擎。 它指导应用程序的部署和重新配置，尊重它们的组合语义。IV简历物联网的应用是将网络上的对象相互连接起来的这些物体相互连接，观察者观察周围的物体，并在物体上移动Pour le grand pubic- lic，这些规则通常以“如果选择了什么产品，就选择什么产品”的形式出现。 Le web des objets（Web ofThings ou WoT）est un ensemble de normes et de principes qui intègrent lescapacités du web et les styles architecturaux à l'IoT. 由于物联网系统的动态性、反应性和复杂性，在构建物联网应用的大规模过程中，物联网体系结构与ECA规则相关联，因此，物联网应用的发展和正确性需要利用物联网技术来实现。L'objectifgénéraldecetravailestdetirerpartidesmethodesformellespourfourniruncertainniveaudeguarantieauxutilisa-finauxdesapplicationsIoT. 在受孕的时候，我们可以确保应用程序可以像之前一样运行在这种情况下，我们建议建立一个以世界贸易组织为基础的发展框架。Les objets sont décrits à 此外，这些应用程序并不适用于特定的ECA规则，但也适用于与组成语言有关的规则。 Ce langagepermet aux utilisaeconomy de quartiire des scénarios d'automatisation plus expressifs.Ladescription des objets et acquisition sont traduites dans une specécificationformelle à partir de laquelle le comportement complet de l'application est identifié.为了确保在部署之前对适用情况有一个正确的概念，这一建议对适用情况的完整性进行了一般和具体的确认 此外，应用程序可以在生命周期的各个阶段重新配置。Letravailexposurelarecombinationenspécifiantdespropriétésdereconfiguration qui permettent de comparerqualitativement le comportementde la nouvelle configuration avec la configuration所有这些提议都是在MozillaWebThings平台上实现的。Un nouvel ensemble Un composant permettant deTransformerautomatiquementlesmodèlesWoTenmodèlesformels ，pleinement intégré au sein d'une boite à outils de vérification formelle a été décampé.Enfin ， un moteur de déploiement est professit en étendant les API deWebThings. Il dirige le déploiement des applications et des reconfigurationsen respectant la sémantique de marticles composition.v确认我要向所有在过去三年中为我们的学习做出首先，我必须感谢我的论文指导教授。 Gwen Salaün，没有他的指导和监督，这项工作就不会实现。教授Salaün他总是愿意倾听，理解问题，并引导我朝着正确的我衷心感谢教授。感谢Radu Mateescu的温和和及时的指导，帮助我解决了工作中一些最具挑战性的问题我从他丰富的经验中受益匪浅，我将把这些经验带到我的工作和生活中。感谢博士。Michel Le Pallec为我的作品带来了工业视角他是一个完美的主人，每当我访问贝尔实验室，巴黎。我也很感激能与才华横溢的人一起工作，他们是Inria Convecs团队的一员教授Hubert Garavel，总是在那里帮助每当我需要他的建议。感谢教授。弗雷德里克·朗在技术问题上的帮助，以及午餐时丰富的讨论我要感谢教授。WendelinSerwe对他的帮助尤其与LNT和建模有关我感谢女士。感谢Myriam Etienne帮助我管理博士学位的行政方面。 我特别感谢小组的所有非常任成员（博士生、研究人员、实习生）。我感谢他们的帮助，不仅在技术问题上，而且在日常生活中。他们让我的逗留愉快而有趣。我认为自己很幸运能成为这个团队的一员，每个人都愿意抽出时间来帮助我，每当我突然提出问题。感谢巴黎贝尔实验室物联网控制组的成员的合作。我必须感谢我的论文的审稿人和审查员审查我的工作，并参加我的论文答辩期间没有像其他。非常感谢我的朋友和家人，他们一直是我的支柱，帮助我追求我的目标。vii内容1介绍11.1背景与动机31.2方法81.3捐款101.4工作时间表121.5结构132相关工作152.1物联网应用模型152.2非洲经委会语文的表达能力2.3物联网应用验证202.4物联网应用的重新配置2.5智能家居中的终端用户工具252.6结束语.303背景313.1行为模型313.2LNT语言333.3模型检查393.4重写逻辑424物联网的正式模型454.1物联网规范464.2物联网对象模型504.3ECA规则和写作语言534.4LNT63中的质量标准4.5Maude71中的质量标准4.6结论性意见. 745物联网的属性规范755.1用MCL75进行设计时验证5.1.1一般属性765.1.2应用程序属性81VIII5.2重新配置属性845.2.1无缝重新配置845.2.2保守重新配置875.2.3有影响力的重新配置895.2.4重新配置示例915.3结论意见.926莫扎特工具936.1项目WebThings936.1.1WebThings网关936.2设计时验证和重新配置的WebThings扩展6.2.1设计时验证组件976.2.2重新配置组件996.3技术与应用1016.3.1CADP1016.3.2Maude系统1036.3.3执行1036.4评价1046.4.1作品的表现力1046.4.2用户反馈1066.4.3验证性能1086.4.4部署设置1106.5讨论1127结论1137.1物联网模型1137.2物联网验证1147.3工具实施1157.4未来的工作116参考书目1191„介绍1随着机器变得越来越高效和完美，人们也会清楚地认识到，不完美是人类的伟大之处。-恩斯特·菲舍尔奥地利记者、作家和政治家多年来，通信技术和电子技术发展迅速，这使世界比以往任何时候都更加紧密其中，互联网帮助发现了传统通信之外的新领域互联网与现代电子设备一起，打破了地理和文化障碍，创造了规模和范围难以想象的社区，使新型企业成为可能。物联网（IoT）就是网络通信和现代电子产品的出现所释放的一种可能性。 从广义上讲，物联网涵盖了物理世界中连接到互联网的一切，我们将这些“一切”称为对象或设备。一个物体可以像我们每天使用的灯泡一样简单，也可以是一个连接到互联网的复杂工业控制器 这些对象可以相互通信并执行实用任务。国际电信联盟（ITU）将物联网定义为：“信息社会的全球基础设施，通过基于现有和不断发展的可互操作信息和通信技术互连（物理和虚拟）事物来实现高级服务”[ITU16]。 在这项工作中，我们将物联网应用称为一组旨在服务于特定目的的相互关联的事物。技术专家KevinAshton于1999年在Procter &Gamble（&PG）的一次演讲中首次介绍了物联网一词，以描述通过无处不在的传感器与物理世界交互的互联网连接系统[LLC13]。 这个定义源于他对互联网连接的射频识别（RFID）的研究。然而，连接物体捕捉周围环境的想法并不新鲜，它甚至可以追溯到互联网的出现18世纪末发展起来的普通老式电话系统（POTS）可以被认为是第一个连接对象系统。它将声音捕获为模拟信号，并使用导线传输。后来随着无线电的发明，2第1章绪论通信系统进入市场，它们实现了新一代的连接系统。1959年的一项重大突破导致了现代电子学的诞生：贝尔实验室的研究人员发明了金属氧化物半导体场效应晶体管（MOSFET），这是一种广泛用于数字和模拟集成电路的半导体器件[Mus20]。如果我们想看看一个更相关的物联网应用的早期实例，那就是卡内基梅隆大学（CMU）的连接苏打水自动售货机。20世纪80年代的研究人员实现了一个应用程序，可以在舒适的办公室里检查苏打水自动售货机是空的还是最近重新进货的（如果饮料最近被放在机器里，饮料会是热的）。它是通过连接到互联网的前身阿帕网的电路板实现的。值得注意的是，连接对象的概念并不局限于消费者领域。1995年，西门子推出了M1 GSM模块，开创了蜂窝机器对机器（M2M）通信的先河[Bha18]。它进一步开创了一个工业制造的新时代，涉及嵌入式控制系统的远程监测，控制和遥测。随着时间的推移，机器不仅能够理解周围的世界，而且能够与其他机器协调并做出有意义的决策。物联网生态系统正在迅速发展，在医疗保健、交通运输、农业、制造业、智能家居和智能城市等许多应用领域发挥核心作用。 预计到2030年将部署近1250亿台连接的物联网设备[MTK18]。 这种爆炸式增长可以通过理解物联网如何为我们的日常生活带来价值来解释。简单的传感器，如蓝牙收发器或温度传感器，在孤立的情况下似乎只有特定的用途收发器可以与附近的物体交换数据，温度传感器可以测量体温。但是，当我们将这些看似简单的物体连接到互联网上，并使它们能够相互通信时，可能性超出了显而易见的范围。例如，蓝牙与GPS相结合有助于在最近的冠状病毒爆发期间进行接触追踪[Gre20]。 Smart 1温度计通过汇总消费者的温度数据并在患者出现症状之前准确预测病毒传播，在跟踪和减少冠状病毒传播方面发挥了关键作用[YS 20]。在日常物品前加上smart是一种向读者传达该物品具有网络和编程能力的方式31.1背景与动机1.1 背景与动机与每个走向成熟的系统在成功采用物联网生态系统之前，需要克服一些成长的我们的目标是通过使用正式的方法来解决物联网生态系统中的挑战在详细介绍这些挑战之前，让我们快速浏览一下与形式化方法相关的重要的是要介绍这些技术，以了解它们如何适应物联网领域的挑战。形式规格说明与验证技术形式方法是基于数学和形式逻辑的技术 使用这些技术，复杂的软件，硬件和网络物理系统可以建模为数学实体。用精确的形式语言描述系统的非数学表示的过程被称为形式规范。形式化语言严格的语法和语义使得能够对规格说明进行形式化推导。 由于该规范精确而明确地捕获了系统的行为，因此可以用于在数学上验证实现。模型检查[BPS01]是一种形式验证技术，其中系统是根据有限状态机进行建模的该模型被馈送到模型检查器，该模型检查器确定给定模型是否满足表示为逻辑公式的属性等价性检查[CS01]是另一种验证技术，它确定两个模型在功能上或语义上是否等价。项重写[BN 99]是一种处理称为重写规则的方程的计算技术这是一个将重写规则应用于术语的归约过程项可以是变量、常数或对变量和常数进行运算的结果重写逻辑理论对并发系统的静态和动态方面进行它包括一个等式理论和一组分别代表静态和动态方面的条件重写规则[Mes12]方程理论结合重写规则可以指定并发系统如何相对于其状态演化。上面提到的验证技术可以应用于物联网应用程序，以验证它们是否按预期运行。物联网应用程序的验证非常重要，因为应用程序具有某些固有的特性，4第1章绪论以保证他们的正确行为。在随后的文本中，我们将描述这些特征以及如何将形式方法置于此上下文中。物联网应用特征与形式化方法在并发系统的各种特征中，使物联网应用程序的开发成为挑战的特征可以大致分为三类。异构：随着物联网生态系统的发展，它利用了各种底层技术、标准和协议。物联网堆栈的不同级别有各种标准[Fuq+15]。图1.1：物联网标准和协议图1.1提供了物联网中跨网络堆栈不同层的现有标准的快照。图1.1中提到的标准列表并不详尽，但它试图给出系统不同层之间存在的多样性的概念。造成这种多样性的原因有很多：标准随着时间的推移而演变，专有标准，大量小制造商在实施标准方面受到限制等。正如彼特拉克所说，多样性是治疗方法;这些标准提供了51.1背景与动机开发物联网系统的充足选择，但它们带来了一系列互操作性问题。 为了按照ITU-T的设想为信息社会建立一个真正的全球基础设施，最好有一个单一的标准。因此，努力集中在构建多层框架上，有时重用这些协议，以克服碎片化并允许具有不同底层标准的系统互操作。有各种组织和联盟在为这一倡议工作。互联网工程任务组（IETF）提出了CoRE（受限的RESTful环境），OneM2M [Par 20]是物联网的Machine2Machine（M2M）标准，Weave是Google支持的应用级协议。最后但并非最不重要的是，万维网联盟（W3C）已经发布了物联网[W3C20c]，这是一个基于Web [GT 09]原则的规范。虽然这些框架在很大程度上解决了互操作性问题，但底层的异构性仍然存在，因此难以理解系统的完整行为行为的正式规范可以在这方面有所帮助，因为人们可以以统一和明确的方式定义不同异构系统的行为。该规范可以提供系统的平台不可知定义复杂性和动态性：物联网系统的异构性使得部署和管理它们变得复杂 除此之外，物联网系统增加复杂性的另一个显著特征是其分布式架构。物联网系统是分布式的，跨越网络和地理边界。物联网系统的范围从小型家庭应用到大型部署，如智能城市，制造业等，并且分布式体系结构易于扩展。然而，由于分布式系统表现出高度的并发性，评估这些系统的一致性和正确性可能是一个挑战，特别是当它们的行为没有明确定义时。物联网对象是反应式系统，不断与其环境交互，从而改变其状态。对象的这种行为使得物联网应用程序高度动态，因此容易受到意外行为的影响。识别意外行为并同时确保所需行为到位可能是一项挑战，在动态系统中更是如此。通过将系统中的意外和预期行为指定为属性，可以使用模型检查技术检查这些属性是否在系统的形式规范中保持属性规范和验证可以帮助检测动态和分布式系统中的错误，这实际上允许人们获得关于系统行为的正确性保证6第1章绪论应用程序的维护和发展：物联网应用程序，特别是在消费领域，并不是一劳永逸的它们正在不断修改或升级，就像当今任何其他消费电子设备一样 与传统的稳定应用程序（如生产线、企业软件等）相比，物联网应用以更快的速度发展例如，应用程序中的更改（重新配置）可能是由于设备停止服务时的更换，也可能是设备软件（功能）的升级。在某些情况下，可以完全替换应用程序以提供全新的服务。应用程序的演化涉及用新行为替换现有行为在典型的情况下，应用程序的行为不会被完全替换，而是用户希望部分保留或扩展现有的行为。重新配置方面的挑战之一是从质量上衡量变动对现有配置的影响。此外，重新配置发生在应用程序的执行生命周期期间，因此，对正在运行的应用程序的影响应保持最小，以便尽可能保留功能和服务质量项重写可以有效地跟踪系统中状态的演变，因为重写主要是用等价表达式替换表示对象状态的表达式重写分析可以识别系统中的状态是否等价，也可以确定两个不同的系统是否导致相同的状态（收敛）。这些技术可以在两个领域的物联网应用中使用：第一，跟踪系统相对于原始系统的演化;第二，识别从原始系统演化到保持状态一致性的期望系统的方式智能家居前面提到的问题需要一系列解决方案，其中一些超出了本工作的范围此外，即使这些问题出现在各个物联网领域，如果它们是特定领域的解决方案将更有意义。因此，我们将工作重点放在消费者物联网上，特别是将我们的方法应用于智能家居。 智能家居自动化是物联网发展最快的领域之一。 用户可以使用市场上可用的智能对象自动化家中的任务，与工业自动化任务不同，这不仅限于熟练或专家用户。可用性是任何系统获得广泛采用的关键因素，特别是在最终用户是消费者的情况下。 在对2017年消费电子展（CES）250名参与者的调查中，几乎所有（>99%）参与者71.1背景与动机R1：如果bpm（异常，异常），则集线器（非异常，bpm）和计数器（bpm，异常）R2：如果计数器（bpm> 3）然后 轮毂（c a l l，112）R3：如果摄像头（开启，触发）则报警（开启，触发）R4：如果温度计（温度>25）则窗口（打开，触发）R5：如果运动（存在，fal s e），则门（打开，fal s e）和窗（打开，fal s e）同意可用性是物联网产品供应商的一个重要领域[R ow17]。 智能家居自动化可访问的原因之一是易于使用的基于UI的工具，如IFTTT [IFT 20]，OpenHab [Com20]等。这些工具允许使用规则设计自动化通常，规则的形式是“如果发生了什么事，那么就做什么事”。在这里，something-happens是一个触发器或一个需要发生的事件，因此do-something是正在执行的动作由于这些规则遵循特定的模式，它们被称为事件-条件-动作（ECA）规则，使用这些规则进行自动化编程的方式被称为触发器动作编程（TAP）。现在，让我们考虑一下环境辅助生活（AAL）环境中的一些场景，其中老年人居住，并且通过使用连接设备设置自动化，使她/他的生活变得更容易 作为一个技术新手，他/她以ECA规则的形式配置简单的自动化来执行例行任务。假设她/他有一组对象，并且她/他配置了以下规则：R1规则使用智能手表（例如，Apple Watch），其主动监测健康参数，例如血压、心率、氧气水平等。因此，如果检测到异常，则通知被发送到家中的集中式集线器设备（例如， Google Nest Home），它具有一个计数器，每当收到警报时都会更新。假设如果检测到异常超过三次（用户没有重置计数器），则可能用户身体不适，并且如规则R2中定义的那样向紧急服务警告事件规则R3被配置为检测家中的入侵它使用智能监控摄像头（例如，Nest IQ），它可以检测陌生人，如果检测到入侵者，就会发出警报在内部，它使用云上的分析服务来识别熟悉的面孔。此外，规则R4使用智能温度计，当房子变暖和时，窗户就会打开。最后，R5确保当没有人在房子里时门窗保持关闭。这个家庭设置说明了智能家居自动化的各个方面可以观察到，IoT对象不仅仅是简单的传感器和致动器，它们可以执行更复杂的操作（例如，分析），从而具有先进的8第1章绪论行为（例如，集线器和监视摄像机）。在设计规则时考虑对象的行为是很重要的例如，在R3的情况下，入侵检测功能依赖于云服务，并且自动化规则中不会捕获此外，在R1中，如果用户用不具有心律失常检测特征的不同品牌的另一手表替换他的手表，则该异常将不会被规则捕获这可能会对用户的健康造成严重后果 这个问题的出现是因为没有机制来检查自动化是否在功能上是等效的。在大多数自动化设置中，规则是并行运行的（无论事件何时发生）。现在考虑规则R4和R5，当没有人在房子里时，不能保证窗户总是关闭的（温度可以>25）。这可能是一个安全问题，因为当用户离开家时，窗户可能会打开在设计时没有帮助用户检测不安全自动化的检查考虑到这些方面，我们的目标是使用户能够以简单的方式设计应用程序，同时为他们提供确保应用程序在部署时按预期运行的方法。这种正确性保证不仅要考虑规则，还要考虑各个对象的行为1.2 方法如前所述，我们的工作利用形式化方法来解决1.1节中提出的挑战。形式化建模允许以抽象的方式指定物联网应用程序的行为，独立于底层的异构组件。可以使用形式验证技术分析此规范，以确保系统按预期运行，即， 它满足某些感兴趣的性质。应用程序的规范包括对象、规则以及它们与物理环境的交互。我们在多层框架的基础上指定应用程序，因为这些框架提供了桥接不同协议的水平集成因此，它允许我们专注于指定应用程序的行为，而不用担心底层协议。 这也使得我们的方法适用于所有的现实世界的对象和应用程序的框架支持。物联网（WoT）是一个框架，它通过抽象底层细节来帮助缓解互操作性问题，同时为用户开发物联网应用程序提供必要的接口。它使用Web的架构风格和原则，其中每个对象都由其URI标识对象91.2方法使用它，由称为事物描述（TD）[W3C20b]的机器可读描述指定。作为第一步，我们根据TD指定对象的行为该行为描述的标签转换系统（LTS），状态转换图，其中系统从一个状态移动到另一个状态取决于由系统本身或外部环境执行的动作这些对象可用于定义自动化规则。规则的形式是“如果发生了什么事，那么就做什么事”。此外，我们使用一种语言来编写这些规则，与独立运行规则相比，它允许定义更高级的应用程序最后，通过指定与对象交互的环境来捕获应用程序的执行，从而影响规则及其组成。一旦应用程序的模型可用，我们就确定了一组可以在模型上检查的属性。这些属性被指定为时态逻辑公式。如果模型不能满足这些属性中的任何一个，则表明应用程序的行为可能与预期的不同，因此需要修改应用程序的设计一旦设计令人满意，就可以继续部署应用程序。关于实现，应用程序在LNT[Cha+18;GLS 17]中正式指定一种具有进程代数语义和编程语言语法的语言 LNT模型可以在CADP [Gar+13]中编译和分析，这是一个正式的验证工具箱。 使用模型检查语言（MCL）[MT08]指定正确性属性，MCL是一种数据处理时态逻辑，适用于表达值传递并发系统的属性。CADP的编译器将LNT规范翻译成LTS，在LTS上检查MCL公式并动态地产生相应的诊断。此外，为了支持可能的演变的应用程序随着时间的推移，我们确定重新配置的属性，允许设计师比较当前的应用程序与一个新的。这些属性检查是否可以部署维护对象状态一致性的应用程序，当前应用程序的行为是否保留在新应用程序中，以及新应用程序的影响。 这种检查是通过指定Maude重写逻辑[Cla+07]中的组成和属性来实现的，因为它允许我们通过重写方程来跟踪应用程序中对象状态的演变。物联网对象的用户需要了解它们的功能，他们应该能够轻松地利用这些功能来构建有用的应用程序。在消费者领域，10第1章绪论大体上存在两种用户可以构建应用程序的方式首先，具有编程知识的用户可以利用Android Things等设备和平台API来构建应用程序。缺乏编程经验或不喜欢使用它的用户可以使用基于UI的工具构建物联网应用程序，如IFTTT [IFFT 20]和Node-RED[F ou 20]。 这些工具抽象了编程API，并为用户提供了简单的拖放界面来构建应用程序。 从表面上看，这种方法似乎工作得很好，因为公众对这些工具的采用率很高，但如果我们深入研究，我们会发现两个问题：i）用户在将他们心目中的应用程序转换为UI工具时面临困难[Bri+17]。 这部分是由于这些工具没有足够的表达能力来捕捉用户需求[Ur+14;HC 15]; ii）即使用户可以设计预期的应用程序，他们也很难理解所设计的应用程序的完整行为[Bri+17]，如果行为没有完全理解，就不能保证系统按预期工作。考虑到这些可用性问题，我们通过扩展Mozilla WebThings平台[Mozilla 20b]构建了一个名为MOZART（MozillaA advancedR uleT riggers）的工具[Kri+20]，该平台提供了基于抽象数据模型和Web of Things中指定的架构的具体实现MOZART提供了一个用户友好的界面来设计组合，验证它们，并部署它们.通过使用基于正则表达式的组合语言，提高了设计的表现力。 验证为应用程序行为提供设计时保证。一旦应用程序被部署，用户可以使用MOZART工具执行重新配置分析，以备他们需要更新设计。通过允许用户重新设计应用程序的界面支持重新配置该接口连接到验证组件以执行重新配置分析并将分析结果提供给最终用户。最后，可以使用该工具提供的支持以一致的状态部署重新配置的应用程序。值得一提的是，该工具通过在简单的用户界面后面自动化验证过程，向最终用户隐藏了形式验证的复杂性1.3 贡献我们的工作提供了一个端到端的解决方案，即， 从设计到部署的物联网应用。具体地说，通过集成形式化方法，它可以确保111.3贡献所设计的系统如预期的那样工作在这方面，我们的主要贡献是：• 对象及其组成的模型提出了物联网对象及其组成的行为模型，考虑到物联网系统的异构性，这有助于以统一和明确的方式理解应用程序的行为对象的组合是通过使用组合语言组合事件-条件-动作（ECA）规则来指定的。在这项工作中定义的语法和操作语义的组合。• 设计和重新配置分析支持验证的组成是通过编码的模型及其行为的过程代数语言（LNT）和重写逻辑（Maude）。在WoT应用程序的设计过程中的正确性属性被识别和指定的时序逻辑。检查这些属性有助于在部署之前检测设计的系统中可能存在的问题通过指定将现有应用程序与新设计的应用程序进行定性比较的属性来提供对物联网应用程序的重新配置的支持• 工具支持通过为最终用户开发一个易于使用的UI工具，实现了形式化方法和验证技术与物联网平台这是通过扩展Mozilla WebThings平台来实现的通过部署引擎提供对所设计应用的部署的支持，该部署引擎执行新设计的IoT对象组合，并且还无缝地部署重新配置的应用