英语原文共 9 页，剩余内容已隐藏，支付完成后下载完整资料
可编程逻辑控制器的正式建模与合成
摘要
可编程逻辑控制器（PLC）是复杂的网络物理系统，在工业中得到了广泛的应用。本文提出了一种设计和实现基于PLC的嵌入式系统的可靠方法。时分自动机用于对控制器及其环境进行建模。我们采用模型检查技术验证设计模型。提出了一种从时位自动机生成PLC代码的算法，并采用原型工具实现该算法。该方法可以浓缩开发过程，保证PLC程序的正确性。案例研究演示了该方法的有效性。
关键词；PLC;正式规范;代码合成;嵌入式软件
简介
可编程逻辑控制器 （PLC） 广泛应用于工业中的安全关键嵌入式系统。传统的PLC软件开发过程由需求分析、软硬件设计、软件编程和测试组成。PLC 测试花费大量的时间和金钱。程序应下载到 PLC。然后连接所有物理工厂并进行系统测试。致命错误通常是由脆弱多变的环境和程序中的逻辑错误引起的。由于系统复杂性的迅速增加、上市时间的缩短以及对实时系统的需求不断增长，正式方法在补充传统测试方法方面变得不可或缺。
提出了一种可靠的PLC系统建模和合成设计方法。本文主要研究从高级抽象模型自动生成代码。由于PLC系统是实时交互系统，我们选择时位自动机作为设计模型。控制器和物理环境由定时自动机建模。设计模型经过验证，通过采用符号模型检查器 Uppaal[1-3]实现，以满足所需的安全和功能要求。模型得到改进，直到满足所有相关属性。这意味着设计模型在所有情况下都运行正常。我们在[4]中介绍了此设计过程。提出了一种将设计模型传输到可执行PLC代码的算法。该算法已在原型工具中实现。自动生成代码可以减少测试的依赖性。该方法可以发现早期控制器的错误，简化开发过程。案例研究说明了拟议的战略。
几种正式技术用于建模和分析基于PLC的嵌入式系统。在[5,6] Sacha 使用有限状态时间机器 （FSTM） 来模拟 PLC 系统并自动生成代码，这是摩尔自动机具有时间特性的扩展。但是，FSTM 不支持验证工具，我们不知道设计模型是否正确。因此，必须将 FSTM 模型转换为 Uppaal 的定时自动机以进行验证[7]。弗雷为PLC开发了一个信号解释Petri网络（SIPN）编辑器。此工具可以从 SIPN 型号 [8] 生成 PLC 代码。时间的概念通过时间到 SIPN 中引入。每个时间点都与最小时间常量相关联，这是令牌在其中必须花费的时间跨度。与时位自动机相比，这种时间延长的表达力较差。在[9]中，Pollmacher 侧重于证明从时间自动机到 ST（结构化文本）语言的翻译的正确性。ST是一种高水平的程序语言，而我们的目标语言是低层次的，以中继为基础，所以翻译方法不同。他从生成的代码中提取了正确的模型，并检查此模型是否是设计模型的改进。
论文的组织如下。第 2 节显示了有关 PLC 和时位自动机的背景。第 3 节介绍正式规范和代码生成。示例用于显示设计方法。第4节结束论文。
2. 背景
2.1.PLC 计划
PLC 同时控制多个物理工厂。它接收来自传感器的信号，并循环向执行器发出控制命令。在扫描周期开始时，传感器的值写入输入内存区域。然后执行PLC程序，并将输出值写回内存。在扫描周期结束时，输出存储器映射到执行器。PLC嵌入式软件系统不同于传统软件。它处理物理环境交互的控制信号，而不是数据计算。
国际电工委员会 （IEC） 发布了可编程逻辑控制器的 IEC61131 标准 [10]。五种程序语言由 IEC 定义。它们是指令列表 （IL）、梯形图 （LD）、结构化文本 （ST）、函数框图 （FBD） 和顺序函数图 （SFC）。在工业中应用最广泛的LD是一种像语言一样的中继图。我们选择西门子PLC [11] 中使用的 S7-300 LD 计划语言作为我们的目标语言。
LD程序由逻辑网络的图形组件组成。一次只执行一个从左到右，然后从上到下执行一个网络。LD 程序模拟电流通过一系列逻辑输入条件并启用输出条件。LD 程序包括左侧通电的电源轨。触点表示逻辑输入条件，如开关、按钮或传感器。闭合触点允许能量通过它们流向下一个元素。通常打开触点 （-||-） 当存储在此触点上方的位值等于 1 时关闭。然后，梯形导轨动力流过触点。对于常闭触点（-|/|-），它是反的。输出线圈 -（） 是逻辑输出结果或中间结果。如果线圈有动力流，则上述位设置为 1。
如果功率流向它，则执行复位线圈 -（R）。位的地址重置为 0。该地址也可以是计时器。此操作会将时间值重置为 0。对于设置线圈 -（S），它是相反的。这两个指令一起形成一盒 S-R 触发器，参见图 1。框用于其他指令，如计时器、整数数学指令、比较指令和移动指令。
比较指令还是可用作正常触点。符号'？'可以是 ==，gt;=，lt;=，gt;，lt;，和lt;gt;。比较结果链接到整个运行的 RLO（逻辑结果）。图 2 显示了 LD 说明。IN1 和 IN2 可以是 L、Q、I、M、D 内存区域或常量的数据。仅当满足框输入条件时，才会执行指令。
图1 RS和SR说明
图2 比较说明
图3 整数数学说明。
2.2. 时分自动机
时分时自动机 [12，13] 是有限自动机，具有实时系统的时间变量扩展。在这里，我们使用 [14] 中定义的定时自动机的变体。让 成为一组有限的变量，包括时钟变量和数据变量 和 。所有时钟变量同时前进。我们使用 表示不变公式和保护公式。我们有, 采取的形式，如 或 和 。赋值运值操作定义为 让 表示所有赋值公式。
定义 1。时时自动化是一个元组
: 有限的位置集合
:初始位置
：有限的动作集合
:有限的变量集合
:位置约束函数
: 一组有限的边
每个边都有一个源位置，一个目标位置 。当满足保护 时，会发生转换，并且 中的变量子集通过公式 更新。边缘可以写成
自动机从初始位置 开始，所有时钟都初始化为 0。随着时间的推移，时钟变量以满足不变约束)的相同速率增加。如果变量满足边缘启用保护 ，则系统可以保持在此位置或传输至 。转换后，将执行操作 ，并通过公式 更新变量。
定义 2。定时自动化的语义被定义为一个带标签的转换系统。是一组状态,是初始状态，是一组关系，分为以下两类。
时间变化:对于，,如果,和rsquo;满足
位置变换：，如果,则满足保护，并且满足。
实时系统由多个部分组成，控制器与环境中的物理环境并发通信。所以我们使用时间自动机网络和,n是网络中的自动机数。这些自动机共享一组通用的操作变量。向量是时间自动机网络的位置向量。不变函数是所有的约束条件的结合点，表示的被代替。
定义 3。定时自动机网络的语义定义为过渡系统, 是状态集, 是初始状态，并且 是定义如下的转换关系：
bull;, 对于, 如果, u和 满足 ,
bull;, 如果有边缘 ,， 满足保护 和满足。
bull;, 如果有退出边缘和另一个边缘,则满足保护，满足。是同步信号，表示接收信号 并且 表示发送信号 。
通过通道发送和接收信号，同步不同时分自动机的转换。
3. 正式规范和代码合成
我们使用一个示例来说明我们的迭代方法。
3.1. 例如：双门控制器
需要保护特殊房间免受灰尘的侵害。因此，房间的入口配有双门。这两扇门不能同时打开。此控制系统的详细信息如图 4 所示。门内外都有按钮。按钮 1 和内部按钮 3 可以打开门 1。门 1 上有一个光电传感器。如果一个人站在门 1 内并挡住光电传感器 1，则第一个门可以自动打开或保持打开。门完全打开后 3 s，门 1 自动关闭。关闭时，如果一个人按下按钮 1 或按钮 3 或站在光电传感器 1 附近，则门 1 将再次打开。门 1 完全关闭后，门 2 将自动打开。每个门有两个行驶开关，用于检测车门是完全打开还是完全关闭。双门控制系统应持有的最重要属性是两个门不能同时打开
图4 双门的架构
图5显示了PLC控制系统的结构。它由五个部分组成，它们是PLC控制器、人、传感器、门1和门2。个人可以按门 1 或门 2 外的按钮 1 或按钮 3。PLC 在输入扫描周期中捕获相应的信号 Button1 或 Button3。经过一些逻辑计算后，打开门 1 命令 OpenDoor1 或打开门 2 命令 OpenDoor2 由 PLC 发送到门。当门打开时，人们可以进入。开仓将持续 3 s，然后自动关闭。光电传感器可以检测一个人是否靠近门。如果人们已经离开了门，传感器1和传感器1的布尔值仍然是正确的。另一扇门将自动打开。开口还保留 3 s，然后关闭。当门打开时，人们不允许按任何按钮。第一次进入门 2 和门时情况相同
图5 双门控制器的结构
3.2. 正式建模和验证
控制器及其环境由时位自动机建模。在定时自动机网络中，定义了十二个信号。它们是按钮1，按钮2，按钮3，按钮4，门1关闭，门1打开，门2关闭门2打开，关闭门1，打开门1，打开门1，打开门2和关闭门2。一个信号由两个部分共享，用于同步。
图 6 显示了门的模型。显示门的状态， 表示门已关闭。一开始，门是关着的。一旦收到 OpenDoor1 命令，它就开始打开。完全打开时，行驶开关知道它，并将门 1 打开发送到 PLC。模型将移动到打开状态。如果它从 PLC 收到 CloseDoor1，门将关闭。当行驶开关抓住门完成关闭时，它会发送门1关闭并将 设置为 1。门 2 也是如此。
图6 门模型
图7是模拟人们行为的自动机。它应包含所有可能的情况。传感器的模型太简单了，我们用人模型来压缩它。人们可以进入房间或走出房间。左侧首先进入门 1，然后进入门 2。右侧的序列相反。一个人按下按钮1，进入第一扇门。自动机移动到位置。跟踪 意味着在人员进入第一个门后，他不穿过第二扇门，而是按下按钮3 然后出去。传感器1是光电传感器1的值。最初，感应器 1 为 1。当一个人站在传感器附近并阻挡光线时，b1 变为 0。因此，位置 意味着有人进入门 1，站在光电传感器之间。 和 是门自动机中定义的变量。 表示门 1 已关闭。
图7 人的行为模型
PLC 控制器的自动机如图 8 所示。初始位置为 M0。如果按下按钮 1 或按钮 3，它将传输到 。 和 是相互排除变量。然后，控制器将打开门命令 OpenDoor1 发送到门 1，同时，将 计算为 0。这意味着无法打开门 2。一旦收到打开的完整信号门1打开，控制器启动一个计时器，并转到位置。t 是本地时钟变量。位置 具有约束 。当时间流逝时，如果 和，它会传输到位置 并发出 CloseDoor1 命令。以下跟踪显示了打开门 1 的过程
虽然在位置 ，有很多选择。因为一个人可以穿过2号门，或者回到1号门。按下按钮1或按钮3或块光电传感器传感器1将导致门1再次打开。当控制器收到门1关闭时，它将打开门2或返回初始位置，具体取决于MuEx1的值。 表示门 1 已完成打开，门 2 将自动打开。跟踪
是打开门 2 的控制过程。因为 在过渡中已设置为 0 ，自动机返回初始位置 。这是先打开门 1，然后是门 2 的整个过程。另一个跟踪
处理从门 2 到门 1 从房间出来。
根据控制系统要求指定以下属性。由 验证，在具有 PM 750 1.86 GHz CPU 的计算机上运行，内存为 1.2 GB。
P1：系统应无死锁。
P2：门 1 和门 2 不能同时打开
控制模型满足上述所有属性。
图8 双门控制器型号
3.3. 代码合成
我们假设包括。翻译方法如下：
-
每个PLC程序都有一个符号表，它是关于设计模型中的符号关系和PLC硬件的绝对地址。首先，我们应该将PLC内存中的数据传输到有时自动机中的变量。PLC 的输入信号对应于输入点 I0.0、I0.1。在我们的示例中，按钮 1、按钮 2、按钮 3、按钮 4、门1 关闭、门1打开、门2关闭、门1打开、传感器1和传感器2分别分配给 I0.0、I0.1。PLC 的输出信号映射到输出点 Q0.1、Q0.2。位内存区域（ 内存）始终用作控制继电器，以存储操作的中间状态。它们可以通过位、字节、单词或双字进行访问。此处的位置分配给0.0，0.1。PLC 内存。当自动机到达某个位置时，此位置变量设置为 1。当自动机离开此位置时，变量将重置为 0。我们应该区分当前位置和下一个位置。所有新分配的位置都是下一个位置。我们使用 来呈现位置 的下一个值。为了简洁的程序，我们使用触发器来描述位置。另一个内存区域 存储操作的中间结果。因此，可以将整
剩余内容已隐藏，支付完成后下载完整资料
资料编号：[237743]，资料为PDF文档或Word文档，PDF文档可免费转换为Word
以上是毕业论文外文翻译，课题毕业论文、任务书、文献综述、开题报告、程序设计、图纸设计等资料可联系客服协助查找。
