多层双图建模：上下文感知系统的挑战

沙特国王大学学报上下文感知系统的多层双图建模方法Ahmed Taki Eddine DIB，Ramdah MaamriLire实验室，君士坦丁二世大学-Abdelhamid Mehri，君士坦丁，阿尔及利亚阿提奇莱因福奥文章历史记录：2021年5月9日收到2021年8月5日修订2021年8月8日接受2021年8月15日网上发售保留字：形式建模多智能体系统A B S T R A C T存在提出用于构建上下文感知系统（CAS）的若干方法然而，由于环境的不断变化，大量的相互关联的组件，复杂性和多样性的应用领域，使上下文感知系统的建模是一个特别具有挑战性的任务。为了解决建模日益复杂的问题：i）考虑环境（操作环境）的重要性至关重要; ii）依靠软件工程概念，如抽象和模块化，以降低复杂性水平。此外，上下文感知系统可能需要智能和自主性。这些自然引导我们应用基于智能体的工程。这项工作介绍了一个正式的分层设计方法，结合智能控制的多代理系统和bigraph的严格模型上下文感知系统。双图反应系统是特别引人注目的，因为它们的能力，同时指定，物理和逻辑分布的系统组件和它们的互连使用两个不同的结构，即：位置图和链接图。虽然行为和动态演化是使用定义的反应规则来表示的，但作为最后一步，用Maude语言对bigraph规范进行编码，以允许其执行和验证其有效性。版权所有©2021作者。由爱思唯尔公司出版代表沙特国王大学这是一个开放的访问CC BY-NC-ND许可证下的文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。1. 介绍在当今世界，上下文感知系统（CAS）无处不在，随时随地提供各种计算能力和服务。应用程序应该了解其环境，并自动适应不断变化的情况，以便为用户提供足够的服务。这就是所谓的上下文意识.任何可以用来描述实体状况的细节都被称为上下文。实体可以是被认为对用户与应用的交互重要的个人、位置或事物如果一个系统能够使其行为*通讯作者。电 子 邮 件 地 址 ： ahmed. univ-constantine2.dz （ A.T.E.DIB ） ， ramerous.maamri@univ-constantine2.dz（R. Maamri）。沙特国王大学负责同行审查制作和主办：Elsevier使用上下文，它是上下文感知的。这些系统最重要的目的是为特定的个人、地点、时间和事件提供足够的服务（Dey，2001）。CAS在无处不在和无处不在的环境中的建模和实现提出了超越传统设计和开发方法的新挑战上下文感知系统可能需要使用预定或自组织通信协议来执行随机任务的不同资源集合。这些系统必须具有灵活和自适应的体系结构，以处理环境和用户不断出现的需求有许多正式和半正式的建模方法，在文献中然而，这些方法并没有在设计阶段将环境作为建模维度来处理。这导致预先建立的通常是刚性的解决方案，其中交互、用户和更改是固定的。此外，他们缺乏技术和工具来验证最终的设计。在这项工作中，我们认为一个上下文感知系统作为一个多层次的网络物理系统。上下文感知系统的建模考虑了一般系统理论的概念，即层次结构和涌现。此外，上下文感知系统需要智能和自主性。这些自然引导我们应用基于代理的工程。因此，上下文感知系统需要这些组件：https://doi.org/10.1016/j.jksuci.2021.08.0081319-1578/©2021作者。由爱思唯尔公司出版代表沙特国王大学这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。可在ScienceDirect上获得目录列表沙特国王大学学报杂志首页：www.sciencedirect.comAhmed Taki Eddine DIB和R. 马阿姆里沙特国王大学学报6126- 一个坚实的概念层（上下文和上下文感知系统）。- 主动性和适应性，以促进给定上下文的共享、管理和推理。- 形式化的基础保证了系统的健壮性和正确性形式化建模在一般计算机系统的开发中变得至关重要。在此背景下，形式化方法在很大程度上依赖于数学定义，可用于为上下文感知系统提供精确模型，并确保根据通用标准（通用标准，2021）的高评估保证级别此外，它有助于在设计阶段早期集成验证，便于早期发现设计缺陷。此外，形式化方法被赋予了强大的工具，用于自动化的各个阶段的验证。在这项工作中，我们提出了一种建模方法，结合智能控制的多智能体系统和bigraph双图是特别吸引人的，因为它们能够指定，在同一时间，系统组件和它们的互连使用两个不同的结构，即位置和链接图的物理和逻辑分布而行为和动态演化是使用一组定义的反应规则来表示的。事实上，BRS已经在几个领域应用中显示出它们的充分性，例如上下文感知系统（Sahnoun等人， 2017），网络（Boucebsi和Belala，2020），雾计算（Benzadri等人，此外，我们依靠Maude系统来实现自动执行和验证所产生的规范（Benzadri等人，2021年）。这种方法收集了上面介绍的功能，并展示了如何该模型的主要特点是通过实施的应用程序进行验证。第2描述了我们对这个问题的一般方法，而第3节描述了系统第4列出了概念验证应用程序和实验，这些应用程序和实验是评估和验证建模方法的第五部分对类似的田野调查进行了总结和比较最后一节对未来的研究提出了一些建议。2. 我们的方法原则情境感知系统（CAS）被认为是一个多层次的信息物理系统，它专注于用户，系统和外部环境之间的显式交互和通信，采用了许多模态。CAS由系统的所有组件以及周围环境（传感器、致动器、智能电器、智能手机和平板电脑、工作站和服务器）组成，其中设备通过使用各种协议并且主要是无线传输的无处不在的数据从一个层到另一个层以统一的格式采用标准的原型传输。应用层提供上下文感知系统、智能决策过程以及通过支持不同实体之间通信的标准接口的交互。因此，CAS的建模必须考虑一些额外的方面相比，经典的软件系统，使这样的系统很难建模和管理通过时间。我们的目标是使我们创建的模型更有用i）通过提出一种建模方法，通过使我们提供的解决方案更接近其各自的领域来简化模型构建过程ii）通过依赖于先进的软件工程概念，如抽象和模块化，以降低复杂性水平应用这些原则拓宽了系统工程的范围，经典的解决方案，通过识别共同的性质的层次水平。除此之外，还有上面提到的SE概念。为了解决建模日益复杂的问题重要的是要考虑到作为建模维度的背景此外，它应该明确和简洁地描述操作环境。环境层表示使用所设计的系统这对实现预期目标至关重要先进的系统性能是通过了解组件可靠性和组件交互如何受到其运行的条件、设置和环境的影响来衡量的在我们的方法中，环境层是一个主要的内生建模维度。在此基础上，接口层在环境层与软件和硬件层之间起着重要的作用它通过确保信息传输和允许双向因果关系来处理操作环境和系统用户。信息（数据）以统一格式并采用标准协议提供给其他层现实世界系统中的工程解决方案涉及与决策者合作。软件层起着重要的作用。首先，它通过特定于域的进程为名义用户请求提供反应行为。其次，它提供了一个主动的行动，作为对操作环境变化的响应。这独立于任何人类活动，促进了自主性并防止了组件的可靠性和交互。它最终通过物理效应器（硬件层）作用于上述层是建立在代理技术作为一个积木。其中，智能体提供自主性、反应性和主动性，通过允许预期来引入智能行为自主和认知代理的交互作为多代理系统的一部分进行协作这与CAS的属性非常吻合，比如上下文感知、分发、协作和适应。这项研究旨在建立一个传记，基于多智能体一种模型，用于基于系统的用户、环境、应用程序和硬件等因素的集合来描述上下文感知系统这些参数相互交织，可以相互影响因此，联合国系统必须适应其业务环境，以实现其最终目标。该系统将满足预定义的和期望的要求，如上下文感知，适应性，可用性，可靠性和鲁棒性。上下文感知系统的建模考虑了一般系统理论的概念，即层次和涌现。它假设上下文感知系统是由上述因素（系统的用户、环境、软件和硬件）组成的多层网络物理系统这些因素代表了我们CAS的层次。其中每一层包含若干子层，这些子层构成实际层的局部上下文。此外，我们还引入了第二个建模维度，该维度跨主层的子层（系统的用户、环境、应用程序和硬件）进行操作。这种层和子层的交错形成了微观/中观层次的建模（见图1）。 1.），代表Fig. 1. 微观/中观层面的建模。Ahmed Taki Eddine DIB和R. 马阿姆里沙特国王大学学报6127！！[啊！的¼¼快！[啊！的局部上下文，而全局上下文表示系统的全局上下文。3. 上下文感知系统的形式化规范CAS系统的规范是通过定义第2节中描述的层的结构和行为来实现的（见图2）。我们构建的上下文感知系统的规范提供了以分层方式管理全局上下文的特定信息的机制。所提出的方法的结构如下; 2构成我们的上下文感知系统的每一层都被建模为一个二图。Milner（Milner，2008）引入了双图反应系统，以提供一种图形化、直观的形式化模型，能够同时表示分布式和高度动态系统（如上下文感知系统）的连接性和局部性概念。而且他们为并发性和移动性提供了现有进程演算的统一（如p演算，Petri网，k演算等）（Milner，2008）。定义1.一个bigraph的正式定义是：G¼.V;E;ctr l;GP;GL：I！J其中：V和E分别表示节点和边的有限集，c = V？K控制：V K控制：V K是一个控制映射，它将控制分配给每个节点。签名K是一组控制。GP第一，第二，第三，第四 ：mn是G的位置图，它表示森林，其中prnt：m V V n是与每个节点及其分层父节点相关联的非循环父映射。m和n都是分别表示站点和区域的有限序数，G L¼V;E;c;link：X！Y是G的连接图，它表示超图，其中连接：XPEY是链接映射，X和Y分别表示内部名和外部名，P是G的端口集合。接口Im;X>和Jn;Y>分别表示偶图G的内面和外面。<<每一层的结构演化是用偶图的合成来完成的。CAS的总体结构是不同层次的偶图并置的结果而动态演化和系统行为的模型使用双图反应规则。3.1. 上下文感知系统结构3.1.1. Biographical specification：环境层我们从环境层开始我们的规范。这一层是重要的信息来源。它也是共享和替代各种异构系统，如服务，传感器等编码的环境层，我们使用米勒的标准bigraph定义。每个节点代表我们环境的一个特定实体（操作上下文），而边和超边则代表这些实体之间的连接。这种选择是由这个传统定义的通用性（抽象）和表达性驱动的，以编码上下文感知系统、应用程序域和功能的许多方面。我们的上下文模型是基于这样的目标，即对一组特定的上层实体进行建模，这些实体可以帮助在不同的应用领域中添加特定的概念。在这项工作中，我们认为上下文表示为高级概念的插图（Dey，2001）。 为此，我们提供了一个映射方法的基础上，特定领域的本体。这种选择的动机是这样一个事实，即本体是通过一组概念和这些概念之间的关系对特定领域内的信息的系统表示（Lüddecke et al.，2014年）。此外，对于CAS操作上下文，如移动服务的上下文驱动适配（CoDAMoS）（Preuveneers等人，2004）、Smart Space（Qin等人，2007）和CACOnt（Xu等人，2013年）。此外，我们为CAS设计者提供了灵活性，以通过i）依赖于现有本体或ii）通过扩展来定义当前环境的概念（参见表1）来定义表示环境层（操作上下文）的偶图。定义2.形式上，环境层由偶图GENV定义。表1上下文感知系统、双图和本体概念之间的映射上下文感知系统环境层Bigraph本体组件/零件节点概念互连边缘，超边缘链接图二. 上下文感知系统建模。Ahmed Taki Eddine DIB和R. 马阿姆里沙特国王大学学报6128我的天Pn.阿托洛河R2.... ..PLG¼.V;E;ctr l;G;G：N！ZL我的天PL¼ G oGoGGENV¼.VEN V;EEN V;ctr l;GEN V;GEN V：I！N定义4. 形式上，双图GH定义如下，P L其中：- ENV表示实体的集合。这些实体构成了特定域的操作上下文;它们可以是虚拟的（虚拟机、服务等），或物理部件，例如（家庭建筑元件、道路、轨道、传感器等）;- EENV表示由实体集合VENV定义的概念之间的关系集合;- GENV和GENV表示操作上下文的概念之间的拓扑和互连。Im;X和J n;Y是操作上下文和上下文感知系统其他层的接口。3.1.2. 接口层：Interface layer在定义了环境层之后，我们现在转向第二步，使我们的上下文感知系统。准确地说，我们描述了界面层。它构成了用户、系统（应用程序和硬件）和操作环境之间的信息传输接口在新一代控制论系统浪潮中，用户和操作环境是系统的组成部分。有必要放松对系统及其操作上下文之间边界的传统假设，使其仅仅是上下文感知系统的延伸。更好地考虑环境的重要性是这一战略转变的关键推动因素。接口层提供通信机制和策略，以从多个源收集信息，使其可用于操作员和决策者。接口层的实现是通过一个链接（k）完成的，它表示一个没有节点的无位置的偶图 连接是使用两种基本的双图形式生成的：基本替换y=X和基本闭包x。定义3.由linking（k）表示的接口层是从内部名称到外部名称的映射，以及往返于环境层双图、用户层、硬件层和应用层的边。这是由不同层的双图的合成、乘积和恒等式生成的接口层是一个链接k，其中从X到Y的替换r是一个张量初等代换的乘积HHHHHPL其中：-VH是CAS的设备集合- EH是连接不同设备的边的集合。- G H的地方图表示的拓扑结构（物理分布）和位置，而G H表示我们的上下文感知系统的设备的互连模式。- 接口Nm;X和Zn;Y表示平均值通过将一个双图放在另一个双图的顶部（组合）或并排（并置）与其他层进行通信。3.1.4. 传记规范：软件层软件层起着重要的作用。首先，它通过特定于域的进程为名义用户请求提供反应行为其次，它提供了一个主动的行动，作为对操作环境变化的它最终通过物理效应器（硬件层）作用于环境。 上述层可以在代理技术上构建为构建块（Dib等人，2016年），但不一定;它可能基于云或雾计算服务。智能体提供自主性、反应性和主动性，通过允许预期引入智能自主和认知代理的交互作为多代理系统的一部分进行协作这与CAS属性非常吻合，例如上下文感知、分发、协作和适应。定义5.在签名K上对我们的上下文感知系统的软件层进行建模的偶图GA采用以下形式：加1/4。VA;EA;ctr lA;GA;GA：Z！J哪里VA是抽象双图节点的集合每个节点表示一个计算实体（即，对象、Web服务或代理）。节点集VA使用新的控制在签名K上被识别控制图控制A：V A！K，为每个节点vi2VA分配控制k，2KwithPA¼vjiji2arcv是端口的集合。节点这种抽象允许设计者def¼ y0/X0 · · ·yn-1=Xn-1 ，其中X¼X0] · · · ]X n-1 和选择所需的范例（面向对象、基于服务或Y¼。！y首先，接口层作为不同上下文感知系统部分之间的双向通信媒介（从本地到全局上下文，反之亦然）起着关键作用。其次，它提供了一个最小公共集（内部名称和外部名称面向代理）。E A是计算实体v i之间的链接的集合V A. 使用双图排序定义与节点和链接相关联的语义。定义6.形式上，对上下文感知系统建模的二图G定义为：名称），以构建和发展的bigraphical上下文感知系统，TEM规格最后，通过传记式的写作，GdefAHENV 其中GA;GH和GENV是分别并置，使重要的双图从较小的。3.1.3. Bigraphical specification：硬件层硬件层表示遵循传统观点的上下文感知系统的物理部分（即，不包括操作上下文物理部分）。它被定义为容器抽象的双图，继续我们的上下文感知系统层。G ENV：我！ N; GH：N！ Z和G：Z！ J是满足GA#G H#G ENV是不交的双图.该上下文感知系统（偶图G）是通过将一个偶图层叠在另一个偶图的顶部而将不同层的偶图并置的结果双图G定义为：（服务器、终端、智能手机、平板电脑等），效应器，传感器，GAo GHo GENVdefAHENV和有线通信介质。效应器和传感器可以A H ENV¼GP o GP o GP;电子的和机械的。硬件层的发展是一个主要因素。这些部件可以随着时间的推移（新设备的部署）或由于技术的变化在设计时，该系统表示为一个双图GH。我！ J我们定义了一个扩展签名K，它由一组称为控制的元素定义。对于每个控件，签名提供端口的有限集合和属性的有限集合，其中：Ahmed Taki Eddine DIB和R. 马阿姆里沙特国王大学学报6129PPP¼控制端口的名称，并且属性（K）表示控制的属性。属性采用名称、类型、值>的形式;属性对于描述CAS设备很有用。它可以帮助规范，ify许多设备例如，角色、组、标识符>、等。基于这些属性并使用工具，我们可以执行分析和一些操作。最后，签名K确定原子和非原子控制以及哪个控制是主动的或被动的。分类原则¼抽象偶图GA;GH和GENV上的fH;K;Ug是树属性结构，其中U是一组形成规则，K是一个签名，H是关于库所和环的一组排序.由于我们定义了一个特定领域的建模语言的形式规格说明的上下文感知系统。 我们采用了一种分类原则，抽象偶图GA、GH和GENV。这样的一个学科强加了结构约束，使双图表示模型例如：Petri网的双图排序（Milner，2004）使得使用双图对Petri网建模成为可能。因此，每个模型都由三个参数表示在双图中：（i）在语法上定义过程（排序）;（ii）定义签名K;（iii）然后呈现其交互规则。唯一允许的双图是那些满足定义的排序规则的双图。3.2. 上下文感知系统动力学的双图规范一个上下文感知系统（CAS），必须管理本地上下文（系统）和全局上下文（使用上下文;环境），以感知它们的状态和环境的状态。为此，这些系统需要更多的自适应功能来处理通常在高度变化的环境中运行的开放式、高度并行和交互式组件。所提出的概念框架定义的机制，以处理在本地和全球范围内的双向反应规则的基础上上下文感知系统动态。系统行为和环境变化构成了局部和全局背景动态。此外，建模上下文感知系统考虑确定系统的行为的过程，作为其内部目标解决方案或环境变化的结果。提供上下文感知系统的关键特性，如自感知和自适应。自我意识指的是一个系统所拥有的关于其自身行为和环境的状态（信息），它可以分布或本地保存。此外，自适应提供了灵活适应和重新配置的能力。为了解决这些问题，我们提出了一种基于双图反应系统（双图+反应规则）的工程方法.通过反应来表示过程的动力学 形式R！双图G上的r 森林论坛G：hm;Xi！hn;Yi在i2m处是活动的，如果站点的每个祖先节点我是活跃的。这些反应定义了行为和结构演变。 排序规程之上的BRS包括0BG神经网络富含一组0R反应规则。我们用0BGdef0B GP;0R表示BRS。4. 为例如今，无处不在的计算已经成为我们日常生活中必不可少的，以及在汽车世界。今天的汽车都配备了安全和驾驶员辅助系统，使驾驶员更容易进行旅行。这些系统是分布式的，基于传感器和摄像头网络技术，可以拦截危险，从而降低事故率。这样的系统需要运行时的能力，灵活的适应和连续的重新配置。本节的目的是将我们的方法（之前介绍过）应用于智能车辆（驾驶员辅助系统）作为案例研究。但首先，我们描述智能驾驶辅助系统。然后，我们提出了使用我们的BRS为基础的方法所产生的建模。驾驶辅助系统是一个复杂的系统，它包含多个基于传感器网络和集中式IT的子系统，由大量异构、分布的物理设备组成。该系统感知来自分布式传感器的信号，这些传感器的操作不同（线路传感器、障碍物传感器等）。并在一个动态和多变的环境中工作，其目的是：- 避免可能导致事故的危险情况- 将驾驶员从许多可能降低其警惕性的任务中解放出来;- 协助驾驶员感知环境（超车检测器、冰冻风险检测器等）。上下文感知系统的原理之一是提供专注于与操作环境交互的能力的服务，如（Dey，2001）中所定义的“如果系统使用上下文向用户提供相关信息和/或服务，则系统是上下文感知的。相关性，取决于用户的任务“。我们可以推断，驾驶员辅助系统是环境感知系统的完美示例，因为后者通过其传感器从其环境中感知信息，然后根据其智能（决策过程）使其行为适应其环境。我们设计了智能驾驶辅助系统，以降低城市道路和高速公路上的事故率我们的智能汽车配备了一套传感器、控制模块和执行器，用于分析来自环境的信息，并通过调整其行为、交通和汽车本身来做出反应。行为被表示为一个动作或一组动作，这可能是最好的或最便宜的。4.1. 智能驾驶辅助系统规范在本节中，我们应用bigraphical提出的方法来建模我们的智能驾驶辅助系统。我们使用Bigraph-CAS对驾驶辅助系统的结构方面进行建模。我们定义了智能车辆系统的不同可能场景，该系统管理不同的情况，以避免共谋并促进驾驶员的任务。我们实例化的一组反应规则的Bigraph-CAS模拟这些情况。4.1.1. 智能汽车辅助系统结构首先，我们指定的操作上下文使用的双图GENV，它表示我们的操作环境的上下文实体和它们的逻辑和物理位置的集合。然后，我们对智能驾驶辅助系统硬件组件进行建模通过双图GH来表示ponents。然后，用二图GA对智能决策过程进行建模。在本案例研究中，我们依靠多代理系统来实现应用层。最后，边、超边和接口表示中间件，该中间件允许（i）不同实体之间的交互和通信以及（ii）双图的组合来组成我们的Bigraph-CAS我们的系统的上下文偶图GENV如图3所示。节点正如你所看到的，节点代表与边和超边相互连接的上下文实体，根（0）代表我们系统的操作环境，站点代表抽象元素。类型R的节点是道路的图，这些图包含轨迹的线;这些线可以是连续的或不连续的，O代表障碍物，V代表智能车辆。 我们在这个抽象层次上提出了两个上下文偶图场景，第一个是在“城市”道路上，第二个是在图中表示的“快车道”上。 四、Ahmed Taki Eddine DIB和R. 马阿姆里沙特国王大学学报6130--P图三. 背景图：表2上下文节点bigraphGENV的分类：节点描述控制Arity图形形式V车辆V1O障碍O1LG道路线L1R路R4见图4。 上下文双向图：GENV是对签名K上的潜水员辅助系统的操作环境进行建模的双图，其采用以下形式：GENV¼.VEN V;EEN V;ctr l;GEN V;GEN V：I！N- 打印ENV= mV ENV？VENV;它是一个转换函数，为每个节点分配其父节点。- G ENV =（V ENV; E ENV; ckenENV; link ENV）：I！ N.P LL-link ENV=：I] E ENV！ E ENV] N.- VENV表示上下文节点的集合{R1，R2，R3，R21，R22，R23，R31，R32，R33，V，L1，L2，L3，L21，L22，L23，L31，L32，L33，O}。- EENV表示链路的集合={e1，e2，e3，e4，e5，e6，e7，e8，e9，e10，e11，e12}。- 控制组= {R，R2，R3，V，LG {L，L2，L3}，O}。- G ENV =（V ENV，c ENV，prnt ENV）：m？ n.- 内部名称集={x}。- 外部名称的集合={£}。- m= 20;位点数。- n= 1;区域编号。然后，我们从系统硬件层的规格说明开始，通过双图GH。这个双图表示一个Ahmed Taki Eddine DIB和R. 马阿姆里沙特国王大学学报6131图五.硬件层的双图表示（双图GH）。表3硬件节点偶图节点描述控制Arity图形形式葛事件管理器葛2GM引擎管理器GM2U障碍物传感器U2UG左侧障碍物传感器UG2UD障碍物传感器右侧UD2LDG不连续线路传感器左侧LDG2LDD右侧不连续线路传感器LDD2SG左侧线路传感器SG2SD右侧线路传感器SD2CG左侧闪光灯CG2CD右侧闪光灯CD2S红绿灯S2更低的抽象级别（Meso级别）。它指定了智能汽车的硬件组件及其互连。车辆节点（V），该双图如图5所示，其中表3表示GH图的节点及其图形形式的描述：每个节点表示双图GH中智能车辆的一个物理元件，下面描述每个物理元件的作用（通用电气）事件经理：这元件管理不同来自传感器的输入信号流和朝向其他元件（如发动机、灯等）的输出信号流;在我们的车辆中，该元件起到驾驶员辅助系统存储器的作用（U，UD，UG）障碍物传感器：这些元件检测道路上的物体;这些传感器基于“超声波”原理，反射障碍物并通过产生回波返回其起点。在我们的车辆中，这些传感器（U，UD，UG）位于车辆前部，右后视镜和左后视镜。(LDG、LDD）不连续线传感器：代表检测形成道路轨迹的两条平行线（右和左）的状态的元件;这些传感器基于“光电晶体管”的原理地面来抓住线。在我们的车辆中，这些传感器（LDG，LDD）分别位于车辆的右边缘和左边缘的中间(SLG线传感器：与不连续线传感器（LDG，LDD）相同的原理这些传感器位于车辆的左前角和右前角。(CG、CD）闪光灯：位于车辆拐角处的闪光灯在紧急制动时均亮起，向右侧超车时亮起，向左侧超车时亮起。(S)刹车灯：刹车时会亮。它位于后面。(GM)发动机管理器：负责车辆的制动、加速和转向。图6中表示的GA偶图模拟了我们的驾驶员辅助系统的多智能体级别结构的描述GA偶图节点在表4中分类。代理由一组节点表示。弧表示代表代理之间通信的互连链路，根（0）模拟SMA环境。相比之下，网站代表了最抽象的元素：Ahmed Taki Eddine DIB和R. 马阿姆里沙特国王大学学报6132PL--GG¼f¼FSC 1CASCASCASCASCASCASS01234F见图6。 辅助驾驶系统，Bigraph GA。在我们的多代理系统中，代理是根据他们的角色分布。下面是我们系统中每个代理的角色描述。见图 六、（AGOB）障碍物代理：该代理的作用是感知智能车辆移动过程中出现的障碍物。当检测到障碍物时，后者评估障碍物的距离，然后将其传达给引导代理。该药剂被鉴定为反应性药剂。（AGSL）Line Following Agent：它的作用是感知形成道路轨迹的两条线，因此车辆将通过跟随这些线向前移动，当后者向右或向左倾斜时，Agent将通知飞行员Agent，以便他可以调整车辆的轨迹这种药剂的类型是反应性的（AGDD）超车代理：其作用是收集信息，以便车辆可以从右侧或左侧超车。这个信息是左线或右线的状态，是不连续的，180°左场或180°右场是自由的，也就是说，在右车道或左车道上有物体或车辆。然后智能体将选择空闲车道，这允许他确认超限动作（如果两个车道空闲，则优先级为右侧超车）。所有这些信息的感知和联合的结果将与试点代理人进行沟通。这个代理是认知的。(AGP)引导代理：这个代理与所有的代理进行通信，这个代理是认知的。在接下来的内容中，使用了传记式的写作。我们将由双图GA指定的应用层的软件代理（多代理系统）部署在由偶图GH.结果的偶图表示在图中。7.第一次会议。代数规格如下：G CAS¼ V CAS; E CAS; CN CAS; G CAS; G CAS：m; Z！ 中文（简体）- 弧的集合={e1，e2，e3，e4，e5，e6，e7，e8，e9，e10，e11，e12，e13，e14}。- 对照组={P，OB，SL，D，GE，U，UG，UD，SLG，SLD，LDG，LDD，CG，CD，GM，S}。- G CAS =（V CAS，cR CAS，prnt CAS）：m？n- 打印CAS=MV CAS？VCASn.它是一个转换函数，为每个节点分配其父节点。- G CAS =（V CAS; E CAS; cancel CAS; link CAS）：Z！ J- link CAS =：I] E CAS！ E CAS] N.-ZxP;xD;xAO;xL;xE;xM;xGO;xDO;xO;xDL;xGL;xLDG;xLDD;xCD;xCG;xS是一组内部名称- yP; yD; yAO; yL; yE; yM; yGO; yDO; yO; yDL; yGL; yLDG;yLDD;yCD;yCG;yS是一组外部名称。- m= 18;研究中心编号。- n= 1;区域编号。我们之前提到过，CAS双图是树双图的组合;操作上下文GENV，硬件GH和决策（应用）GA bigraphs，导致我们的智能驾驶辅助系统。4.1.2. 智能汽车辅助系统动态智能车辅助系统的动力学是以描述系统动态性和可重构性的双图反应规则的形式给出的。在本节中，我们定义了一组不同级别的重新配置反应规则。表5给出了定义的反应规则，其表达了可以应用于智能汽车辅助系统部件的一组可能的动作。一个应用的反应规则，定义了一个redex偶图被转换成reactum偶图。由于redex和reactum bigraphs都遵守形成规则UCS，因此反应规则连续地创建根据定义在结构上正确的设置。如果一个偶图被扭曲，反作用将不会执行。最后，我们将表5中定义的所有规则应用于我们的驾驶辅助系统的一些场景。下面是我们系统的一些场景，通过在双图CAS上应用规则来建模。场景1（跟踪线路/轨迹）：车辆将拾取道路的包裹线，然后车辆在此包裹上向前移动。要实现此场景，您需要应用以下规则：RL1RLLFR RLLFL RL 13RL 11初始状态！我们的C！一样大！p是p！resented！图第8和第9条。车辆将检测道路地块线。在这种情况下，我们将在道路级别应用RL1规则和RLSLG、RLSLD规则。所得到的双图描绘在图1A和1B中。 10和11号。然后，AGSL线路跟踪代理将建立通信P L与代理人。因此，必须适用规则RL13这导致图的偶图。 12个。- 代理节点集合VCAS={AGP，AGOB，AGSL，AGDGE，U，UG，UD，SLG、SLD、LDG、LDD、CG、CD、GM、S、V}。它表示一个不相交的双图集合的并集最后，飞行员代理将与通用汽车发动机管理器代理进行通信。后者使车辆向前移动，我们将应用规则RL 11来获得偶图CASF。表4驾驶辅助系统的GA偶图和图形形式的描述节点描述控制Arity图形形式AGOB障碍物O2AGSL线路跟踪代理S2AGD超越剂DG2AGPPilot AgentP2Ahmed Taki Eddine DIB和R. 马阿姆里沙特国王大学学报6133化学式2¼CAS0CAS1CAS2CAS3CAS4CAS5见图7。 硬件和软件双图组成的双图表示。4.1.2.1.场景2（超越障碍）：车辆处于行驶模式。它会感觉到前方有障碍物。它检查他是否可以超车;超车可以向左或向右进行（优先级设置为向左）。因此，车辆将从道路地块移动到右侧或左侧地块，并打开左侧或右侧闪光灯。此场景动态由以下一组反应规则指定：RL3RL 14RL 9RL 5RL D-U！R L17！RL D-！LDG！RLLDD啊！RL4主要的好处是每当所需的属性在实际系统模型中不成立时提供反例BigraphER（Sevegnani和Calder，2016），BPL工具（Gassara等人， 2017）和BigMC（Perrone等人， 2012）是围绕BRS构建的一些验证工具。然而，这些工具都没有达到我们的期望，因为它们是有限的，只适合于某些特定的应用领域。此外，可能的验证依赖于有限的预定义谓词。在本工作中，我们选择Maude LTL模型检测器进行验证R L！UD CA S6R！L16CAS7RL！2CAS8！UDCA S9R！16CAS10并验证了所提出的基于BRS模型的正确性的！CAS11！CAS12！CAS13RLD-CAS14！CAS16RL2RLD-UDRL15！RL6Maude编程语言（Clavel等人，（2007）用于R！LDCAS13啊！CAS14！ CAS15！CAS16实施所获得的CAS传记模型Maude是一-LDDRLLDGRL10！CAS17！CAS18！ CAS F4.2. 智能汽车辅助系统的可执行性及形式化验证软件验证在一般的计算机系统开发中变得必不可少。验证所提出的BRS模型的正确性。有必要选择适当的验证技术以及相应的自动化工具。在文献中有许多形式化的验证技术，模型检测是最流行的一种。其高级编程语言和支持可执行规范的高性能系统。它将用于定义可执行、可分析和可验证的案例研究场景的正式规范。通过案例研究（场景1），验证过程是作为第一步，我们编码结构方面（即，节点及其签名以及外部和内部接口）然后是动态方面（即，反应规则）转换成Maude语言（清单1）。其次，我们制定我们想要验证的属性最后，我们将分析和验证Maude给出的结果输出Ahmed Taki Eddine DIB和R. 马阿姆里沙特国王大学学报6134清单1.二图CAS概念的Maude实现。Ahmed Taki Eddine DIB和R. 马阿姆里沙特国王大学学报6135.... - 是的. ð Þ ð快！ðð Þ ðÞÞ..-是的..ðÞð快！ð ðÞðÞÞ..- 是的-是的.. 你好ðÞð Þ..- 是的-是的.. 你好ðÞð ÞMAS级别RL 13：：线路检测V：.A GPx y：100000。A G O B xy：1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000A G S L x y：100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000A GDx y：400. 去你的！ V：A GPx ye1：d1. A G O B x y：100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000A GSLx ye1：300。A GDxy：400. d0RL 16：检测到障碍物V：VLAG Pxye1e2：VLAD1mm。AGO Bx y：100 €. AGS Lxye1：300 mm。AG Dxy e2：400. 去你的！ V：AG Pxye1：10000 AGOBx y：200万美元。AGS Lxye1：300 mm。AG Dx y：100 mm. d0清单2表示案例研究的初始状态（场景1）。这里转录的Maude命令red modelCheck（initial 1，>[]~GoalNotAcheiv）指出，从当前状态开始，将存在一个通过反应规则步骤可到达的未来状态图13中描绘了执行的结果。结