基于可靠工业物联网的分布式自动化

1 引言

信息技术和嵌入式系统网络的最新进展正在彻底改变制造业，推动其进入一个被称为工业4.0[15]的新阶段。具体而言，为了应对不断变化的市场需求，制造商已采用大规模定制（而非大批量生产）以及个性化生产范式[8]。这是通过快速且经济高效地改变制造系统的结构、功能和容量，确保其具有高水平的灵活性和适应性来实现的[16]。换句话说，正在向可重构制造系统（RMS）转变，该系统可以临时重新配置以支持多种多样的产品。推动RMS发展的最主要使能技术是（工业）物联网（IIoT）和信息物理系统（CPS）[13]。

为确保可扩展性、可转换性和定制化，RMS应基于由工业物联网使能的智能设备——制造现场设备（传感器、工具、机器等）进行模块化构建；这些设备代表信息物理系统（CPS），除了物理设备外，还集成了计算和通信功能，以支持更高水平的自动化/自主性。RMS的能力，包括模块化和可重构性，对控制系统设计提出了新的要求。传统的自动化金字塔结构（每一层设备的自动化程度严格低于上一层）被打破，取而代之的是功能分布在不同且相互通信的现场设备上的控制系统。工业4.0企业的功能基于构成工业物联网的设备（资产）之间的普遍通信，并实现制造过程的纵向、横向及端到端集成[1, 10]。

然而，具有分布式控制/自动化任务的RMS的可靠运行需要智能设备之间的高性能连接。工业物联网连接的关键性能指标包括：（1）网络可用性（故障鲁棒性），（2）数据丢失和传输错误，（3）数据延迟和抖动，以及（4）数据吞吐量[9]。对于分布式工业控制系统而言，可靠通信、数据延迟和抖动至关重要。

工业自动化/控制系统的设计通常以相对较低的抽象级别形式出现，即作为顺序离散事件系统。在工业实践中，GRAFCET标准（IEC 60848）常用于事件驱动的顺序控制任务的功能规范。控制解释型Petri网（CIPN）是GRAFCET的基础形式化方法，二者之间的行为等价性已在[5]中展示。基于此思路，并考虑到CIPN及其Petri网的母体形式化方法（PN）为工业自动化带来的优势，我们最近提出了一种基于CIPN的工业自动化中控制任务分配的方法[12]。具体而言，从全局（即集中式）控制系统的CIPN表示出发——该表示可从符合GRAFCET的设计工具中提取——控制系统功能被自动分配到多个运行在支持IIoT的智能设备上的本地控制器（LC）；在此过程中，所有LC的本地CIPN以及C语言控制代码均被自动生成。为了确保所得到的分布式系统的功能与集中式系统一致，通过通信实现对具有物理访问传感器和执行器权限的LCs的协调。

然而，智能设备之间的通信引发了可靠信息交换的问题，这在安全关键和任务关键的生产系统中至关重要。

GRAFCET和CIPN最初旨在用于建模集中式自动化系统，因此不支持将通信通道模型纳入控制设计和性能分析中。因此，无法保证新获得的分布式系统在真实工业环境中运行时的控制性能。另一方面，PN的母体形式化方法已被用于通信协议的建模与分析[6]，但普遍采用的无线信道的随机特性无法在其内部编码。

因此，我们在广泛采用的控制模型的表达能力与自动综合的分布式控制系统的验证需求之间架起了桥梁。通过将分布式CIPN模型自动转换为随机奖励网（SRN）——一种支持随机时序特性的PN变种，适用于建模通信信道和时变物理执行——实现了这一目标；这使得能够捕捉真实IIoT设计中自动化层面（与控制相关）的影响。SRN已成功用于建模软件/硬件（例如，[4, 18]）、通信协议（例如，[14]）以及分布式系统（例如，[21]）的性能/可靠性。我们利用SRN模型的组合来验证相关系统属性，这些属性基于从系统测量数据中获取并在运行时持续更新的概率分布。违反期望属性的执行场景随后被用来修改分布式CIPN控制器，以避免潜在的故障模式。最后，我们的分析不仅限于设计时阶段。为了支持动态的IIoT环境，我们开发了一种基于边缘的运行时监控系统，在系统模型更新时随时检查关注的属性；SRN模型通过智能设备及监控系统本身获取的实时过程和通信信道测量数据进行持续更新。

本文组织如下：第2节概述了基于CIPN的最先进的分布式自动化建模与设计及其在真实基于IIoT系统中的局限性。第3节介绍了SRN、从CIPN控制器模型的转换以及网络建模。第4节展示了如何利用这些模型进行离线分析和属性验证，并介绍了基于SRN的分布式自动化系统的基于边缘的运行时验证。第5节展示了我们的框架在实际工业案例研究中的应用，最后在第6节给出结论。

2 先进自动化分布及其局限性

有效实现RMS需要快速且可靠的方法，以将控制任务分配给作为本地控制器（LCs）的智能工业物联网设备。然而，系统的控制功能通常使用生成全局（即集中式）控制器描述为CIPN的工具（例如，兼容GRAFCET的工具）来指定集中式控制器。因此，在本文中，我们将采用一种最近提出的将基于CIPN的控制任务分配给LCs[12]的方法，并在本节中概述该方法。我们首先简要介绍Petri网和CIPN。

