Comparison of Event-Triggered and Cycle-Driven Models for Verifying SFC Programs

As a complement to testing procedures, verification techniques as e.g. model checking have been proposed to analyze logic controllers specified as sequential function charts (SFC). For the success of these techniques suitable execution models of the SFC and of the programmable logic controllers (PLC) on which the SFC are implemented and operated in practice are crucial. This paper investigates and compares two different suggested transformation schemes for mapping SFC into timed automata (TA): an event-triggered and a cycle driven scheme. For the example of a laboratory experiment, the paper shows how the schemes lead to TA models of the controller which can, when complemented with appropriate plant models, be used for verifying properties as e.g. safety by employing the software tool UPPAAL. The event-triggered transformation scheme is found to lead to considerably smaller TA models and hence to be more suitable for verification purposes.