基于PLC建模的正式检查方法

基于PLC建模的正式检查方法摘文高可靠性是电气控制设备的关键性能。PLC是结合了计算机技术、自动控制技术和通信技术,被广泛用于工业过程的自动化技术。在本文中,提出了一个有效的方法用于PLC系统的建模和验证。为了确保PLC的高速特性,我们提出了一个“时间间隔模型”技术和“notice-waiting”。它可以降低状态空间,也可以验证一些复杂的PLC系统。同时,从PLC构建模型转换Promela语言来获得建模和检查工具PLC-Checker的PLC系统设计。尽管PLC这种逻辑错误发生的概率非常小,但是发生错误可能导致系统崩溃。接下来使用PLC-Checker检查一个古典PLC的例子,这是一个反例。关键词:模型检查、PLC建模、PLC-Checker正式的方法介绍[1]PLC是一种自动控制装置,可以从传感器接收信息,计算设备或其它PLC逻辑输入信号和输出信号的逻辑处理。可以使用标准语言编写控制算法,如梯形图(LD)、结构化的文本(ST)或指令表(IL)。[2]使用PLC技术的可编程语言来控制大规模集成电路已广泛应用于工业。关于关键软件的安全可以严重危害生命或财产,验证关键软件的安全已经成为不可或缺的步骤，所以需要保证软件质量。目前的PLC验证方法仍是通过仿真和测试。然而,他们不能涵盖所有可能的情况下,特殊的PLC的设计模型是否满足需求。因此,模型检测技术引入PLC的领域。提供给PLC设计重要的理论分析。[3]PLC模型检测的主要步骤是建立PLC模式,如建立模型函数图表。[4]关于PLC模型建立的时间属性。它可以被建模的方法有时间自动机[5]或时间段建模方法[6]。[7]因此状态空间模型与时间自动机相比将下降。不管怎样选择,最终都可以抽象模型。对于如何构建一个好的PLC抽象模型检查是最重要的问题。手动建模很容易引入许多错误,所以建立一个集成建模和测试工具是非常重要的,这是本文关注的问题之一。PLC控制程序在实时操作系统中运行(多任务或单一任务);本文主要是基于多任务调度PLC系统。第二节的文章介绍了PLC系统的建模方法。第三节给出了此模型的分析和改进,还有我们需要减少虚拟错误的概率。第四节是设计一个模型检测工具PLC-Checker检查建立模型,包括介绍了PLC程序转换成主要的输入语言Promela的代码。最后，介绍了一个应用PLC-Checker检查和一个关键问题的经典例子。PLC建模有三个步骤的模型检查:建模、属性描述和验证。最重要的是如何构建系统模型。在系统中,PLC控制器不是孤立的,而是由驱动程序和人控制它的工作环境[8]。因此,这些因素也应该被建模。环境、人、PLC控制器是相互独立和并发的逻辑。同时,模型检查器转换的输入语言Promela侧重于描述并发,所以从这个观点中,我们建立这些因素分成几个并发进程转换符合检查,它也会准确地描述这个系统。为了描述方便,他们将被称为并发实体。PLC控制器与并发交互实体通过符号表来表示。PLC系统的符号包括I(输入端)、Q(输出端口)和M(中间继电器)。图1是一个图表的PLC系统模型。时间间隔建模策略:使用特定的并发实体的一些特定的状态代表了并发中的实体状态,而不考虑系统时钟。这可能忽视特定的时差,从而简化了PLC模式。建模策略不添加系统时钟属性,不能完全符合最初的PLC模式。主要是由于加入系统时钟会引起PLC系统模型太大,没有模型检查工具来处理如此大的模型。建模的起点状态是不考虑PLC迁移时扫描的数量有经验。不管经历了多少扫描,他们都将包括在这个模型。换句话说,真正的模型将是建立模型的一个子集(时间间隔模型)。PLC的现实环境是复杂的,包括各种硬件和人为的行为。下面我们将分析不同类型的PLC并发实体环境。硬件实体硬件实体的PLC中,PLC控制系统主要是一些设备。这些设备的状态可以输入PLC控制器。虽然硬件都有自己的工作流程,但这个流程是由硬件需求决定的。因此,绑定硬件实体及其相关I和Q,。这个工作流程可以抽象为自动机。该自动机用于描述硬件的工作状态。定义2.1.一个硬件实体是一个元组Env=<Ienv,Qenv,A>,Ienv是I的端口绑定与硬件实体，Qenv是Q的端口绑定的实体。A是自动机描述实体的工作流程，A是一个元组A=<s0,S,T>,当s0的初始状态是A，S是特定集合T的转移。硬件实体的状态是I的一个子集符号,和标志每个状态都映射到{真,假},I没有出现的特定状态可以是真或假(即:任意行动)。硬件实体的转移与Q的子集直接表达符号表示所有问符号子集是真实的同时将驱动状态之间的迁移。硬件实体的状态转换图还需要从这个状态转换图指定一个初始状态。硬件实体的状态转换图是基于分工的象征,不考虑时间和属性。硬件实体状态转换图实际上是一个忽略时间的抽象硬件实体,且需要抽象模拟硬件的参考。简单输出实体简单的输出实体只有绑定Q端口不使用I端口，这意味着简单输出实体没有状态转换图。简单的输出实体显示了PLC的工作状态的设备,像一个信号光。使用简单的输出实体是绑定的Q端口,PLC可使其进行逻辑设计。M端口Q端口I端口PLC控制器扫描和计算设置端口的值并发的实体简单的输出实体硬件实体M端口Q端口I端口PLC控制器扫描和计算设置端口的值并发的实体简单的输出实体硬件实体人类行为实体图1所示PLC系统模型模型和实际模型并不完全相同的情况下,它应该是远大于实际模型。与时间间隔模型相比,该模型进一步降低实际系统之间的距离,大大减少发生误差的机会。模型检测工具会给出一个破坏特性制度的反例;很容易手动确定反例在现实系统是真的还是假的。如果这一个反例是在原系统存在的错误。那么这个错误是因为在抽象模型中比真正的系统大,这是一个误差。因此,虽然这个时间间隔模型和原系统不完全相同,但是通过这个模型,我们可以判断一个系统满足一定的特性,如果不是我们可以找到一个特定的反例(仍然需要更多的研究来确定是否有误差)。模型并不等同与原系统,主要是因为有许多因素难以模型在实际系统,其中一些可能会导致错误。如果所有的因素进行建模,这将导致建立一个巨大的模型,无法检查,或者根本无法实现。时间间隔模型抽象的关键因素从实际系统和模型,大大减少了状态空间,降低时间复杂度。注意等待机制的存在,使添加的模型变得更接近实际系统,不仅降低了时间复杂度,同时减少了之前提到的误差。4所示。PLC模型检查PLC广泛应用在许多应用程序和很多设备中;这是一个大的研究领域。PLC任何的工作环境,都包括了不同的设备和人,所以PLC系统并发。同时,PLC系统很难找到如果有一些错误,主要是因为逻辑设计的错误,而不是计算误差。我们专注于PLC程序逻辑过程的检测,和这个逻辑可以完全由一些逻辑描述。因此,为了简化PLC程序模型,集中在模型检查,我们进行以下设置:PLC是一种逻辑控制程序,所有的控制变量只有0和1两种状态;在并发环境中PLC程序运行。在这种情况下,PLC编程更可能有一些错误不容易找到。具上述特点,我们使用模型检查工具转换(我们的工具PLC检测程序实现NuSMV)对上述建立的模型检查。我们做了一系列的转换规则,建立上述模型转换为输入语言Promela,系统属性也需要翻译成Promela,转换后将把它们放在一起,然后执行检测。PROMELA语言是一个C类语言,它们在语义上是相似的。所以我们只会给一些例子显示翻译的基本概念。看到PROMELA语言的细节,请访问。我们将介绍三个PROMELA文件作为输入的一部分。PLC控制器的代码PLC控制器是由多个网络组成的。PLC控制器的代码也是来自网络。当然,在那之前,你应该申报所需要的变量。每个网络都有其输入端口和输出端口,每个端口可以表明一个布尔表达式。我们分配输出端口的值通过计算逻辑的输入端口。这是PLC网络的翻译方法。这是一个老转换网络的例子:if::Exp(R)==1->Q=0;::else->if::Exp(S)==1->Q=1;::else->skip;fi;fi;/*Exp(S)是布尔表达式的港口Exp(R)是R的布尔表达式端口Q是输出端口*/并发实体代码我们认为每个并发实体一个独特的过程,不管它是人类行为或设备。这些过程与PLC控制器进程共享变量。必须这样做,以确保系统的并发性。在本文的第二部分,我们将讨论所有的并发实体建模为一个自动机。自动机的意思是从一个状态转移到另一个地方。我们使用I端口形成实体的状态。使用goto语句作为转移(就像在汇编语言)。一个简单的例子如所示:StateA:atomic{if::Q1->{IB,gotoStateB}::Q2->{IC,gotoStateC}fi;}/*StateA状态的标签Q1、Q2是转移的条件IB是设置状态值状态B的值gotoStateB意味着跳到StateB*/代码的特性特性是PLC系统必须遵守的规则。我们使用LTL(线性时间逻辑)公式的输入格式。我们应该写计数器属性的机制。转换会在一个我们特定的情况下发生,这应该是一个反例。我们不能直接写LTL公式,要通过使用宏。首先我们应该在一个宏定义所有命题LTL(如#definepi5==0),然后使用LTL定义形成命题公式。SPIN可以自动转换LTL公式PROMELA代码通过使用“SPIN-f”指令(见更多的细节在SPIN手册)。注意等待机制在建模讨论,我们建议增加注意等待机制。这种机制也需要反映在代码。具体实现是为每个non-PLC签署一些变量的过程(所有流程PLC控制器除外)作为一个信号。自动机状态转移标签时,信号变量设置为0,和下一个任务需要1继续这个变量。PROMELA语法特性的结果,过程将挂起。PLC过程中没有这样的限制,相反,PLC过程可能将这些变量设置为1,从而确保每一个动作必须经过至少一个PLC扫描完成。这就是所谓的注意等待机制。遵循以上四个步骤,我们得到一个完整的代码的SPIN系统的输入文件。然后我们可以使用SPIN检查模型。SPIN模型检查器的操作步骤,看SPIN的手册(请访问)。SPIN结果是否找到反例,我们可以使用上述理论分析SPIN的跟踪文件。使用这种检测机制,我们开发了一个工具检查PLC检测程序模型。它有助于构建可视化模型和实施检查,并可以给一个简单的分析结果。当然,相反的例子,找到应用手动检查以确定是否真正的反例。然而,在小径的帮助文件,这不是一个非常困难的任务。我们还成功地实现一些检查使用PLC检测程序。在一个典型的范例,找到了一个反例。虽然反例的发生概率很低,但它确实发生,可能造成严重后果。这个工具也证明了本文理论的正确性和有效性。5。运行PLC检测程序我们将介绍PLC的有效性检查器通过检查一辆双门通道模型。双门通道用于防止一个封闭的房间与外界联系。通过输入梯克和并发实体工具,在符合属性的定义下,我们执行检查。图3显示了结果。我们可以看到,有一个错误的结果。它被证实是一个真正的反例通过检查手动跟踪文件。也就是说我们的机制是有效的检查这样的PLC程序。6。结论我们研究的理论建模和检查PLC系统在正式的方法。PLC建模分析的要求,和并发实体的模型是建立在时间间隔的方法。然后我们证明的时间间隔模型一套超级的PLC系统,通过添加注意等待机制和减少模型。这也保证了考试的所有更改可以扫描系统中PLC控制器。我们发现系统的误差通过检查系统的反例。最后,用SPIN的方式检查模型。也对相应的模型检查工具PLC-Checker介绍。在这个阶段,机制仍然有许多缺陷,如处理定时器。但它在解决问题的探索有伟大的和独特的优点，表现我们仍在积极探索问题。引用[1]Pavlovic,R.PingerandM.Kollmann,“AutomatedFormalVerificationofPLCProgramsWritteninIL,”ConferenceonAutomatedDeduction(CADE),Bremen,July2007,pp.152-163.[2]M.B.YounisandG.Frey,“FormalizationofExistingPLCPrograms:ASurvey,”ProceedingsofCESA2003,Lille,2003.[3]N.Bauer,S.Engell,S.Lohmann,M.RemelheandO.Stursberg,“VerificationofPLCProgramGivenasSequentialFunctionCharts,”LectureNotesinComputerScience,Vol.3147,2004,pp.517-540.[4]S.R.Koo,P.H.SeongandS.D.Chaa,“SoftwareDesignSpecificationandAnalysisTechniquefortheSafetyCriticalSoftwarebasedonProgrammableLogicController(PLC),”ProceedingsoftheEighthIEEEInternationalSymposiumonHighAssuranceSystemsEngineering(HASE’04),Florida,March2004,pp.283-284.[5]A.MaderandH.Wupper,“TimedAutomatonModelsforSimpleProgrammableLogicControllers,”Proceedingsofthe11thEuromicroConferenceonReal-TimeSystems1999,York,June199