形式上，Petri网是一个五元组 PN =(P, T, F, W, M0)，其中 P ={P1, …, Pm} 是一组库所（用圆圈图形表示），T ={T1, …, Tn} 是一组变迁（用条形图形表示），满足 P ∪T , œ 且 P ∩T = œ，F ⊆{P ×T} ∪{T ×P} 是连接库所和变迁的弧的集合，W 是弧权向量，M0 是初始标识，表示在网络初始化时哪些库所包含（多少）令牌[20]。在任何时刻，Petri网的状态由其标记定义，即令牌的分布（用库所内的黑色圆圈图形表示），而变迁触发会从某些库所中移除令牌并将其添加到其他库所，从而表示Petri网状态的变化。

控制解释型Petri网（CIPN）是一种PN变种，其中变迁的触发与系统输入（即传感器采样）同步，而控制输出（即执行命令）则由活动库所（即拥有令牌的库所）发出。形式上，CIPN表示为一个六元组CIPN =(P,T, F, C, A, M0)，其中P、T、F和M0分别表示库所、变迁、弧和初始标识的集合，与PNs[5]相同。为了将传感器测量值与CIPN同步，引入了一组逻辑条件C ={C1, …, Cn}；Ci表示传感器值的布尔函数，并分配给相应的变迁Ti。此外，CIPN通过一组动作A ={A1, …, Am}与执行器输出同步；Ai表示分配给库所Pi的一组布尔函数（或其他函数）的执行器输出函数。注意，CIPN中的所有弧权重均为1，且在初始标识M0中仅有一个库所包含令牌。在图形表示中，条件Ci（动作Aj）标注在相应变迁Ti（库所Pj）的旁边（例如见图2）。当某一变迁Ti的所有前序库所均包含令牌且条件Ci满足时，该变迁Ti可以触发，并将令牌传递给后续库所。

基于CIPN的控制任务分配到LCs的方法，从捕获功能表示的全局CIPN开始。

示例

本文采用一个处于拾放配置中的2-DOF工业机械手（图3）作为运行示例。该机械手由两个提供平移自由度的气动双作用气缸（分别记为A和B）以及一个记为C的气动夹爪组成。所有执行器均由电驱动的单稳态5/2双控阀（具有5个端口和2个位置）控制，该阀门通过信号xp、x ∈{a, b, c}触发。其中，小写字母x表示与以大写字母X标记的执行器相关的信号，X ∈{A, B, C}。此外，气缸配备有接近开关，用于检测其完全缩回（原点）和完全伸出（终点）位置；原点位置传感器信号记为x0，终点位置传感器信号记为x1，x ∈{a, b}。系统还配备有一个启动开关st。每个执行器均代表一个带有集成LC的智能现场设备，可直接连接传感器和双控阀。本地控制器（LC）及信号分配如下：i) 气缸A：LC1 ←{ap, a0, a1}；ii) 气缸B：LC2 ←{bp, b0, b1, st}；iii) 夹爪C：LC3 ←{cp}。

机械手的工作过程如下：启动开关（st==1）被激活后，气缸B伸出（由于动作 bp=1）。当气缸B到达终点位置（b1==1）时，夹爪被激活，并在拾取位置（cp=1）夹紧工件。随后，气缸B缩回（bp=0），当其回到原位（b0==1）时，气缸A前进（ap=1）。当气缸A到达终点位置（a1==1）时，气缸B开始伸出（bp=1），当其到达终点位置（b1==1）时，夹爪C在放置位置释放工件（cp=0）。然后，气缸B缩回（bp=0，b0==1），接着气缸A缩回（ap=0，a0==1）。之后循环自动重复，无需再次按下启动开关。定时器确保在气缸B缩回前完成工件的夹紧和释放，即插入一段延迟在命令 cp=1 和 bp=0 之间，以确保从拾取位置提升物体前完成夹紧；放置时同理。

图2显示了一个CIPN，该CIPN使用CIPN形式化方法描述了机械手的全局顺序行为。采用基于CIPN的控制任务分配到LCs后，得到图4中的局部CIPNi。每个CIPNi包含：(i) 根据传感器/执行器映射到LCi从全局CIPN中提取出的带有条件和动作的库所与变迁；以及(ii) 通过令牌传递确保所需控制序列的弧。此外，CIPNi中的某些库所包含向LCj传输特定信号的命令（即通信API调用）。例如，库所PaCTRL_TxB_aEnd包含命令Send(B,a1)，该命令将信息从LC1（气缸A）发送到LC2（气缸B），表示传感器a1已被激活（即1==1 a表示气缸A已到达终点位置）；LC2在变迁TbCTRL_wfAextended.1处接收此信息。LC之间的通信确保分布式系统的行为符合全局指定要求。

然而，不可预测的网络延迟和故障（包括丢包）可能会破坏分布式系统的功能安全。例如，如果从控制器B发送到控制器C的消息未能及时到达控制器C，则工件将处于未夹紧状态，导致工作循环被浪费，或夹爪与工件之间发生碰撞。此外，如果某个气缸未能通知其他部件其已到达终点位置，则整个系统将陷入死锁。需要注意的是，此类情况在集中式控制下不会发生。

因此，为了在真实IIoT环境中确保系统的可靠运行，有必要在考虑真实网络和故障模型的情况下分析分布式控制性能。

为实现这一目标，我们首先提出使用随机奖励网（SRN）对通信和时变执行过程进行建模；该形式化方法支持在适用于定量可靠性及控制相关性能分析的框架中，对通信信道/执行延迟的概率特性进行建模。我们展示了如何使用SRN对物理组件（即被控对象）和通信信道进行建模，以及如何将基于分布式CIPN的控制器模型自动转换为SRN模型。我们还展示了如何期望的系统属性可以通过求解SRN的工具进行指定和高效验证，并介绍如何通过调整局部CIPNi控制器来避免检测到的故障模式。由于基于工业物联网的RMS的部署环境是动态的，我们还引入了一个基于边缘的可靠性和性能运行时监控系统，该系统根据当前系统模型在运行时重新评估属性。接下来，我们将描述图1中框架的各个阶段。

