Name
Title | ||
|---|---|---|
Transformation of Function Block Diagrams to UPPAAL timed automata for the verification of safety applications. |
Abstract | ||
|---|---|---|
Verification of IEC 61131-3 based safety applications is a challenge in the industrial automation domain. In this paper, the transformation of FBD diagrams to UPPAAL formal models was adopted to address this challenge. A set of transformation rules are defined for the automatic transformation of IEC 61131-3 Function Block based safety applications to UPPAAL timed automata models. These models are next used for the verification of the safety application. Both the source and the target domain models have been formally defined and these definitions are used for the definition of the transformation rules. Based on this a prototype model transformer was developed using Java. The transformer was used with various safety applications to check the efficiency of the transformation process. A laboratory system is presented as a case study to highlight the proposed approach. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1016/j.arcontrol.2012.09.015 | Annual Reviews in Control |
Keywords | Field | DocType |
Function Block Diagram,Timed automata,IEC 61131-3,UPPAAL,Verification,Safety applications,PLCopen | IEC 61131-3,Programming language,Computer science,Automaton,Transformer,Automation,Control engineering,Function block diagram,Java,Block diagram,Reliability engineering,Domain model | Journal |
Volume | Issue | ISSN |
36 | 2 | 1367-5788 |
Citations | PageRank | References |
12 | 0.76 | 7 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Doaa Soliman | 1 | 13 | 1.53 |
| Kleanthis Thramboulidis | 2 | 293 | 38.13 |
| Georg Frey | 3 | 172 | 40.32 |