售前咨询-朱:19381904226
售前咨询-杨:19381903226 English
前沿资讯 真实、准确的物联网、互联网行业新闻

低水滴压电模型电压采集器

你的位置: 网站首页 新闻动态 技术应用
低水滴压电模型电压采集器(下)
2022-07-24 17:44:06 阅读: 发布人:纵横智控

4. PLC模型检查

PLC被广泛应用在许多应用中,并且有许多设备;这是一个很大的研究领域。任何PLC工作在包括不同设备和人,所以PLC系统是并发的。同时,个

PLC系统如果有一些错误很难发现,主要是因为逻辑设计错误,但不是计算错误。所以我们专注于PLC的检测程序逻辑过程,而这个逻辑完全可以

位逻辑描述。因此,为了简化PLC程序模型,专注于模型检查,我们进行以下设置:

 PLC是一个逻辑控制程序,所有的控制变量只有0和1两个状态;

 PLC 程序在并发环境中运行。在这种情况下,PLC编程更可能有有些错误不容易发现。针对以上特点,我们采用模型检查工具 SPIN(我们的具 PLC-Checker 也在上述建立的模型上实现了 NuSMV)检查。我们制定了一系列的转换规则,将上述模型构建成SPIN的输入语言Pro mela,系统属性也需要翻译成Promela,SPIN 将它们放在一起然后执行检测。PROMELA 语言是 C 类语言,它们是语义相似。所以我们只举一些例子

显示翻译的基本概念。要查看PROMELA 语言的详细信息,请访问 www.spin root.com。我们将介绍 PRO MELA 文件的三个部分作为 SPIN 的输入。

1)PLC控制器代码

PLC控制器由多个网络组成。

PLC控制器的代码也是从网络生成的。当然,在此之前,您应该声明您需要的变量。每个网络都有其输入端口和输出端口,每个端口都可以用布尔表达式表示。我们通过逻辑分配输出端口的值

计算所有输入端口。这是翻译

PLC网络的方法。

下面是一个转换 SR 网络的例子:

if  :: Exp(R) == 1 -> Q = 0;  ::else ->   if ::Exp(S) == 1 -> Q = 1;   ::else -> skip; fi;  fi;  /* Exp(S) is the Boolean expression of S port   Exp(R) is the Boolean expression of R port   Q is the output port */


2)并发实体的代码

我们认为每个并发实体都是一个独特的过程,没有不管是人的行为还是设备。 这些过程与 PLC 控制器进程共享变量。 这必须是确保系统的并发性。在本文的第二部分,我们讨论了所有并发实体被建模为自动机。 这自动机的意思是从一种状态转移到另一种状态。我们使用 I 端口来形成实体的状态。 利用goto 语句作为转移(就像在汇编语言中一样)。 一个简单的例子如下所示:


atomic {  if  :: Q1 -> {IB, goto StateB}  :: Q2 -> {IC, goto StateC}  fi;}  /* StateA is the label of State A   Q1, Q2 is the condition of transfer   IB is to set the state value to the value of state B   goto StateB means jump to stateB */

RTU

3) 财产代码

属性是PLC系统必须遵守的规则。我们使用 LTL(线性时间逻辑)公式作为输入格式。我们应该写相反的财产,因为SPIN的机制。 SPIN 会发现我们的情况财产发生,那应该是一个反例。我们不能直接写 LTL 公式,而是使用 ing 宏。首先我们应该定义所有的命题在 LTL 中的宏中(如 #define p i5 == 0),那么我们使用定义的命题来形成 LTL 公式。旋转可以使用“SPIN-f”指令自动将 LTL 公式转换为 PRO MELA 代码(查看更多SPIN 手册中的详细信息)。

4) 通知等待机制

在建模讨论中,我们建议不添加时间等待机制。这种机制也需要体现在代码中。具体实现是签一个每个非 PLC 进程的位变量(所有进程PLC 控制器除外)作为信号。当自动机转移到状态标签,信号变量设置为0,并且下一个赋值要求这个变量为 1 才能继续。由于 PROMELA 语法特征,该过程将继续进行。在PLC过程中没有此类限制,相反,PLC 进程可以设置这些变量为1,从而确保每一步都必须走通过至少一次 PLC 扫描来完成就是这样称为通知等待机制。

按照上面的四个步骤;我们得到一个完整的代码我们系统的 SPIN 输入文件。然后我们可以使用 SPIN检查模型。 SPIN模型的操作步骤检查器,请参阅 SPIN 手册(访问 www.spin root.com)。 SPIN会给出是否找到反例的结果,我们可以用理论来分析上面提到了 spin 给出的跟踪文件。使用这种检测机制,我们开发了一个工具模型检查 PLC-checker。它有助于建立视觉模型和执行检查,并可以给出对结果进行简单分析。当然,它找到的反例应该手动检查以使确定它是否是一个真正的反例。然而,随着在trail文件的帮助下,这不是一个非常困难的任务。我们还成功地使用了一些检查PLC 检查器(显示在下一节中)。在经典教科书的例子,找到了一个反例。虽然反例的发生概率非常低,但确实会发生并且可能会产生严重的后果。这个工具也证明了正确性和本文理论的有效性。


5. 运行 PLC-Checker

我们将通过以下方式展示 PLC 检查器的有效性检查两门通道模型。 两门通道用于防止封闭的房间与外面的世界。

通过输入梯形图和并发实体进入工具,也就是属性的定义,我们执行一下检查。 图 3 显示了结果。如我们所见,结果中有一个错误。 这是通过检查线索证明是一个真正的反例手动归档。 也就是说我们的机制是有效的在检查此类 PLC 程序时。


6。结论

我们研究PLC的建模和检查理论本文采用形式化方法。 要求分析了PLC建模的特点,通过时间间隔策略建立了并发实体模型。然后我们证明时间间隔模型是一个超集PLC系统,并通过增加无时间等待机制减少模型。 它还确保了所有的变化系统可由PLC控制器扫描。 我们发现通过检查系统的反例来找出系统的错误。 最后,SPIN的使用方式检查模型给出。 还有对应的介绍了模型检查工具PLC-Checker。 在这个阶段,该机制还有很不完善的地方,比如作为定时器的处理。 但它有伟大而独特的解决状态探索问题的优势。我们仍在积极探索此类问题。


友情链接