3 分布式顺序控制的网络感知建模

随机奖励网（SRN）通过引入随机变迁触发时间以及用于解决竞争变迁触发的竞争策略，扩展了Petri网的表达能力。此外，还可以指定通用的标记依赖型守卫函数和触发速率。同时，SRN支持标记依赖型奖励函数，该函数可编码任意的系统性能度量，从而实现广泛的可靠性与性能分析[22]。

为了分析非零执行、网络传输延迟和丢包对分布式顺序控制的影响，我们将由CIPNi给出的分布式控制spec转换为SRN模型SRNctrli，i= 1,…,N；我们还添加了由SRNctrli控制的物理组件对应的SRNplant i模型，以及用于建模通信信道的SRNchannelj，j= 1,…,M。

由于CIPN和SRN形式化方法的结构特点，除以下情况外，将局部控制器模型CIPNi转换为SRNctrli在所有库所和变迁上的转换都是直接的：(1) 通过设置控制变量发出执行命令的库所，例如 actr=value，以及由输入信号（传感器值）状态决定条件的变迁，例如 sensor==value；(2) 在库所中用于信号传输的通信API调用，即 Send(目的地,信号)，以及在变迁上等待信号的转移条件，即 转移条件 signal==value。

本质上，例外情况（1）指的是控制器SRNctrli与被控对象SRNplant i之间相互作用的显式建模。在CIPN范式中隐式的、操作系统支持的传感器采样和执行命令发布，必须转换为SRN框架，以便支持控制器和被控对象SRN组合的分析或仿真求解。此外，例外情况（2）涉及通过信道SRNchannel j中介的控制器间的协调建模。在这种情况下，CIPN中隐式的发送/接收范式必须转换为通过信道模型实现控制器间的显式同步，这些模型需要进行组合并求解。

为了解决这些挑战，本节其余部分将介绍对物理组件、网络以及控制器‐网络交互进行建模的方法，而第4节则专注于求解SRN模型。

3.1 建模物理组件

我们首先描述一个由分布式自动化系统控制的物理被控对象的示例模型，以及被控对象与分布式控制器之间的交互，重点突出SRN支持的建模便利性。

3.1.1 设备建模

被控对象的预期行为通常可在设计时获得，因为被控过程（即被控对象）的特性在设计时是已知的。在我们的运行示例中，我们展示了如何建立基于SRN的被控对象模型。

SRN模型如图5(a)所示，对应于图3中的两位线性气动气缸。由于气缸的位置无法在两个终点位置之间进行控制，因此使用库所PaCYL_Retracted和PaCYL_Extended足以表示这两个终点位置（状态）（见图5(a)）。

气缸初始时处于缩回（原点）位置；因此，初始时有一个令牌放置在PaCYL_Retracted中。变迁TaCYL_Extending（TaCYL_Retracting）是一个定时变迁，用于建模伸出（缩回）执行信号与气缸到达终点（原点）位置之间的延迟。如果该延迟是固定的（即在系统运行期间不发生变化），则可以使用确定性触发时间变迁，如图5(a)所示。另一方面，气动气缸在端点位置之间的行程时间上可能并不表现出完全确定性的行为。在这种情况下，可以将确定性时间变迁替换为一个分布，以对行程时间在标称行程时间周围的变动进行建模。

通常，控制器与被控对象交互中的被控对象侧通过在被控对象模型中用依赖于控制器模型标记的函数作为变迁的警戒条件来建模。在我们的示例中，变迁TaCYL_Extending（TaCYL_Retracting）受一个布尔函数g_aCYL_ExtendEn（g_aCYL_RetractEn）的保护——即当控制器模型中存在令牌位于对应命令气缸伸出（缩回）的库所时，该变迁被使能（图5(c)）。下一部分将介绍控制器‐被控对象交互的控制器侧。

注释1. 由于CIPN是工业自动化控制器表示的事实标准，在本研究中我们假设物理被控对象的基于Petri网的模型（例如CIPN或SRN模型）是可获得的。另一方面，如果被控对象模型是以自动机、时间自动机或离散事件系统等形式给出的，这些也是工业自动化中广泛用于模型物理系统动态的其他形式化方法，则可以使用将此类形式化方法转换为符合Petri网的模型的标准方法（例如如[3, 7]中所述）。

3.1.2 建模控制器-被控对象交互

通常，在初始CIPN控制器模型中，以执行器=值形式发出执行命令的库所会被转换为相应SRN控制器模型中的库所，其令牌数量由上述被控对象模型中的保护功能进行评估。例如，为了将图4(a)中CIPN的库所PaCTRL_aCYL_Extend中的命令ap=1映射，在图5(a)中气缸的变迁TaCYL_Extending受到函数g_aCYL_ExtendEn的保护，该函数在气缸的控制器（图5(b)）处于库所PaCTRL_aCYL_Extend时返回1（即，此时发出伸展的执行信号命令），否则返回0。这有效地建模了控制器‐被控对象交互中的执行部分。形式上，控制器将令牌存入使能被控对象变迁的库所；语义上，控制器向本地连接的执行器发送执行命令。

