售前咨询-李:13308089138
售前咨询-吴:17760489178 English
前沿资讯 真实、准确的物联网、互联网行业新闻

PLC建模,PLC建模与校验方法

你的位置: 网站首页 新闻动态 技术应用
基于形式的PLC建模与校验方法(上)
2022-07-21 23:49:39 阅读: 发布人:纵横智控

高可靠性是电气控制设备性能的关键。 PLC结合了计算机技术、自动控制技术和通讯技术,广泛应用于工业过程的自动化。 传统的验证方法无法满足复杂PLC系统的一些要求。 在这个本文提出了一种高效的PLC系统建模和验证方法。 为了保证PLC的高速性能,我们提出了“时间间隔模型”和“通知等待”技术。 它可以减少状态空间并使验证一些复杂的 PLC 系统成为可能。 此外,还获得了从建立的PLC模型到Promela语言的转换,并设计了一个用于PLC系统建模和检查的工具PLC-Checker。 使用PLC-Checker 检查一个经典的 PLC 例子,找到一个反例。 虽然这种逻辑错误发生的概率很小,但可能会导致系统死机。

一、简介

PLC是一种自动控制设备,可以接收来自传感器、计算设备或其他PLC的信息逻辑输入信号,输出处理后的逻辑信号。

控制算法可以使用标准语言编写,例如梯形图 (LD)、结构化文本(ST) 或指令列表 (IL) [1]。

PLC使用可编程语言的技术控制大规模集成电路已广泛应用工业[2]。由于安全关键软件可以对生命或财产造成严重损害,核实安全关键软件已成为不可或缺的一步保证软件质量的必要条件。目前的验证PLC的方法仍然停留在仿真和测试上。但是,它们并不能涵盖所有可能的情况,尤其是 PLC 的设计模型是否满足需求。因此,引入了模型检查技术进入PLC领域。对PLC进行理论分析设计变得很重要。

PLC模型检查的首要步骤是建立PLC模型,比如建立一个模型来自功能图 [3]。 PLC模型侧重于建立时间属性[4]。可以建模通过时间自动机[5]的方法或时间段建模方法[6]。因此模型的状态空间将是与定时自动机相比减少了。无论哪种方式选择,最终可以给出一个抽象模型[7]。如何建立一个好的PLC抽象模型是检验的重中之重。作为手动建模容易引入很多错误,所以建立一个集成的建模和测试工具非常重要,这是本文关注的问题之一。

PLC控制程序在实时操作系统中运行(多任务或单任务);本文主要基于多任务调度PLC系统。第 2 节文章介绍了建模方法PLC系统。第 3 节给出了该模型的分析和改进,因为我们需要降低伪错误。第四节设计了一个模型检查工具PLC-Checker 检查已建立的模型,包括介绍PLC程序转换成SPIN的方法输入语言 Promela 代码。最后,一个经典的 PLC示例用于检查和关键的计算机示例由 PLC-Checker 发现。

RTU

2.PLC建模*

这项工作由 NSFC 60973049、60635020 和 TNList 资助跨学科基础。模型检查分为三个步骤:建模、属性描述和验证。最重要的是如何建立系统模型。在系统中,PLC控制器不是孤立的,而是具有与工作环境、驾驶员和人的交互[8]。因此,这些因素也应该建模。环境、人、PLC控制器在逻辑上相互独立和并行。此外,该模型检查器 SPIN 的输入语言 Promela 专注于关于描述并发,所以从这个想法开始,我们将这些因素构建到几个并发进程中符合 SPIN 的检查,它也将准确地描述系统。为了方便描述,它们将是称为并发实体。 PLC控制器与并发实体通过图像表中的符号。

PLC系统的符号包括I(输入端口)、Q(输出端口)和M(中间继电器)。图1是一个PLC系统模型图。时间间隔建模策略:使用标志哪个特定并发实体的位状态代表状态中的并发实体,没有关于系统时钟。这可能会忽略时间状态的差异,从而简化了 PLC 模型。

