Title: Verification and implementation of software for dependable controllers

Authors: Krzysztof Sacha

Addresses: Warsaw University of Technology, Nowowiejska 15/19, Warsaw, 00-665, Poland

Abstract: A method is described for modelling, verification and automatic generation of code for PLC controllers. The requirements for a controller are modelled using UML state machine diagram, with a formal semantics given by a finite state time machine. The model can automatically be converted into a timed automaton, embedded into a model of the environment (a controlled plant) and verified against safety requirements using UPPAAL – a free model checking tool for the networks of timed automata. The verified model can automatically be translated into a program code in one of the IEC 61131 languages, e.g., ladder diagram of structured text.

Keywords: critical computing; dependable controllers; modelling; model verification; automatic code generation; reliability; programmable controllers; PLCs; programmable logic controllers; UML; state machine diagram; semantics; embedded systems; safety requirements.

DOI: 10.1504/IJCCBS.2010.031717

International Journal of Critical Computer-Based Systems, 2010 Vol.1 No.1/2/3, pp.238 - 254

Published online: 21 Feb 2010 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article