与前述的执行建模类似，在控制器模型中，我们通过在被控对象模型的状态（即，令牌分布）上引入保护功能来建模被控对象的感知。形式上，CIPN控制器模型中每个由传感器==值所触发的变迁被替换为一个受布尔守卫函数保护的立即变迁：当且仅当被控对象模型当前在对应于该传感器读数等于特定值的状态的库所中存在令牌时，该布尔守卫函数的值为1，否则为0。注意，对于复杂变迁（即使用多个传感器的变迁），可同时考虑多个被控对象的库所。虽然也支持对实值变量和更复杂的保护功能进行扩展，但为了简化表述，此处不予讨论。

为了说明这一点，对应于该气缸控制器的CIPN模型的中间控制器模型（图4(a)）是如图5(b)所示，而图5(c)包含了相应的保护功能。在图4(a)中由a0==1保护的变迁TaCTRL_aCYL_Retracted被映射到图5(b)中由函数g_aCTRL_aCYL_Retracted保护的变迁TaCTRL_aCYL_Retracted。注意，该控制器模型仅包含控制器与被控对象之间的交互，并沿用了CIPN通信范式——传输Send(目的地,信号)，以及由信号==值保护的变迁所建模的信号接收。

3.2 建模网络‐控制器交互

在分布式控制器的CIPN模型中，发射器与接收器之间的通信通过一个库所实现：该库所在发射器上发出Send(目的地,信号)命令，而接收器则在其位于接收前的库所到变迁的路径上设置相应的信号==值条件作为守卫，如图6(a)所示。为了使该库所/变迁能够与通信信道交互，需要一种合适的SRN兼容表示。然而，显式的网络建模是(a)介质相关、(b)协议相关和(c)依赖于实现的。例如，图6(c)展示了基于半双工、需要确认应答的单播CSMA‐CA通信信道的模型。尽管其他信道模型也可以同样方便地采用，但在本文中，我们定义了从CIPN到该特定信道模型的SRN兼容表示的发送/接收语义转换。需要注意的是，尽管此模型看似简单，但它捕捉到了在工业物联网部署中实验观察到的通信延迟/故障对应用层（控制相关）的影响。此外，正如我们将在第5节中展示的那样，这种抽象已被成功用于发现现有分布式自动化系统实现中的缺陷。

所考虑的通道可以处于空闲状态、正在发送通信数据包、刚完成发送并准备接收确认应答（ACK），或正在发送ACK，如图6(c)所示。只有当相应的发射器处于对应的发送状态时，变迁Tch_wfTx才被使能。因此，保护函数g_Tx依赖于发射器上Pa_wfTx库所中的令牌数量（即发射器正在发送数据包的位置，如图6(b)所示）。

在存在多个发射器的一般情况下，首先将其令牌存入发送库所（即启动传输）的发射器将触发信道状态的变化。发射器之间的竞争条件可以通过优先级确定性地解决，或通过概率性方式解决。一旦变迁Tch_wfTx被使能，信道模型中的令牌便可转移到库所Pch_TxBusy。

（即信道状态发生改变），并在此状态下保持，直到模拟网络/信道引起的延迟的随机时间变迁 Tch_Tx 发生。此外，一旦 Tch_Tx 发生，数据包被发送，从而触发变迁 Ta_wfTx，使发射器进入等待确认状态。因此，当信道已准备好传输确认应答（Pch_Txd 中的令牌），且发射器正在等待确认应答（Pa_wfAck 中的令牌）时，接收器接收到数据包，转移到库所 Pb_TxAck（即变迁 Tb_wfRx 发生）。这描述了数据包传输模型。

消息传输后，信道模型进入Pch_AckBusy状态，因为变迁Tch_wfAck被使能。此时，接收器立即继续执行，因为确认应答由通信栈的低层处理。因此，接收器的令牌通过Tb_TxAck向前推进，完成接收器在分组交换中的活动。另一方面，发射器在Ta_wfAck处被守卫条件g_TxFin阻塞，直到确认应答在信道中传播完毕。信道在随机触发时间变迁Tch_AckTx发生前一直处于忙于传输确认应答的状态，之后信道返回空闲状态，并使发射器进入Pa_TxDone状态，从而完成确认过程。

请注意，除了对事件顺序进行建模外，SRN模型还能够捕捉传输时间（time‐to‐transmit）和确认时间（time‐to‐ACK），我们使用两个独立的随机时间转换来建模这两个参数。这使得可以采用更真实的模型，其中ACK数据包由于远短于原始数据包，因此传播速度要快得多，并且总是在成功完成完整数据包传输后立即发生。完整的发射器/接收器和信道模型如图6(b)‐(d)所示。为了提高可读性，在图6(b)和(c)中，变迁和库所根据其依赖关系进行了着色。

此外，该模型引入了两种竞争条件，分别存在于变迁Tch_wfTx与Ta_wfAck之间，以及Tch_wfAck与Tb_TxAck之间。在这两种情况下，相互竞争的变迁同时被使能，前一个变迁的触发会禁用后一个变迁（Petri网中不允许同时触发变迁）。在第一种情况下，当发射器A接收到确认应答时，保护条件g_TxFin不再抑制Ta_wfAck，因为通道处于Pch_Idle状态。然而，Pch_Idle中的令牌也允许另一个发射器A’将通道状态从Pch_Idle变为Pch_TxBusy，从而禁用了Ta_wfAck。在第二种情况下，由于接收器已准备通过确认应答发送推进（Tb_TxAck被使能），同时通道也准备开始传输确认应答（Tch_wfAck被使能），Tb_TxAck的触发会移除Pb_TxAck中的令牌，从而禁用Tch_wfAck；这导致保护条件g_Ack抑制Tch_wfAck。

