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...

Full description

Saved in:
Bibliographic Details
Main Authors: Lohmann, S., Stursberg, O., Engell, S.
Format: Conference Proceeding
Language:English
Subjects:
Automata
Automatic control
Computer languages
Cooling
IEC standards
Laboratories
Logic programming
Logic testing
Programmable control
Safety
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0743-1619
2378-5861
DOI:10.1109/ACC.2007.4282937