Automatic program verification of continuous function chart based on model checking

Awang N.I. Wardana, Jens Folmer, Birgit Vogel-Heuser

Research output: Contribution to conferencePaperpeer-review

15 Scopus citations

Abstract

Continuous function chart (CFC) is a graphical-oriented programming language that is widely used as application programs in process industry (e.g. pharmaceutical plants, chemical plants and power plants). The CFC programs have to be validated whether they fulfill the safety requirements that are specified in the control task specifications to verify their correctness before they are being tested by user in the plant. Nowadays, this verification is being done manually. This potentially causes errors and it is very time consuming. In this paper, we present an automatic verification approach to ensure the correctness of the CFC programs. Our verification approach is based on model checking where the CFC programs are modeled into timed automata.

Original languageEnglish
Pages2422-2427
Number of pages6
DOIs
StatePublished - 2009
Event35th Annual Conference of the IEEE Industrial Electronics Society, IECON 2009 - Porto, Portugal
Duration: 3 Nov 20095 Nov 2009

Conference

Conference35th Annual Conference of the IEEE Industrial Electronics Society, IECON 2009
Country/TerritoryPortugal
CityPorto
Period3/11/095/11/09

Fingerprint

Dive into the research topics of 'Automatic program verification of continuous function chart based on model checking'. Together they form a unique fingerprint.

Cite this