我们通过分配变迁优先级来处理；如果prio(Ta_wfAck)> prio(Tch_wfTx)且prio(Tch_wfAck)>prio(Tb_TxAck)，则竞争条件被正确解决；这在语义上是正确的，因为在基于CSMA‐CA的网络中，第一个发射器必须完成传输后，另一个发射器才能开始下一次传输（第一种情况），并且接收器在接收到数据包后必须先启动确认应答的传输，然后才能继续执行（第二种情况）。

备注2. 所提出的建模方法具有灵活性，可针对不同的物理层和MAC层变体进行调整。例如，如果低关键性传输不需要确认应答，则可通过移除对确认应答发送/接收进行建模的库所和变迁，轻松修改上述信道模型。也可考虑诸如多次重试机制等底层协议特性。例如，标准的基于指数的重传退避可通过在传输失败时概率性地从Pch_TxBusy库所冲刷令牌，并以随机速率注入新令牌来建模。其他随机退避模型同样适用。

此外，在所提出的模型中，接收器通过受g_Rx保护的Tb_wfRx变迁推进到发送确认应答的操作，该保护条件依赖于通道和发射器的标记。这确保了在存在多个接收器的情况下，只有被激活的发射器所指向的接收器才能继续执行；即，该通道为单播。通过简单修改保护函数g_Rx，即可建模多播或广播通道。为了表述清晰，本文始终采用图6中的通信模型，该模型适用于我们案例研究背后的网络。有关使用Petri网对通信与协作协议建模的更多细节，请参见[6]。

示例（具有2自由度的工业机械臂）。 我们使用了所提出的方法论，将分布式CIPN控制器转换为SRN模型，该模型还捕捉了控制器之间的通信（即网络连接），从而将图4中的CIPN模型完整地转换为图7所示的SRN模型。下一节通过引入可形式化编码的功能和安全属性来分析模型的实用性，这些属性可在支持SRN分析的工具中进行验证。

4 系统分析与验证

基于SRN开发的模型可用于验证期望的系统属性。给定网络的概率分布延迟、执行器和被控对象响应时间以及控制器设置作为输入，可以使用PN软件包进行系统分析。如果所有定时变迁均为立即的或具有指数型触发时间，则可使用解析/数值方法[11, 22]求解模型。另一方面，对于一般分布的触发时间，则执行离散事件仿真。由于在大多数IIoT应用中假设触发时间为指数分布或立即的是不成立的，我们采用随机Petri网软件包（SPNP）[11]，该软件包也支持离散事件仿真以进行定量系统分析。接下来，我们讨论相关系统属性的规约以及所采用的设计时和运行时验证设置。

4.1 系统属性的指定

Safety Properties. Safety properties can be defined as reward functions——即控制器和被控对象状态（即标记）的任意函数，这些函数在每次标记更新时（即离散仿真步）进行评估。例如，在我们的运行示例中，当气缸B向下推进靠近工件时，夹爪C绝不能处于闭合状态；否则将导致夹爪与工件发生碰撞。如果当mark(PcGRIP_Gripped)==1 AND mark(PbCTRL_bCYL_Extend1)==1成立时，安全属性被违反。因此，使用一个布尔奖励函数，在条件成立时返回1，否则返回0，以评估此类事件的发生概率；任何非零的发生概率都被用作潜在安全违规的指示。为了简化表示法，我们将此类形式的函数记为R()= if(BooleanCondition,ValueIfTrue,ValueIfFalse)。

对于我们的运行示例，当网络引起的通信延迟为指数分布时（数据包延迟的速率参数为1/200，而确认应答的速率参数为1/1000），SPNP返回结果显示系统是安全的。在第5节中，我们使用从已部署系统获取的实际信道测量数据，通过SPNP工具进行分析。

活性属性。 除了安全之外，确保系统能够向前进展并按照期望的性能规范运行也非常重要；我们在此稍为滥用术语，将这些称为活性属性。SRN模型的分析结果为每个库所和变迁提供一组平均度量值。对于库所，包括标记的平均数量和库所处于某种状态的平均概率可以定义非空。这些度量可提供系统在特定状态下的驻留时间信息。例如，我们预期通道在Pch_Txd库所的驻留时间为零，否则将表明确认应答传输存在问题（可通过在SPNP中分析模型来验证）。此外，执行器系统的执行动作时间通常受到特定上限的限制。在我们的运行示例中，气动气缸处于伸出或缩回状态的概率可用于计算机械部件的平均占空比，进而用于验证系统是否在预设限制内运行，或预测磨损的增加。

相反，可以定义令牌通过每个变迁的平均吞吐量，以及变迁处于使能状态的概率。变迁的吞吐量可用作性能指标；例如，针对我们的运行示例中的拾取与放置循环的执行速度——使用SPNP进行分析表明，所有控制器变迁的吞吐量为0.295 tokens/sec， resulting in the processing time of 3.389 sec/unit。

4.2 基于SRN的系统分析

所推导的SRN模型用于借助现有的支持PN的工具进行设计时和运行时系统的安全性和性能分析。

基于Petri网的工具的功能。 当使用解析/数值方法时，可以在构造可达性图的同时确定安全属性的违规情况；即无需统计仿真即可识别出不良标记。另一方面，如果执行离散事件仿真（例如，在具有非指数分布的触发时间的情况下），则关于违反安全属性的标记是否可达需基于每次仿真运行的结果来确定；即所得结果转化为概率性保证。两种广泛使用的基于Petri网的工具是[2, 11]，它们为解析/数值和仿真求解模式均实现了一类停止准则。因此，一旦检测到安全属性违规（即，达到不良状态的非零概率），分析即可终止。

