外文科技文献译文自动化的逻辑控制机械在化工过程工业系统设计中的实现Jinkyung Kim, Il Moon*化学与生物分子工程学部，Yonsei大学，134 Shinchondong Seodaemoonku ，首尔 120-749, 韩国摘要 自动化模型检查被用来决定SIS（安全器具系统）的无错误设计而且用于查找化工过程逻辑的错误。它拥有自动化的技术提供而且修正SIS控制逻辑的PID。这一个方法能被申请查证SIS的正确性而且通过自动综合能实行的序列找合乎逻辑错误。这个研究致力于化工过程SIS控制逻辑中的自动修改和综合设计、可操作性和便利性。1.介绍过程机械设计者开始系统设计的工作自动地减少了危险，这种危险是危险分析家所指出的减少多少危险符合公司和管制的目标所需。在考虑过程设计的改变和继承安全的选择之后，许多工程师开始安全的设计器具系统（SIS）的设计, 一个自动的系统保护人员、环境和公司资产免于过程的危险。在化工过程工业中，SIS是最特别的最重要的保护的保护措施之一。同大部分控制系统一样，它包含感应器，一个控制器 （通常称为 逻辑解决者 ) 和预先条件被毁坏时的稳定状态的最后的元素。SIS设计为安全加上特别容易理解和标准需要所有的知识以及设计所要求的正常控制系统的所有知识和技能。如果SIS发生失败，避免意外事件，像是爆炸、过程损害、环境的损害、费用的损失和人类生命的损失很困难。SIS，因此，一定被彻底地而且有系统地在设计阶段期间查证而且有效。SIS的不可实行设计导致程序关闭或者导致不正常的状态。大部分现有方法，像是 HAZOP（危险和可操作性研究）、FTA（过失树分析）、 FMEA（失败模态和效果分析）, 等等普遍作为工业领域中证明 SIS 的危险、安全性和可信度。然而，这些方法通常是耗费时间的而且需要人力。模拟器时常被用来分析以一个测定的模型为基础的控制制度和程序变数的行为。虽然检查模拟的输出有时是有帮助的，但是，在实际中，这一个方法不适当的处理不连续的事件和行为，因为SIS控制逻辑是致力于不连续的事件和行为。这研究计划是一个新颖方法查证化工过程的SIS控制逻辑设计的有效性。被提议的方法是那最近已经在系统的设计、逻辑和行为的完成中达成重要的结果的样板的检查。确认是支持一个错误发现和系统设计的修正的技术。更明确地说，这一个过程的建立、设计实现了它的要求。模型检查为在设计策略的结束的过失是无法接受的：大量的努力会被需要修理或者修正此时被发现的一个错误。为了要见到错误在哪里和如何引起错误整个的设计策略会需要被打乱。本文介绍被证明了的模型核查，该模型被应用于化工系统中SIS全新的设计。本文指出了化工工业过程SIS控制逻辑的模型发展和目前模型检查被有效的用于SIS控制逻辑状况的发展。2.模型检查检查模型的基本目的是使用运算法则，它被计算机工具运行查证系统的正确性。用户输入系统模型 （可能的行为）的描述, 需求规格 （期待的行为）的描述造成确认决定于机器。如果一个错误被识别样板的检验员提供一个反例的成绩在哪一个之下境况错误能被产生。反例有情节在哪一个模型做出一不想要的举止。如此反例提供证据模型是有过失的而且需要被校订。这让使用者位于错误而且在继续之前修理样板的规格。如果没有错误被发现，使用者能精炼它的样板描述 （藉由考虑较多的设计决定举例来说，所以模型变成较多的具体现实的）而且能重新开始确认程序。图 1 表示检查的模型的确认方法学。被提议的方法在一些利益之后包括: （Kim， 2006)1.检查的模型是完全自动、快速的。2.检查的模型能被适用于部分的设计，而且因此能提供关于一个系统正确性的有用资讯即使系统不完全被指定。3.样板的检验员相当方便使用者使用4.检查的模型更可适用控制强烈的申请，像是 SIS 控制逻辑。5.检查的模型能产生反例，能被用来援助除错。模型检查，方法本来被Clarke,Emerson & SIStla(1886)。Moon和Moon等人 (1992,1994) 应用这一个确认方法到自动确认的研究不连续的化学过程控制制度。(也就是开关的开关、泵、接替者，战车水平和开关）他也应用了 PLC 建立的化学的处理系统的在安全和可操作性的确认方法。(1994,Moon等人，1997)Probst,Powers,Long，和Moon(1997) 使用火炉系统的阀门有黏性的例子建议决定性的操作步骤的方法。土耳其人 （1999) 为为安全确认取得有关的动力学和现象的不连续模型的工程呈现了一个程序。因为一届处理，Kim和Moon(2000) 因为在操作时间表方面发现错误计划了一个方法。Yang,Tan，和他(2001) 学习了安全互锁系统可操作性的确认。Milam(2003)使确认成为不同化学的程序的组件了。我们崭新应用这方法在化学的工业程序中提供而且修正 SIS 的设计。这一个方法被决定 SIS 的无错误位置而且自动地找合乎逻辑、不能实行的错误哪一个难以用手找的个案研究测试。Fig. 1. The verification methodology of model checking3.模型、模拟和规格一个模型检查，工具(UPPAAL被用于本文)接受系统需求或者设计(被称为模型)和最后一个系统预期满意的财产(被称为规格)。那样板的检查工具能被用来有关于一个自动机械装置决定给定财产的满足。(Alur & Dill, 1994)如果财产没被满意，诊断的痕迹能被产生指出财产可能如何被违犯。它也提供一个允许系统描述的一个可能动态行为的图解式使看得见的模拟器。(也就是，象征的痕迹)诊断的痕迹，被产生以防万一财产被违犯，被喂回到模拟器以便它能与图解式发表的帮忙一起分析. (Kim, Lee, & Moon, 2006)为了要自动地查证 SIS 的设计，控制导向的系统，信号和被控制逻辑，各种不同的程序变数展现的现象，操作程序，操作员行为和他们的网络必须在仿制部份方面被描述。模型为程序和 SIS 控制逻辑分别地因程序描述和 SIS 控制逻辑描述而发展。当查证 SIS 控制逻辑的时候，完全和模型的正确性是主要议题。样板的描述是与简单的数据的一种非决定论的被防护着的指令语言。(举例来说跳跃完整的事物，排列)工具服务当做一个模型或把程序行为(举例来说给，装阀门抽，马达)说成是的设计语言，自动机械装置和 SIS 的网络控制化学的工业程序的程序逻辑。模拟器是提供的在早的设计阶段期间和如此使系统的可能动态实行的考试能够的一个确认工具一廉宜的在包括系统的无遗漏动态行为的样板检验员的确认之前过失发现意指。提供系统描述的可能动态行为的图解式的使看得见的和录音的一个图解式的模拟器，也就是系统被陈述的代号的序列。它也被用来使被样板检验员产生的痕迹看得见。给特定的财产和要检查的可操作性的疑问语言是一个 CTL（计算的树逻辑）的子集。疑问语言有路径公式和州公式。州公式描述，个体陈述，然而路径公式在模型的路径或痕迹之上定量。路径公式能进入能达到性、安全和可操作性之内被分类。CTL 已经通常被用于许多检查，工具和它的有力效率已经被从系统逻辑规格的许多申请证明的模型。4.个案研究4.1压力阀门系统用压力指示器图 2 举例说明用液化石油气渠道的压力指示器管理阀门系统的压力。这一件个案研究的目的将查证控制压力指示器的位置为安全互锁控制制度。程序有二插入物瓦斯流程和一出口瓦斯流程。一插入物 flowindicates 的压力20kg/cm2 G 和另外一是 12kg/cm2 G。二插入物流程的压力能被振动，而且出口流程的压力也能因插入物流程而振动。较正常压力的出口是 12kg/cm2 G。 压力 12 kg/cm2 G 插入物流程的振动能被忽略因为由于相同的压力它有对出口流程的压力的小效果。20 kg/cm2 G插入物流程使用管理阀门(PV)的一压力是受约束的压力至12kg/cm2 G。Fig. 2. Pressure regulating system图 3 表示 PI101 的模型描述。区域inlet01 和 inlet02能从开始的州被石绵水泥板到正常或不正常的，从常态到不正常的和从不正常的对常态任意地。如果inlet01 和 inlet02是常态，出口的状态指出常态和不正常的如果inlet01是不正常的或者插inlet02不正常的或者两者是不正常的。PI101 的开始状态取消。如果只有出口变成不正常，它打开，直到出口来向后正常的州。在 PI101 打开之后，如果 PI101 关掉，inlet02的状态被石绵水泥板到使常态化然后它变成正常。Fig. 3. The model description of PI101给确认的 CTL 的规格是：A!(inlet02_normal=1&PI101_on=1) 这规格表现，没有情形在哪一个虽然由于出口inlet02是流动的常态不正常的州，inlet02透过管理阀门的压力通常被控制。PI101 情形的规格结果没被满意。从结果，我们识别， PI101 是压力指示器的一个得不到位置。图 4 表演 PI101 没被满意的痕迹。因为一个压力指示器位于出口流程线，所以如果 PI101 ，当inlet02是正常的流程，而且inlet01是不正常的流程时候，管理阀门的压力不必要地被操作。Fig. 4. A counter-example trace of the specification4.2 然水供应系统天然水供应系统是在化学的工业植物的一般的程序。图 5 是在石化的植物的一个 PID (管道和仪器)的部份。Fig. 5. Water supplying system in petrochemical processFig. 6. The model description of the process.Fig. 7. A counter-example trace of the specification.天然来自一条河的生的水在生的水池塘中被储存。水经过一个泵流到生的水箱。Thewater 经过三个阀门 (V22、V23和V14) 陷入植物。水经过阀门22 作为程序的冷却水, 为澄清剂饲养经过阀门 23, 和为火水或紧急的阵雨经过阀门 14。阀门 14 直接地被连接到那被泵和生肉之间的途径渠道水箱。因为它作为紧急的情形，所以阀门 14 总是被打开。系统有二个泵，一在平常的时间被操作和另外的正在站立藉着泵。如果一个泵混乱又另外泵将会立即地被操作。这些泵从指示器 I-100 得到一个信号。I-100 被压力控制器 PI101 或同高的控制器 LIC-101 控制。PI101 拿形式给信号压力翻译者 PT1, 监听从生的水池塘到泵的流程的压力。如果 PI101 指出低的低点压力，泵自动地关掉；否则泵通常被操作。如果 I-100 被连接到 LIC-101, 当生水箱的水平高度地是高的，而且泵关掉这信号的时候， I-100 从 LIC-101 得到一个信号。一定没有情形，二个泵同时关掉，因为水总是准备为紧急使用。至少，一个泵需要被操作。这一个例子表现搜寻在早的设计阶段中被器具所有可能的控制逻辑的系统的安全的这些不安全控制逻辑。对于确认的样板描述有 10个组件，像是图 6 。单位或设备不在下面存在不被做模型因为这些能当做大约系统的分析控制逻辑被省略。给确认的 CTL 的规格是：A!(PI101=1&Pump1=0&Pump2=0&Lv=1&(!(Pump1_fail=1)&!(Pump2_fail=1) 这规格表现没有生的水池塘的插入物流程不是低的低点压力的情形，没有失败，二个泵没被操作。结果为规格没被满意。反例的痕迹在图 7 被显示。当生水箱的水平带领的时候