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)