英语原文共 7 页，剩余内容已隐藏，支付完成后下载完整资料
大型plc程序时序方面的建模与形式验证
摘要：防止模型检查被广泛应用于工业控制系统的主要障碍之一是PLC程序中建立形式模型的复杂性，特别是在需要集成时序方面的时候。本文提出了一种方法来解决这个障碍，以建立和验证PLC程序的时序方面的方法。提出了两种方法，允许用户平衡模型复杂度之间的权衡，即其状态数和可验证的规范集。开发了一种工具，支持直接从PLC程序生成不同型号跳棋的模型。现实生活中的PLC程序定时方面验证本文提出的基于NuSMV。
关键词：PLC，计时器，形式的验证，模型检测的抽象自动机，
1引言
欧洲核子研究组织（CERN）依靠大量的PLC（可编程控制器）来操作不同的粒子加速器。这些应用程序对CERN操作至关重要，因此保证其行为符合规范是最重要的。形式验证，特别是模型检查，似乎是一种很有前途的技术，以确保PLC程序符合初始规范。然而，由于构建PLC程序的形式模型的复杂性，这种技术并没有广泛应用于工业中：构建这种形式化模型需要深入了解系统对模型（硬件和软件）以及底层模型检查器的深入了解。此外，在定时方面需要考虑，即PLC时间和定时器，模式化的任务变得更加复杂的模型，没有一个精确的表示，通常太大的状态空间是由模型检查处理。
在本文中，我们提出了一种建模plc时间和定时器的方法。该方法集成到在达瓦斯等人描述的通用框架。（2013）允许从PLC程序自动生成正式模型。提出了以时序方面的考虑有两种途径：现实与抽象模型化。现实的方法代表计时器的行为和高保真的PLCs时间的内部表现。这种建模允许验证与时间相关的属性，以确保给定的动作将（或不会）在给定延迟后执行（例如在给定输入设置为真之后，PLC输出设置为真500毫秒）。而这种模式化是从表现力强大，它可以产生模型过大被模型检查器，从而处理，导致第二建模方法。抽象方法忽略了时间本身的建模并给出了定时器的非确定性模型。与第一种方法相比，这一方法大大减少了生成模型的状态空间，因此可以验证大型PLC程序，同时还能够验证一些与时间相关的规范。可以通过采用本次建模验证的性质例如活性（如PLC的输出将被设置为真后输入设置为false）。要求验证使用抽象的时间建模仍然有效的现实模型，为现实的办法是重新抽象的一个问题。最后，一个工具，实现两种时间建模和生成的正式型号为NuSMV（西马蒂等人。（2002）），BIP（巴苏等人。（2011））和工具（阿内尔等人。（2001）已经开发并应用于欧洲核子研究中心的控制系统。
1.1相关工作
虽然时序行为建模的PLC程序以前的研究文献中，他们没有提供一个通用的方法，可以自动地生成正式的模型包括时间方面，并对这些模型进行验证的同时。此外，在文献中发现的所有方法都局限于一个特定的模型检查器，从而防止利用不同类型的模型检查器。
事实上，马德和福（1999）或佩林和福雷（2013）提出了一种模拟PLC定时器使用时间自动 机模型的方法，但不存在版本化的结果。由于时间被认为是一个线性和单调函数，生成的模型将有一个巨大的状态空间，如果在欧洲核子研究中心开发的系统将这种方法应用于大型系统，就不可能进行验证。同样，mokadem等人。（2010）提出了一个案例研究，其中建立了一个定时多任务PLC程序的全局模型，用于验证姿态。这种方法类似于一个由马德和福提出（1999）但验证是使用时钟，因此单调UPPAAL时间表示。在王等人。（2013）、PLC控制系统包括定时器等几个方面进行建模，采用基于组件的BIP框架。在这种情况下，他们假设固定的PLC周期长度是一个大的应变，定时器模型不够精确，与实际的PLC定时器相比。此外，没有给出验证结果。
论文的其余部分结构如下：第2节介绍了时间和计时器在PLCs的概念。SEC 3给出了所提出的方法的概述，该方法允许用PLC程序生成各种模型检查器的正式模型。4部分详细介绍了本文提出的两种方式，PLC程序的时序模型方面，随着应用现代elization案例研究。此外，这一部分展示了一个现实的时间正式建模是一个完善的抽象。最后，第5节分析了这两种方法的优缺点，并对论文进行了总结。
2、定时plc控制系统
本节概述PLC控制系统，着重于时序方面。此外，案例研究，将在剩余的部分用来说明本文提出的模型化方法。
plc的定时行为
PLC是一种工业计算机执行一个SYN -异步的循环扫描周期的过程，包括以下主要步骤： （1）阅读输入值的记忆，（2）解释和使用读取的数据执行程序逻辑，最后（3）写作计算输出值房输出。
在标准的PLC，即非安全PLC中，循环时间不是固定的，但是有一个上限由一个看门狗模块强制执行。如果PLC的循环时间大于这个上限，例如由于PLC程序中的无限循环，PLC执行程序的一个特殊部分负责处理定时误差。相比之下，安全PLC有固定的循环时间。
定时操作，如计时器，是由IEC 61131定义的，可以看作是一个功能块，用于延迟信号或产生脉冲。不同类型
计时器可以在PLCs找到，最常见的计时器之一是吨（定时器延迟）（参见图1）。这个定时器有2个输入变量：输入和输出。在一个布尔输入信号中，PT是延迟时间。定时器有2个输出：q和q。q是布尔输出变量，当执行上升沿时，它的值将是正确的。ET是经过的时间，它的值被增加到PT，开始时出现一个上升沿。
1
IN
输入
PT
0
1
Q
输出
0
PT
ET
历时
0
图1。TON时间图
PLC定时器使用特定的数据类型进行定时操作，称为时间。这种数据类型由IEC 61131定义为一个有限变量，它表示“这些数据类型中的表示值的范围和精度是依赖于实现的”。代表由有限变时产生非单调的时间表示为变量可以溢出（参见图3的上半部分）。例如，在西门子S7系列PLC，时间数据类型定义为一个有符号的32位整型和1毫秒的精度相同（见西门子（1998）），有大约24天的上限和下限的24天。然而，在Schneider和Beckhoff PLCs，时间数据类型在本文中一个32位无符号整数用1精度的女士，我们考虑签署时间解释为西门子PLC的定义。
案例研究
在本文的背景下，工业控制系统的系统框架，开发和使用由欧洲核子研究中心，被称为与（布兰科等人。（2011）作为个案研究。与提供一种较常见的工业控制仪器仪表的基础对象库（如传感器、执行器、子系统）。这些对象被表示为PLC代码中的功能块，使用ST（结构化文本）语言，它可以在PLC上调用不同的函数、函数块。目前与实施标准的PLC，即周期时间是不固定的，取决于整体的应用。
在本文中，我们专注于通过西门子PLC与图书馆提供的对象。此对象用于表示物理设备，如由数字信号驱动的致动器（例如阀门、加热器、马达）。60个输入变量（13参数），62个输出变量，600行的ST代码，和3定时器的开关情况下，对象的规模和复杂性方面与其他对象代表。
3、plc程序建模
本节给出了一般方法的简要概述模拟PLC程序不考虑时序方面学。更多详情，读者可参阅瓦斯等。(2013). 此外，还介绍了应用的约简和抽象。
方法论
此方法旨在从st代码生成正式模型。它提供了一个中间模型和一组转换规则，用于从控制系统的“非正规世界”中生成不同验证工具的输入模型（参见图2）。这个“非正规世界”基本上是由与执行平台相关的ST程序和环境因素组成的（例如PLC扫描周期）。
图2。从st代码生成正式模型的通用方法学概述。
这种基于自动机的中间模型简化了模型检查器所使用的任何形式化模型的转换规则，该模型的建模语言与基于自动机的形式化方法接近。它允许很容易地将新的模型检查器添加到方法中，并用不同的验证工具验证同一模型，从而从验证性能、模拟和性能描述的表现力中受益于验证工具的不同优势。
我们的基于自动机的形式化是足够强大的模型的PLC控制系统的所有相关功能。书的中间模型的抽搐是类似的时间自动机的形式主义在Behrmann等人定义的网络。（2004）但没有明确的逻辑时钟表示。此外，自动生成工具已经开发支持这种方法，可以生成模型NuSMV，UPPAAL和BIP的ST代码。
简化提取技术
为验证目的建模PLC程序意味着创建具有巨大状态空间的模型，因为它适用于任何其他真实的软件。如果这些是定时系统，则需要建模时间，因此问题变得更大。虽然本文的主要目的不是详细介绍在生成的模型上应用的抽象技术，但我们需要介绍它们，以了解我们在定时PLC程序上的实验结果。这些技术包含在方法中，并自动应用到中间模型，因此所有生成的最终模型都受益于它们。应用的主要抽象和归约技术：
利用PLC的执行模型的特点，采用基于规则的简化方法简化生成的自动机。例如，如果没有相互影响，就可以合并在后续转换中的变量赋值，因为在执行PLC循环期间，变量的值没有被检查，但只有在结束时。已经定义了超过20条规则来简化和减少模型。
当性能验证提供，我们将影响锥（COI）减少（参见克拉克等人。（1999）），它包括删除不影响属性的所有变量。由于它取决于被检查的需求，它对状态空间大小的影响非常不同，但是对于许多例子，我们可以观察到一个大的状态空间缩减。
在某些情况下，谓词抽象也可以应用到PLC应用程序中。它由布尔值函数代替非布尔变量。
读者在瓦斯等应用技术的详细信息。（2014）。
4、PLC程序时序建模
本节重点介绍PLC时间和计时器的建模方面，扩展了第3节中所描述的方法。吨计时器，在第2节，是用来说明两个拟议的方法，以模型时序方面，但同样的方法可以应用到任何其他PLC定时器块。在所提出的方法扩展中，PLC定时器由一个分离的自动机表示，该自动机与主程序同步。建模PLC定时器也意味着对时间数据类型进行建模。然而，正如前面提到的，计时模型通常包含一个巨大的状态空间，这不能由模型检查器来处理。基于这一观察，本节提出了两种不同的方法。第一种是逼真的计时器表示，它接近现实，能够进行精确的建模和验证。第二种方法提出了一种抽象的时间表示，它不太准确，但极大地减少了模型的状态空间。
分析了这两种方法对时间和定时器表示、属性说明和实验结果的关注。此外，我们还证明了抽象方法模拟现实的方法，从而保证抽象方法验证的任何属性在现实中也能保持，即使是简单得多。
现实的方法
第一种方法提出了一个现实的TON计时器和时间处理模型。这种方法允许指定具有显式时间的属性。有这种现实的计时器代表意味着时间也需要现实地建模。
时间表征的三个主要特征方面认为这种方法模型的时间：
（1）时间为ftnite变量：它代表高保真PLC中的时间数据类型。然而，使用16位变量来表示此数据类型，而不是有符号的32位整数变量（如西门子PLC）。这种范围的减少是可能的，因为PLC的行为是循环的，循环时间、定时器的延迟和需求的延迟要比这个16位变量的范围小得多。这个变量的精度是1毫秒，就像在真实的PLC中一样。由于这种时间表示，在建模计时器时必须考虑时间溢出，也需要表示要检查的需求（例如，当前时间可以较小，用于以后的事件，参见图3）。
（2）时间的递增增加周期时间：这表示，时间不加说明个人单位时间。相反，它是在最后一个PLC周期结束时递增的。这种假设明显简化了全局模型，与PLC中的实际实现相比，没有任何损失的准确性，考虑到在每个PLC周期中，定时器最多被调用一次，它适用于我们的实际情况。
（3）周期时间选择的不确定性：为了表示标准的PLC具有不同的时间周期，一个随机值是在每个周期结束时产生的代表。所选的随机值在5毫秒到100毫秒之间，这是基于欧洲核子研究中心的PLC系统的有效假设。
C
当前时间
0
最小时间
最大时间
tm
tm
开始时间＜停止时间
图3。有限时间表示的后果
计时器表示给出有限时间代表性，定时器的行为表明它是在ST代码所示（见图4）。在这段代码中，输入变量和输出变量的PT，和Q等变量CTime表示当前时间和它是仿照以前解释。此外，增加了两个变量：运行和启动，在运行是一个布尔变量表示当定时器工作在上升沿上并开始包含CTime价值时有一个上升沿。
通过应用扩展的方法，生成了相应的吨st代码自动机，并在图5中示出了等效状态机。（注意，从状态机中省略了ET的分配，以简化数字）。这个状态机包含3个状态，对应于3个原始状态的吨：NR（不运行；运行= FALSE，Q = FALSE），R（运行；运行= TRUE，Q = FALSE）和（超时；运行= TRUE，Q = TRUE）。状态机中的转换（标记为T1、T2、T3、T4）对应于ST代码中的条件语句。
IF in = false THEN
Q := false; ET := 0;
running := false; // t1 ELSIF running = false THEN
start := CTIME;
running := true; // t2 ELSIF CTIME - (start PT) gt;= 0 THEN
Q := true; ET := PT; // t3 ELSE
IF not Q THEN ET
剩余内容已隐藏，支付完成后下载完整资料
资料编号：[478583]，资料为PDF文档或Word文档，PDF文档可免费转换为Word
以上是毕业论文外文翻译，课题毕业论文、任务书、文献综述、开题报告、程序设计、图纸设计等资料可联系客服协助查找。
