Sciweavers

Share
DFG
2004
Springer

Verification of PLC Programs Given as Sequential Function Charts

9 years 11 months ago
Verification of PLC Programs Given as Sequential Function Charts
Programmable Logic Controllers (PLC) are widespread in the manufacturing and processing industries to realize sequential procedures and to avoid safety-critical states. For the specification and the implementation of PLC programs, the graphical and hierarchical language Sequential Function Charts (SFC) is increasingly used in industry. To investigate the correctness of SFC programs with respect to a given set of requirements, this contribution advocates the use of formal verification. We present two different approaches to convert SFC programs algorithmically into automata models that are amenable to model checking. While the first approach translates untimed SFC into the input language of the tool Cadence SMV, the second converts timed SFC into timed automata which can be analyzed by the tool Uppaal. For different processing system examples, we illustrate the complete verification procedure consisting of controller specification, model transformation, integration of dynamic plant mode...
Nanette Bauer, Sebastian Engell, Ralf Huuck, Sven
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2004
Where DFG
Authors Nanette Bauer, Sebastian Engell, Ralf Huuck, Sven Lohmann, Ben Lukoschus, Manuel Remelhe, Olaf Stursberg
Comments (0)
books