Download of the papers is allowed for personal use only!

Various copyright restrictions apply.

**Abstract.**
Programmable Logic Controllers (PLC) are widely used as device
controllers for assembly lines, chemical processes, or power plants.
Sequential Function Charts (SFC) form one of the main programming
languages for PLCs and, therefore, the correctness of the PLC software
implemented as SFCs is crucial for a safe operation of the controlled
process. A prerequisite for reasoning about program correctness is a
clear understanding of the program semantics. As we show in this work,
this is currently not the case for SFCs. Although syntactically
specified in the IEC 61131-3 standard, SFCs lack an unambiguous,
complete semantic description. We point out a number of problems and
explain how these lead to different interpretations in commercial
programming environments. To remedy this situation we introduce a
parameterized formal semantics for SFCs including many high-level
programming features such as parallelism, hierarchy, actions and
activity manipulation. Moreover, we show how to extend the semantics
to include time, clocks, and timed actions. The presented semantics is
general enough to comprise different existing interpretations while at
the same time being adjustable to precisely represent each of them.

Nanette Bauer, Sebastian Engell, Ralf Huuck, Sven Lohmann, Ben Lukoschus,
Manuel Remelhe, Olaf Stursberg.

**Verification of PLC Programs given as Sequential Function Charts.**

*Integration of Software Specification Techniques for Application in
Engineering, Lecture Notes in Computer Science 3147,*
Springer-Verlag, 2004.

**Abstract.**
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 models, and identifying errors in the control
program by model checking.

Nanette Bauer, Ralf Huuck, Sven Lohmann, Ben Lukoschus.

**Sequential Function Charts: Die Notwendigkeit formaler Analyse.**

*atp - Automatisierungstechnische Praxis,*
Oldenbourg Wissenschaftsverlag, August 2004.

**Zusammenfassung.**
Sequential Function Charts (SFCs, im Deutschen auch als
Ablaufsprache bezeichnet), stellen eine in der Norm IEC 61131-3
definierte Koordinations- und Programmiersprache für
speicherprogrammierbare Steuerungen (SPS) dar. Gerade für die
bei SFCs besonders interessanten strukturellen Konzepten
Parallelismus und Hierarchie liefert die Norm jedoch nur
informale und zum Teil mehrdeutige Beschreibungen der
Programmsemantik. Der Beitrag zeigt anhand eines Vergleichs
von SPS-Entwicklungswerkzeugen verschiedener Hersteller,
dass daher das Verhalten eines SFC-Programms nicht immer
klar vorhersagbar und somit auch nicht immer portabel ist, und
nennt Vorschläge zur Umgehung von Mehrdeutigkeiten. Außerdem
wird ein Ansatz zur formalen Analyse von SFCs vorgestellt, der
im Gegensatz zu herkömmlichen Testverfahren eine weitgehend
automatisierte Verifikation von Programmeigenschaften
ermöglicht.

**Abstract.**
Sequential function charts (SFC) are a high-level graphical programming
language for programmable logic controllers. Their main purpose is to provide
a structure and organization of the control flow. Therefore, various
features such as parallelism, priorities on branching transitions, and
activity manipulations are incorporated. The syntactic rules for building
SFCs are formally defined in IEC 61131-3. It is, however, still possible to
derive SFCs from these rules whose structure do not make sense. In this work
we give a characterization for so-called *safe SFCs.* Moreover, we
present a semantic definition for them, as well as an algorithmic approach to
automatically detect whether an SFC is safe or not.

Paper (updated version):
[PDF]

Slides:
[PDF (for printing,
without animations)]
[PDF (for viewing, with animations)]

**Abstract.**
Hybrid systems are well-suited as a design and modeling framework to describe
the interaction of discrete controllers with a continuous environment. However,
the systems described are often complex and so are the resulting models.
Therefore, a formal framework and a formal verification to prove the
correctness of system properties is highly desirable. Since complexity is
inherent, standard formal verification techniques like model checking soon
reach their limits. In this work we present several options how to tackle the
complexity arising in the formal verification of hybrid systems. In particular
we combine the model checking approach with abstraction and decomposition
techniques such as the assumption/commitment method as well as deductive
methods.

[PDF]

Nanette Bauer, Ralf Huuck, Ben Lukoschus.

**A Stopwatch Semantics for Hybrid Controllers.**

*b '02: The XV. IFAC World Congress,*
Barcelona, Spain, July 21-26, 2002.