运行时监控支持。 各种运行时效应，如通信通道利用率、组件老化和机械磨损，可能会影响所开发模型的参数；因此，在设计时（即离线）基于最初获得的SRN模型进行的系统分析结果，在系统执行期间可能不再适用。因此，能够在运行时检查静态属性违规对于可靠性和性能监控至关重要。我们探索了对分布式自动化系统的运行时监控支持；基于PN的工具的停止准则功能对于运行时安全验证非常有用，因为监控器可以在完成完整分析之前，就预测到不可靠性而收到警告。

我们开发了一个执行环境，其中实时获取过程测量值（例如，气缸行程时间）和信道特征（例如，数据包传播延迟），并用于对SRN模型内概率特征的预设参数进行运行时适应。为了确保在带宽受限的基于IIoT的部署中实现及时响应，我们探索将模型检查工具的执行放在边缘而非云上（详细信息见第5节）。基于边缘的监控部署在基于IIoT的自动化中自然得到推广，因为此类系统在设计上就包含持续供电的网关设备，支持高层级协调和决策。

注释3（估计分布与直接使用基于样本的测量）。 最先进的PN工具支持变迁触发时间的参数化规范，符合大多数深入研究的概率密度函数（超过15种分布），适用于灵活建模离散事件过程[2, 11]。在此设定下，通过将分布拟合到离线数据以创建实际系统的精确模型。然而，最先进的工具也支持基于样本的触发时间——即求解器在仿真期间可以从运行时测量获得的触发时间数组中进行采样，而不是从预定义分布生成随机样本[11]。我们的系统能够利用此功能，从而省去对采集数据拟合概率分布的额外步骤，提高所获得度量与实际系统的统计适配性。因此，尽管使用离线数据拟合模型的分析方法存在，但我们在线基于边缘的性能与可靠性监控不依赖于独立同分布假设，因为它采用的是运行时获取的过程和通道测量。

5 个工业案例研究

在两个真实工业案例研究中，我们展示了本方法论在支持IIoT的分布式自动化中的适用性：（I）三自由度气动机械手，以及（II）具有并行过程的复杂气动机械手。所考虑的机械手并非传统类型；它们在机械子系统及其控制（使用智能IoT设备）方面采用模块化设计，以方便重新配置。此外，所考虑的控制场景也不遵循传统的IEC 62264分层式工业自动化金字塔。尽管我们的评估仅限于物理测试平台中的机械手，但该方法同样适用于其他支持IIoT的设备。

在两个案例研究中，我们均从使用现有技术获得的分布式控制模型开始。我们将这些CIPN转换为SRN，并利用开发的被控对象和信道模型进行分析。我们首先展示如何发现在真实IIoT环境中运行的现有分布式控制器可能出现的潜在问题，然后展示如何通过在代码生成阶段引入补丁（通过引入适当的通信结构并利用LC运行时支持）来解决这些问题。

5.1 案例研究一：3自由度工业机械手

5.1.1 物理装置与建模

所考虑的机械手配置为在拾取位置抓取一个工件，将其转移至浸入位置并浸入液体中，从液体中缩回工件，通过旋转甩掉多余液体，并将工件返回原始位置。带有高亮组件的气缸配置如图8(a)所示，而系统上部（即气缸部分）如图8(b1)所示。提供平移自由度的气缸A和B，以及提供旋转自由度的气缸C，均配备有末端位置传感器，而夹爪D则没有（与我们的运行示例类似）。每个气缸模块均由基于ARM Cortex‐M3的低成本NXP LPC1768微控制器（即图8(b2)中的LC）控制，工作频率为96MHz。所有LC执行由形式化CIPN描述通过我们框架[12]生成的C代码。最后，LCs通过符合IEEE 802.15.4标准的无线模块形成一个低功耗、低延迟的网络。

通过使用现有框架[12]获得的局部CIPN控制器模型被转换为SRN兼容的表示形式，被控对象和信道模型则按照第3节中所述进行开发。被控对象模型参数（即气缸行程时间）来自实验测量，因为它们依赖于多个外部参数（例如控制阀设定、额定气压）。因此，在SRN模型中，气缸响应时间（即从初始位置到终点位置的行程时间）采用均匀分布建模，其参数见表1。

同样，信道参数（即传播延迟分布）是从物理装置获取的数据中得出的。图9显示了在两天内进行实验所获得的发送到接收和接收至确认时间的直方图，表明系统在标称条件下运行时变化较小。采用截断正态分布，其参数为μ = 4.84ms，σ= 4.7· 10−6，xmin= 4.83ms，xmax= 4.85ms用于Tx → Rx，以及μ = 0.57ms，σ= 4.7· 10−6，xmin= 0.56ms，xmax= 0.58ms用于Rx → Ack时间；这些参数用于离线系统验证。为了涵盖环境和运行条件可能发生显著变化的情况，概率分布参数在运行时进行更新。

5.1.2 验证与运行时监控

我们在基于Intel Core i3的NUC平台上运行SPNP，该平台适用于基于边缘的近网关部署。NUC平台通过收集分布式控制器之间事件触发的通信数据包，并接收来自控制器自身的附加诊断测量数据（例如气缸行程时间、执行到感知延迟），实现对已部署工业机械手的监控，这些诊断数据是通过使用Microchip ZENA IEEE 802.15.4兼容适配器进行本地在线监测获得的。

