Verification and validation of safety applications based on PLCopen safety function blocks |
| |
Authors: | Doaa Soliman Georg Frey |
| |
Affiliation: | Chair of Automation, Saarland University, University Campus Building A5.1, 66123 Saarbrücken, Germany |
| |
Abstract: | Functional Safety is a major concern in the design of automation systems today. Many of those systems are realized using Programmable Logic Controllers (PLCs) programmed according to IEC 61131-3. PLCopen - as IEC 61131 user organization - semi-formally specified a set of software function blocks to be used in safety applications according to IEC 61508. In the presented work, formal models in the form of timed automata for the safety function blocks (SFBs) are constructed from the semi-formal specifications. The accordance of the formalized blocks to the specification is verified using model checking. Furthermore, their behaviour is validated against specified test cases by simulation. The resulting verified and validated library of formal models is used to build a formal model of a given safety application - built from SFBs - and to verify and validate its properties. |
| |
Keywords: | Timed automata Safety function block IEC 61508 IEC61131-3 Verification and validation Model-checking |
本文献已被 ScienceDirect 等数据库收录! |