**Abstract.**
Programmable Logic Controllers (PLC) are frequently used in the automation
industry for the control of hybrid systems. Although the programming languages
for PLCs are given in the standard IEC 61131-3, their semantics are defined in
an ambiguous and incomplete way. This holds in particular for the graphical
language Sequential Function Charts (SFC), a high-level programming language
comprising such interesting features as parallelism, activity manipulation,
priorities and hierarchy. In this work we present a formal semantics for timed
SFCs, which belong to the class of linear hybrid systems.

**Keywords.**
Programmable Logic Controllers, Linear Hybrid Systems,
Sequential Function Charts, Stopwatch Semantics

Goran Frehse, Olaf Stursberg, Sebastian Engell, Ralf Huuck, Ben Lukoschus.

**Modular Analysis of Discrete Controllers for Distributed Hybrid
Systems.**

*b '02: The XV. IFAC World Congress,*
Barcelona, Spain, July 21-26, 2002.

**Abstract.**
The algorithmic analysis of control systems for large and distributed hybrid
systems is considerably restricted by its computational complexity. In order to
enable the verification of discrete controllers for such hybrid systems, this
contribution proposes an approach that combines decomposition, model checking
and deduction. The system under examination is first decomposed into a set of
modules represented by communicating linear hybrid automata. The
*Assumption/Commitment* method is used to to prove properties of coupled
modules and to derive conclusions about the behavior of the entire system. The
individual Assumption/Commitment-pairs are proven using established methods for
model checking.

**Keywords.**
Abstraction, Assumption/Commitment, Discrete Controllers, Model Checking,
Verification.

**Abstract.**
We thoroughly examine the experimental batch plant in its two major operation
modes: a normal operation mode and a failure operation mode. In order to do so,
we use discrete condition/event system as well as timed automata for the
specification and the model checking tools SMV, Kronos and HyTech for
verification.

**Keywords.**
Controller synthesis, Hybrid Systems, Model checking, Verification.

Goran F. Frehse, Olaf Stursberg, Sebastian Engell, Ralf Huuck,
Ben Lukoschus.

**Verification of Hybrid Controlled Processing Systems based on Decomposition
and Deduction.**

*ISIC 2001: 2001 IEEE International Symposium on Intelligent Control,*
Mexico City, Mexico, September 5-7, 2001, pages 150-155.
IEEE Press. ISBN 0-7803-6733-2 (CD-ROM: 0-7803-6735-9).

**Abstract.**
While formal verification has been successfully used to analyze several
academic examples of controlled hybrid systems, the application to real-world
processing systems is largely restricted by the complexity of modeling and
computation. This contribution aims at improving the applicability by using
decomposition and deduction techniques: A given system is first decomposed into
a set of physical and/or functional units and modeled by communicating timed
automata or linear hybrid automata. The so-called
*Assumption/Commitment* method allows to formulate requirements for the
desired behavior of single modules or groups of modules.

Model-Checking is an appropriate technique to analyze whether the requirements
(e.g., the exclusion of critical states) are fulfilled. By combining the
analysis results obtained for single modules, properties of composed
modules can be deduced. As illustrated for a laboratory plant, properties
of the complete system for which direct model-checking is prohibitively
expensive can be inferred by the iterative application of analysis and
deduction.

**Keywords.**
Abstraction, Assumption/Commitment, Deductive Analysis, Discrete Controller,
Hybrid System, Verification.

Paper:
[gzip-compressed PostScript]
[PDF]

Slides:
[PDF (for printing, without animations)]
[PDF (for viewing, with animations)]

Stefan Kowalewski, Peter Herrmann, Sebastian Engell, Heiko Krumm,
Heinz Treseler, Yassine Lakhnech, Ralf Huuck, Ben Lukoschus.

**Approaches to the Formal Verification of Hybrid Systems.**

*at-Automatisierungstechnik,* 49(2):66-74, February 2001.
Special Issue: Hybrid Systems II: Analysis, Modeling, and Verification.
Oldenbourg Verlag. ISSN 0178-2312.

**Abstract.**
This paper presents two different approaches to the problem of formally
verifying the correctness of control systems which consist of a logic
controller and a continuous plant and, thus, constitute a hybrid system. One
approach aims at algorithmic verification and combines Condition/Event Systems
with Timed Automata. The first framework is used to model the controller and
the plant in a block-diagram representation, which is then translated into the
latter model for analysis by available tools. A second approach is presented
which is based on deductive verification. It allows for a structured analysis
of compositional specifications formulated in a temporal logic called
cTLA. This logic is a compositional style oft he Temporal Logic of Actions
established in computer science by Lamport. Both approaches are introduced
using a common example and the results of their application are discussed. As
an outlook, a possible strategy for integrating algorithmic and deductive
verification of hybrid systems is sketched at the end of the paper.

