Conference proceedings article
Algorithmic verification of logic controllers given as sequential function charts



Publication Details
Authors:
Remelhe, M.; Lohmann, S.; Stursberg, O.; Engell, S.; Bauer, N.
Editor:
IEEE
Publication year:
2004
Pages range:
53-58
Book title:
Computer Aided Control Systems Design, 2004 IEEE International Symposium on
ISBN:
0-7803-8636-1

Abstract
The a-posteriori analysis of logic controllers can be a suitable means to detect design flaws if the controller was not developed by a synthesis algorithm that correctly considered all relevant requirements. This paper advocates the verification of logic controllers with a special focus on the following three issues: (a) the control code is given as a sequential function chart (SFC), a description language becoming increasingly popular for industrial controllers; (b) the cyclic operation mode of the hardware on which the controllers is implemented is taken into account; (c) specifications of the control logic that include timers and the real-time behavior of the controlled plant are considered. We propose an approach in which the SFC controller is first translated into a timed automaton using an algorithm that explores a special graph grammar. The automaton can then be composed with a timed automaton modeling the plant behavior, and model-checking of the composition reveals whether a given set of requirements is fulfilled. All steps of the procedure are illustrated for the example of a controlled evaporation system


Authors/Editors

Last updated on 2019-25-07 at 10:08