我们考虑了由领域专家规定的一系列详尽的安全与活性属性。为了说明我们的方法，本文重点讨论以下属性：

属性1（气缸A行程期间夹爪D始终处于夹紧状态）。 违反此属性意味着工件在拾取/放置位置与浸入位置之间转移过程中掉落，可能导致工件和/或操作器平台损坏。我们添加指示此属性违规的奖励函数如下：R1()= if((mark(PdGRIP_夹持)==0 AND mark(PaCTRL_aCYL_Extend)==1) OR ((mark(PdGRIP_Gripped)==0 AND mark(PaCTRL_aCYL_Retract)==1)),1,0).

属性2（在气缸B接近工件行程期间，夹爪D始终处于释放状态）。 违反此属性意味着夹爪与工件之间发生碰撞。表示属性违规的奖励函数定义为：R2()= if((mark(PdGRIP_Released)==0 AND mark(PbCTRL_bCYL_Extend1)==1,1,0).

属性3（气缸C占空比至少为5.5%）。 违反此属性意味着工件浸入后发生突然旋转，导致机械部件磨损加剧。库所PcCTRL_RotateCW和PcCTRL_RotateCCW collectively 表示气缸C旋转的时间比例。

属性4（机械手以最大速率为3秒/工件）处理工件。 违反此属性意味着机械磨损增加，并可能导致向周边制造系统供料的速率高于预期，从而引发潜在问题。任何控制器的变迁的平均吞吐量都反映了这一活性属性（即控制器返回其初始状态的速率等于工件被处理的速率）。

此外，我们考虑了在系统操作过程中观察到的以下代表性场景。

场景1（正常系统运行）。 此场景涉及使用正常被控对象参数，以及在部署时对应于实验测量所获得的信道模型（即第5.1.1节中的参数）；我们的实验表明，在正常工作条件下，模型参数不会发生显著变化。

场景2（拥塞导致的网络不可用）。 由于通道利用率增加，网络数据包可能出现比正常情况更高的延迟或丢失率；我们的实验表明，在此类条件下可能会出现双峰（或多峰）分布。当引入大量额外的LCs并全部使用相同的无线信道进行通信时，观察到了场景2。为了以一种符合实际的方式实现该场景并提高信道利用率（在信道的时间和带宽需求方面），我们模拟了额外的气动机械手，这些机械手类似于此处考虑的实际机械手——即，运行示例和案例研究I/II中的机械手混合体通过实际控制器实现，但采用软件模拟气缸。

场景3（组件故障 – 由于气压控制系统故障导致气压逐渐增大）。 由于气压控制系统出现故障，导致输送至气动气缸的气压增大，从而引起气缸响应时间（即终点位置之间的行程时间）逐渐缩短。我们通过逐步增加气动系统中的气压来模拟组件故障，从而实现了场景3。

5.1.3 结果

表2 显示了针对这些属性的模型分析结果。在NUC上，SNPN中平均模型分析运行时间捕获了1000次持续时间为1000秒（> 200次机械手循环）的离散事件仿真，为28.2 秒。由于集中式控制系统设计上正确，并且在标称条件（场景1）下无线通信在本地控制器之间不会引起显著的延迟和丢包，系统表现符合预期（气缸C平均占空比为6.1208%，平均零件加工时间为3.9368秒），且安全属性未被违反。图11（顶部）展示了在标称条件下一次机械手运行样本期间获取的事件序列。

在场景2中，由于夹爪D未配备末端位置传感（因其尺寸限制），控制器B与控制器D之间的通信最为脆弱；根据设计，控制器B向控制器D发送夹紧指令，并确定性地等待500 ms，假设操作在此时间过后已完成。如果通信数据包失败，例如，在此场景的实验运行期间，当气缸B从拾取位置缩回工件前，控制器D本应夹紧工件，却可能使夹爪D处于释放状态，如图11（底部）所示。

根据我们的运行时分析，我们发现协议级重试不足以实现可靠的数据包传输。通常，图6(c)中所示的信道模型并未涵盖失败的传输，而这些失败传输占所有数据包传输的3%。通过对导出模型进行分析，我们得到属性P1和P2违反的概率显著（分别为26.9%和3.3%）。对于控制器A、B和C而言，通信失败会导致死锁；本质上，接收控制器始终等待信号以继续执行，且（不成功的）发射器耗尽了协议级重试。由于通信中断导致系统经常停止，在表2中省略了气缸C的平均占空比和生产率。

因此，我们利用所提出的SRN模型分析所支持的推理来修改CIPN通信语义的转换；我们在为LCs进行代码生成时引入应用层传输重试。相应地，我们还重新设计了信道模型以适应这一变化；图10展示了相对于图6(b)改进后的信道模型。我们使用LCs中修改后的通信API语义重新部署了整个分布式系统，并复现了场景2。结果表明，在此情况下，尽管存在网络拥塞，系统仍能安全运行，且仅出现轻微性能下降——即由于应用层重传处理延迟，单个零件平均处理时间增加了 ∼ 0.03sec。需要注意的是，成功传输概率在运行时动态更新（如第4.2节所示），以避免在非拥塞部署场景下产生过于保守的结果，并在动态运行时条件下最大化分析准确性。此外，SPNP工具的离散事件分析在NUC上平均耗时28.6sec，而判断可能的安全违规仅需313.6 ms（比系统的周期时间低一个数量级），从而防止了故障系统操作。

最后，在场景3中，由于气压逐渐升高，工件被加工的平均速率提高，气缸C占空比降低，这可能危及工艺质量并增加部件磨损。随着时间推移，零件加工时间减少至3.2154sec，气缸C占空比下降至5.6214%，如表2所示。离散事件模型仿真利用增量信道和过程测量，在NUC上平均耗时29.7sec，并警告监控器系统性能正在下降。该信息用于在系统性能降至可接受限值以下之前纠正故障。

5.2 案例研究II：具有并行过程的工业机械手

机械手采用并行装卸配置；它由两个（并行的）气缸A和B以及一个旋转气缸C组成。旋转气缸用于转动带工件的底座，而气缸A和B则并行进行工件的装卸。集中式控制器的CIPN模型如图13(a)所示。现有的本地控制器的CIPN模型如图13(b)、(c)所示。

这种气缸配置特别值得关注，因为气缸A和B需要同时伸出行程以装卸工件；因此，在控制器C发出指令后（随后完成气缸C的旋转运动），在分布式设置下的控制器A和B必须同时向各自的气缸发出伸出行程的执行命令。虽然从控制器C到控制器A和B的通信可以使用组播协议实现，但必须确保气缸A和B都能接收到信号，并同步发出执行命令。

另一方面，虽然广播是支持的，但先前的案例研究中采用的IEEE 802.15.4低功耗无线通信标准并不原生支持组播通信。尽管已有一些通过IPv6协议实现组播通信的研究（例如，[19]），但无法保证在多个接收节点上的数据包的同步传输和处理。

在对按照第3.12节所述方法获得的SRN模型进行分析时，我们再次发现需要调整控制器通信语义的转换（即图6(b)中的转换），因为所得的分布式自动化系统违反了安全属性。例如，若仅有控制器A或B之一接收到数据包并开始执行动作，则系统将进入错误状态；例如，新的工件被加载到尚未卸载的前一个工件之上。

因此，我们在从CIPN转换为代码生成的过程中修改了通信API的语义，以利用[17]中设计的低功耗、低带宽同步协议，该协议与我们的LC平台实现完全兼容。当采用该同步协议时，一旦控制器A和B均接收到控制器C的信号，即可实现对控制器A和B上执行命令的同步执行。这可能会引入额外的延迟，因为在控制器A和B之间增加了额外的握手过程，以及气缸C与A、C与B之间潜在的额外重传，而这些在基于CIPN的分布式自动化模型中原本是不存在的。尽管如此，在生产周期时间最多增加100ms的情况下，实现了气缸A和B行程的亚10μs级同步，从而获得了一个可验证的安全系统。

6 结论

本文提出了一种方法论，该方法论以工业自动化中广泛使用的基于CIPN的控制器模型作为输入，这些模型排除了对分布式自动化部署的正确性和容错性分析。此类模型被转换为一种原生支持通信信道和系统故障随机建模的SRN兼容表示。我们展示了如何在SRN范式内对分布式自动化系统进行具有概率保证的分析/验证。此外，我们改进了现有的基于SRN模型结果的分布式控制代码自动综合策略。为了支持基于IIoT的自动化系统的动态部署环境，我们验证了一种基于边缘的监控系统的可行性，该系统在运行时根据持续更新的实时过程和网络信道测量数据重新检查相关系统属性。我们在包括工业机械手在内的真实案例研究中评估了我们的方法。未来的方向，我们将探索在控制器和信道模型中引入真正的非确定性，这将使我们能够捕捉对分布式自动化系统的对抗性影响。

两位气动缸的SRN模型；(b) 气缸A的控制器扩展模型（来自图4(a)）（该模型不是SRN，因其仍保留通信API）——被控对象‐控制器交互通过由被控对象和控制器标记的布尔函数(c)所守卫的变迁来描述。)

