CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

On Formal Specification and Verification of Function Block Applications in Industrial Control Logic Development

Oscar Ljungkrantz (Institutionen för signaler och system, Automation)
Göteborg : Chalmers University of Technology, 2011. ISBN: 978-91-7385-569-3.- 195 s.

Developing a control system for an automated manufacturing system is a challenging task. In addition to controlling and coordinating the machines and robots used in the production, the safety of the operators must be assured. The control system should also be easily modifiable and quickly made fully operational, to reduce down-time and ramp-up-time of the manufacturing system. To handle these challenges, Programmable Logic Controllers (PLCs) and a set of standard programming languages are typically used. Many industrial practitioners also use standardized programming structure and they reuse code in form of function blocks between and within different programming projects. Although the PLC programming is well standardized, there is no established standard for the specifications. The function blocks are typically documented informally, for instance using natural language and pictures, or not specified at all. Unambiguous specifications of function blocks would not only promote efficient reuse and facilitate verification, but are fundamental for the part handling safety. International safety standards emphasize the importance of specifying and verifying safety-related software. This thesis proposes the Reusable Automation Component (RAC) framework for formal, mathematical specification and verification of function blocks. The RAC formal specification removes ambiguity and enables automated and exhaustive off-line verification using model checking. Developing formal specifications is typically a tough task for PLC programmers and maintainers and this thesis therefore proposes methods and a language for assisting the specification development. The main contributions of the thesis are the proposed specification assistance and industrial studies on PLC programming and function block specifications. A prototype RAC tool has been implemented in which the function blocks can be specified and then verified using a model checking tool. Several industrial examples show that the RAC framework may help the users to find errors and inconsistencies within the function blocks, and to confirm that the expected safety properties are fulfilled.

Nyckelord: manufacturing automation software, programmable logic controller (PLC), safety logic, software requirements and specification, formal verification, model checking, temporal logic, reusable automation component (RAC), IEC 61131, function block

Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2011-09-13. Senast ändrad 2013-09-25.
CPL Pubid: 146137


Institutioner (Chalmers)

Institutionen för signaler och system, Automation (2005-2017)


Information Technology

Chalmers infrastruktur

Relaterade publikationer

Inkluderade delarbeten:

A formal specification language for PLC-based control logic

Formal Specification and Verification of Industrial Control Logic Components

Practice of Industrial Control Logic Programming using Library Components

An Empirical Study of Control Logic Specifications for Programmable Logic Controllers

Towards Industrial Formal Specification of Programmable Safety Systems


Datum: 2011-10-14
Tid: 10:15
Lokal: HC1, Hörsalsvägen 14, Chalmers University of Technology, Göteborg
Opponent: Prof. Georg Frey, Department of Mechatronics Engineering, Saarland University, Saarbrücken, Germany

Ingår i serie

Doktorsavhandlingar vid Chalmers tekniska högskola. Ny serie 3250