**Abstract.**
Programmable logic controllers (PLCs) occupy a big share in automation
control. However, hardly any validation tools for their software are
available.
In this work we present a lightweight verification technique for PLC
programs. In particular, static analysis is applied to programs written in
Instruction List, a standardized language commonly used for PLC programming.
We illustrate how these programs are annotated automatically by an abstract
interpretation algorithm which is guaranteed to terminate and is applicable
to large-scale programs. The resulting annotations allow static checking for
possible run-time errors and provide information about the program structure,
like existence of dead code or infinite loops, which in combination
contributes to more reliable PLC systems.

Sébastien Bornot, Ralf Huuck, Yassine Lakhnech, Ben Lukoschus.

**An Abstract Model for Sequential Function Charts.**

*Discrete Event Systems: Analysis and Control,
Proceedings of WODES 2000: 5th Workshop on Discrete Event Systems,*
Ghent, Belgium, August 21-23, 2000, pages 255-264, Boston, Dordrecht, London,
2000. Kluwer Academic Publishers. ISBN 0-7923-7897-0.

**Abstract.**
Sequential function charts (SFCs) are systems where every step can contain
other SFCs as well as state transformations. The standard by IEC 1131-3
explicitly defines some languages for this. In this paper we point out that the
standard has many ambiguities, and that it is crucial to have a formal
framework for the definition of SFCs. We define the syntax and semantics of
them. The semantics we give is general enough to cope with different possible
implementations of the standard.

Sébastien Bornot, Ralf Huuck, Yassine Lakhnech, Ben Lukoschus.

**Verification of Sequential Function Charts using SMV.**

*PDPTA 2000: International Conference on Parallel and Distributed Processing
Techniques and Applications,* Monte Carlo Resort, Las Vegas, Nevada, USA,
June 26-29, 2000, volume V, pages 2987-2993. CSREA Press, June 2000.
ISBN 1-892512-51-3.

**Abstract.**
Sequential function charts (SFCs) are defined as a modeling language in
the IEC 1131-3 standard and can be used to structure and drive
programmable logic controllers (PLCs). It includes interesting concepts as
hierarchy, history variables and priority. As the typical application area
of this language is the control of industrial processes, it is obvious that
safety and reliability is a crucial goal for systems using SFCs. In this
work we give an abstract formal model for SFCs and present a method to
automatically verify properties concerning the safety of such systems using
the model checking tool SMV (Symbolic Model Verifier).

Sébastien Bornot, Ralf Huuck, Ben Lukoschus.

**Statische Analysetechniken für speicherprogrammierbare Steuerungen.**

*FBT 2000: 10. GI/ITG-Fachgespräch: Formale Beschreibungstechniken für
verteilte Systeme,* Lübeck, Germany, June 22/23, 2000, pages 175-181,
Aachen, Germany, June 2000. Shaker Verlag.
ISSN 0945-0807, ISBN 3-8265-7491-5.

**Zusammenfassung.**
Speicherprogrammierbare Steuerungen (SPS) unterliegen einer stark
zunehmenden Verbreitung in der Automatisierungstechnik. Während diese
in der Vergangenheit meist nur zur Steuerung einfacher Abläufe
eingesetzt wurden, sind sie heutzutage verantwortlich für die
Steuerung komplexer hybrider Systeme, sei es in der petrochemischen
Industrie oder in Kraftwerken. Daher ist eine korrekt funktionierende
Steuerungssoftware von grundsätzlicher Bedeutung. In diesem Vortrag
wird die Methode der statischen Analyse für eine standardisierte
SPS-Sprache, Anweisungsliste (AWL), vorgestellt. Statische Analyse
umfaßt Techniken, die Laufzeitverhalten ermitteln bzw. nachweisen,
ohne den Code selbst auszuführen. Insbesondere die Technik der
abstrakten Interpretation spielt hier eine wichtige Rolle. Wir werden
diese Techniken mit Bezug auf AWL vorstellen und aufzeigen, welche
statischen Analyseziele für AWL erreichbar sind. Ferner gehen wir
darauf ein, was statische Analyse im Vergleich zu anderen
Verifikationstechniken leistet und wie diese in Kombination genutzt
werden können.

**Abstract.**
We consider different ways of combining discrete and timed condition/event
systems (CESs) in a modular, compositional way. In addition to the
interconnection operators for CESs found in the literature, we introduce a new,
powerful operator, called parallel interconnection operator, which allows
arbitrary connections among a set of CESs. An extensive example shows various
possibilities how to verify properties of a system consisting of some
interconnected CESs. We conclude this work by showing how a set of
interconnected discrete CESs can be transformed into the input language of the
model checking tool SMV. This offers another possibility to apply formal
verification to condition/event systems.

