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

基于形式的PLC建模与校验方法(中)

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

三、PLC模型的分析与改进

上一节介绍了 PLC 的建模系统,根据这个策略;我们可以将 PLC 系统抽象为模型检查的正式模型。所以,这个模型的可信度将直接决定模型检查结果。如果模型不完全覆盖原系统(我们称之为小于原系统),可能会导致一些错误未被检测到;如果真实系统可以完全覆盖模型,但它包含许多原始系统没有的状态存在(我们称它比原始系统大),这可能引入一些真实系统不存在的错误。这里称之为伪错误。所以有两个要求建模策略。

首先,为了找出系统中的所有错误,我们应该建立一个足够大的模型来覆盖所有的州原始系统;二、要求模型接近尽可能真实的系统。这不仅会减少状态空间,也提高效率。根据关于需求,我们将进行分析时间间隔模型。命题 1 如果时间间隔模型符合属性,真实的PLC系统模型也符合。可以得出命题1的正确性从两个模型之间的关系来看。那表示真实模型将发生的所有情况都是包含在时间区间模型、时间区间模型中比真实模型大。如果你找不到一个通过使用时间间隔模型的反例,您可以证明真实PLC模型的正确性;另一个手,如果我们找到反例,我们无法确定真实的PLC系统是否有错误。那就是说命题1的逆命题是错误的。然后手动需要介入分析反例以确定是否为伪错误。

时间间隔建模策略可以得到一个摘要PLC 模型,许多基于 NuSMV 的研究也使用类似于时间间隔模型的策略来模拟 PLC 系统。但“时间区间模型”与真实模型存在较大偏差,有待改进。这偏差是:“时间间隔模型”没有反映PLC的高速扫描特性和低速扫描特性并发实体的特征。也就是说,所有环境的变化应该被扫描高速PLC,但时间间隔模型忽略了PLC的高速特性,从而改变在外部环境中可能无法被扫描。针对上述问题,考虑到外部高速扫描和低速并发物理特性、时间间隔建模策略将通过增加通知等待机制来改进。基于时间间隔模型,每个并发状态实体必须被阻止并在传输完成后等待地方。仅当 PLC 控制器至少完全扫描一次,通知等待机制将向

并发实体删除块并继续工作。然后传输完成。并发实体通过通知等待机制完成迁移的过程如图2所示:

 t0:传输启动、阻塞和通知 PLC 控制器。

 t1-tm:PLC 完全扫描 m 次(m 在

至少)。

 tm+1:并发实体收到通知PLC,传输完成。

RTU

这种机制确保并发实体的每个状态变化都可以被 PLC 控制器至少扫描一次。命题 2 添加通知等待机制后,该模型成为时间间隔模型的子集。在

同时,模型还可以包含真实模型中的全部情况。也就是说,如果一个模型添加通知等待机制符合属性,真实PLC系统模型也符合。用命题 1 证明命题 2 类似。通过命题2我们可以看到,在添加通知等待之后机制模型仍然具有良好的性质。如前所述,抽象系统模型有两个要求:首先,要完全包含真实系统,其次是模型尽可能接近真实系统。首先命题证明时间区间模型包括真实系统,只要使用模型检查工具以证明该抽象模型满足某些属性,那么系统的真实性质将也满足这一点。但是这个模型和真正的模型不是完全相等,应该远远大于真实模型。与时间间隔模型相比,该模型进一步缩小了真实系统之间的距离,大大降低了发现伪错误的机会。

模型检查工具将给出一个反例侵犯系统的财产;手动很容易确定真实系统中的反例为真或不。如果原系统的错误真的存在,然后我们找到一个反例。否则,这个错误是因为抽象模型比真实系统大,这是一个伪错误。 因此,虽然这个时间间隔模型与原系统不完全等价,但是通过这个模型,我们可以判断一个系统是否满足某个属性,如果没有我们可以找到一个具体的反例(仍然需要更多检查以确定它是否是伪错误)。模型与原系统不等价,主要是因为有很多因素难以建模在实际系统中,其中一些可能会导致错误。 如果所有的因素都被建模了,这将导致建立一个无法检查的巨大模型,或者干脆无法实现。 时间间隔模型抽象关键来自真实系统的因素并对其进行建模,极大地减少状态空间,降低时间复杂度。同时,通过通知等待机制,模型变得更接近真实系统,不仅降低了时间复杂度,同时也减少了前面提到的伪错误。

在上述建立的模型上实现了 NuSMV)检查。我们制定了一系列的转换规则,将上述模型构建成SPIN的输入语言Promela,系统属性也需要翻译成Promela,SPIN 将它们放在一起然后执行检测。PROMELA 语言是 C 类语言,它们是语义相似。所以我们只举一些例子显示翻译的基本概念。要查看PROMELA 语言的详细信息,请访问 www.spinroot.com。我们将介绍 PROMELA 文件的三个部分作为 SPIN 的输入。

1)PLC控制器代码

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

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

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

PLC网络的方法。


友情链接