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

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

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

3) 人类行为实体

定义 2.2。人类行为实体是一个元组 Env= < Ienv, A>,其中 Ienv 是 I 端口与硬件实体,Qenv是与实体绑定的Q端口。 A 是描述工作流程的自动机实体,A 是一个元组 A = <s0, S, T>,其中 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 触发器可以直接使用布尔表达式映射到它们的行为。

RTU

三、PLC模型的分析与改进

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

首先,为了找出系统中的所有错误,我们应该建立一个足够大的模型来覆盖所有的州原始系统;二、要求模型接近尽可能真实的系统。这不仅会减少状态空间,也提高效率。根据关于需求,我们将进行分析时间间隔模型。命题 1 如果时间间隔模型符合属性,真实的PLC系统模型也符合。可以得出命题1的正确性从两个模型之间的关系来看。那表示真实模型将发生的所有情况都是包含在时间区间模型、时间区间模型中比真实模型大。如果你找不到一个通过使用时间间隔模型的反例,您可以证明真实PLC模型的正确性;另一个手,如果我们找到反例,我们无法确定真实的PLC系统是否有错误。那就是说命题1的逆命题是错误的。然后手动需要干预来分析反案例以确定它是否是伪错误。时间间隔建模策略可以得到一个摘要PLC 模型,许多基于 NuSMV 的研究也使用类似于时间间隔模型的策略来对 PLC 系统进行建模。但“时间区间模型”与真实模型存在较大偏差,需要改进。这偏差是:“时间间隔模型”没有反映PLC的高速扫描特性和低速扫描特性并发实体的特征。也就是说,所有环境的变化应该被扫描

高速PLC,但时间间隔模型忽略了PLC的高速特性,从而改变在外部环境中可能无法被扫描。针对上述问题,考虑到外部高速扫描和低速并发

物理特性、时间间隔建模策略将通过增加通知等待机制来改进。基于时间间隔模型,每个并发状态实体必须被阻止并在传输完成后等待地方。仅当 PLC 控制器至少完全扫描一次,通知等待机制将向并发实体发送消息以移除块并继续工作。然后传输完成。并发实体通过无时间等待机制完成迁移的过程如图2所示:

这种机制确保了 PLC 控制器至少可以扫描一次并发实体的每个状态变化。命题 2 添加通知等待机制后,该模型成为时间间隔模型的子集。在同时,模型还可以包含真实模型中的全部情况。也就是说,如果一个模型添加通知等待机制符合属性,真实PLC系统模型也符合。

用命题 1 证明命题 2 类似。通过命题2我们可以看到,在添加通知等待之后机制模型仍然具有良好的性质。如前所述,抽象系统模型有两个要求:首先,要完全包含真实系统,其次是模型尽可能接近真实系统。首先命题证明时间区间模型包括真实系统,只要使用模型检查工具以证明该抽象模型满足某些属性,那么系统的真实性质将也满足这一点。但是这个模型和真正的模型不是完全相等,应该远远大于真实模型。

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

同时,通过通知等待机制,

模型变得更接近真实系统,不仅降低了时间复杂度,同时也减少了前面提到的pseu do-errors。


友情链接