- Home
- Companies
- Inderscience Publishers
- Articles
- Verification and implementation of ...
Verification and implementation of software for dependable controllers
Courtesy of Inderscience Publishers
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
-
Most popular related searches
Customer comments
No comments were found for Verification and implementation of software for dependable controllers. Be the first to comment!