和图6(c)所示；保护功能根据其中所示模式定义。)

3自由度工业机械手；(b1) 气缸A和B提供平移自由度，气缸C提供旋转自由度，夹爪D处理工件；每个部件均由低成本基于ARM Cortex‐M3的逻辑控制器控制 (b2)。尺寸和功耗感知的NUC(b3)监控系统性能（气动气缸未按比例绘制至逻辑控制器和NUC）。)

属性	场景下的平均违规概率 (S1) 标称条件	场景下的平均违规概率 (S2) 因拥塞导致网络不可用	场景下的平均违规概率 (S3) 气压控制故障 无应用层重试	场景下的平均违规概率 (S3) 气压控制故障 有应用层重试
(P1)	0.0000	0.2690[0.2459, 0.2908]	0.0000	0.0000
(P2)	0.0000	0.0330[0.0237, 0.0423]	0.0000	0.0000
属性	气缸C平均占空比[%]	气缸C平均占空比[%]	气缸C平均占空比[%]	气缸C平均占空比[%]
(P3)	6.1208[6.1202，6.1213]	—	6.0761[6.0754，6.0768]	5.6214[5.6210, 5.6218]
属性	平均吞吐量的倒数 [seconds per unit]	平均吞吐量的倒数 [seconds per unit]	平均吞吐量的倒数 [seconds per unit]	平均吞吐量的倒数 [seconds per unit]
(P4)	3.9368[3.9366，3.9370]	—	3.9671[3.9668, 3.9674]	3.2154[3.2152, 3.2156]

表2： 案例研究一：不同场景下的属性违规概率和性能指标；对于由于拥塞导致网络不可用且无应用层重试的情况，由于频繁的操作中断，未给出性能指标。置信区间按99%置信度计算。