Ben Lukoschus.

**An Abstract Model of VHS Case Study 1 (Experimental Batch Plant).**

*Technical Report TR-ST-99-2,*
Chair of Software Technology,
Institute of Computer Science and Applied Mathematics,
Christian-Albrechts-University of Kiel, May 1999.

**Abstract.**
In this work we describe the verification of safety properties for the
experimental batch plant of case study 1 using the model checker SMV. Discrete
condition/event systems are used to describe the physical parts of the plant
and the control programs. This model is transformed into SMV code, and the
properties are checked.

**Abstract.**
In this paper, several aspects of the composition of discrete
state condition/event systems according to Sreenivas and
Krogh are discussed. We introduce a new composition operator
called parallel interconnection. It is shown to be a
generalization of the originally defined cascade and feedback
operators. Based on this composition operator, a modular
refinement rule is presented which can be used to prove that
a parallel interconnection of condition/event systems refines
a given other one.

Ben Lukoschus.

**Komposition von Bedingung-/Ereignissystemen und deren
Echtzeitvarianten.**

**(Composition of Condition/Event Systems and Their Real-Time Variants)
**

*Diplomarbeit (Master's thesis),*
Christian-Albrechts-Universität zu Kiel, August 1998.

(German title, but English text.)

**Abstract.**
We consider different ways of combining discrete and timed
condition/event systems (CESs) in a modular, compositional
way. In addition to the interconnection operators for CESs
found in the literature, we introduce a new, powerful
operator, called parallel interconnection operator, which
allows arbitrary connections among a set of CESs. An
extensive example shows various possibilities how to verify
properties of a system consisting of some interconnected
CESs.

[gzip-compressed DVI] [gzip-compressed PostScript]

Ralf Huuck, Yassine Lakhnech, Ben Lukoschus, Luis Urbina, Sebastian Engell,
Stefan Kowalewski, Jörg Preußig.

**Integrating Timed Condition/Event Systems and Timed Automata for the
Verification of Hybrid Systems.**

*Parallel and Distributed Computing Practices,*
1(2):45-60, Commack, New York, June 1998. Nova Science Publishers, Inc.
ISSN 1097-2803.

Also published in:
Lonnie R. Welch and Dieter K. Hammer (eds.),
*Engineering of Distributed Control Systems,* pages 59-80.
Nova Science Publishers, Inc., 2001. ISBN 1-69033102-8.

**Abstract.**
In this paper we integrate two different approaches for the
specification and verification of timed systems being used in
control theory and computer science. These are the timed
condition/event systems and the timed automata formalisms.
Our main result states that timed condition/event systems can
be efficiently transformed into timed automata which then can
be analyzed automatically.

Stefan Kowalewski, Sebastian Engell, Ralf Huuck, Yassine Lakhnech, Ben
Lukoschus, Luis Urbina.

**Using Model-Checking for Timed Automata to Parameterize Logic Control
Programs.**

*ESCAPE 8: 8th European Symposium on Computer Aided Process Engineering,*
Brugge, Belgium, May 24-27, 1998, volume 22 (issue 1001) of
*Computers & Chemical Engineering,* pages S875-S878.
Elsevier Science, 1998.

**Abstract.**
In this contribution we describe how the modeling and
analysis framework of Timed Automata can be used to determine
valid parameter ranges for timers in logic control programs.
The procedure is illustrated by means of a simple process
engineering example for which the complete Timed Automata
model is presented. To analyse the model, the tool HyTech is
used which provides routines to determine values of model
parameters depending on reachability conditions.

**Zusammenfassung.**
Der Beitrag beschreibt, wie aus zeitbewerteten
Bedingung/Ereignis-Systemen bestehende, modular aufgebaute
Modelle mit Hilfe von Werkzeugen für Echtzeitautomaten
automatisch analysiert werden können. Dies geschieht,
indem eine Übersetzungsvorschrift angewendet wird, die
einem zeitbewerteten Bedingung/Ereignis-System einen
Echtzeitautomaten mit äquivalentem Verhalten zuordnet. Der
Ansatz wird anhand des aus der Literatur bekannten
Bahnschranken-Beispiels illustriert. Als Werkzeug wird KRONOS
eingesetzt.

Ben Lukoschus (ben@lukoschus.de) Last modified: 2007-04-06 23:43:16 CEST (+0200)