建模策略不加系统时钟属性,与原PLC不完全对应模型。那主要是因为加入系统时钟会导致PLC系统模型过大,没有对于模型检查工具来处理这么大模型。对状态建模的起点这是不考虑 PLC 扫描的次数,当经历过迁移。不管扫描多少次经验丰富的,他们都将包括在这个模型中。在换句话说,真实模型将是构建的子集模型(时间间隔模型)。真实的 PLC 环境是复杂的,包括一个

各种硬件和人类行为。以下

我们将对不同种类的PLC环境并发实体进行分析。

1) 硬件实体

PLC系统的硬件实体主要是一些PLC控制的设备。这些设备的状态可以作为PLC控制器的输入。因此,硬件实体与其关联的 I 和 Q 绑定,而硬件有自己的工作流程,这个工作流程是由硬件要求决定的。这个工作流程可以抽象成自动机。该自动机用于描述硬件的工作状态。定义 2.1。硬件实体是一个元组 Env =,其中 Ienv 是与硬件绑定的 I 端口entity,Qenv是与实体绑定的Q端口。 A 是描述实体工作流程的自动机,A 是元组 A =,其中 s0 是 A 的初始状态,S 是状态集合,而 T 是转移集合。硬件实体的状态是 I 符号的子集,并且每个状态的 Is 符号都映射到 {True, False},I符号不出现的状态可以是True或 False(即:任意行事)。硬件实体的转移直接用 Q 的子集表示符号,表示子集中的所有 Q 符号在同时将推动国家之间的迁移。这硬件实体的状态转移图也需要指定初始状态,转换图从这种状态。

硬件实体的状态转移图是基于符号 I 的划分,时间属性为不考虑。硬件实体状态转换图实际上是硬件实体的抽象被忽略时间,抽象的模拟需要参考的硬件。

2)简单的输出实体仅与 Q 端口绑定的简单输出实体不使用 I 端口,这意味着简单的输出实体没有状态转换图。简单的输出entity是显示PLC工作状态的设备,就像号灯一样。简单输出实体的用法是与 Q 端口绑定,以便 PLC 可以使其逻辑设计。

3) 人类行为实体定义 2.2。人类行为实体是一个元组 Env= < Ienv, A>,其中 Ienv 是 I 端口与硬件实体,Qenv是与实体绑定的Q端口。 A 是描述工作流程的自动机实体,A 是一个元组 A =,其中 s0 是初始A 的状态,S 是状态的集合,T 是状态的集合转移。

人类行为实体与硬件实体类似;它们具有相同的状态定义。很难模拟人的行为,尤其是设计一个PLC涉及到一些个人。作为回应这些困难,人类行为建模应该采取一个迭代过程:首先,一个简单的行为模型是建立使用模型验证;那么,如果没有找到柜台例如,构建并验证更复杂的模型,

直到找到反例或难以更复杂;最后,如果之前没有找到有意义的反例,则生成一个完全随机的人的行为模型(即:人的行为是一个完整的图

所有转移都是真实的)以进行验证。但是,完全随机行为的验证会导致状态空间急剧增加,那么如何选择合适的人类行为模型是建模的难点。如果人的输入比较简单,我们可以使用完全随机的行为建模,否则,你需要认真考虑建立合理模型的人类行为。

我们对PLC环境和人建立模型上面的行为,然后我们将对 PLC 控制器进行建模。 PLC控制器在转动时会处于一个循环中上。

 PLC 从 I 端口读取所有输入。

 PLC 计算所有逻辑单元。

 PLC 设置所有 Q 端口。

PLC进程上的基本单元称为网络。所有网络将按照编号顺序运行设计时设置。

PLC控制器的基本逻辑运算网络包括:S触发器、R触发器、SR触发器、EQ触发器、RS触发器,POS上升沿检测器,NEG下降沿探测器等。对基本逻辑运算网络建模,我们采用直接映射策略,即:PLC控制器模型的网络行为和网络的逻辑行为是完全等价的。哪里触发器, R 触发器, SR 触发器, EQ 触发器, RS 触发器可以直接使用布尔表达式映射到它们的行为。


友情链接