@InCollection{BHLE04, author = {Nanette Bauer and Ralf Huuck and Ben Lukoschus and Sebastian Engell}, title = {A Unifying Semantics for Sequential Function Charts}, booktitle = {Integration of Software Specification Techniques for Application in Engineering}, publisher = {Springer-Verlag}, editor = {Hartmut Ehrig and Werner Damm and J\"org Desel and Martin Gro{\ss}e-Rhode and Wolfgang Reif and Eckehard Schnieder and Engelbert Westk\"amper}, volume = 3147, year = 2004, pages = {400--418}, series = {Lecture Notes in Computer Science}, 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.} } @InCollection{BEHLLRS04, author = {Nanette Bauer and Sebastian Engell and Ralf Huuck and Sven Lohmann and Ben Lukoschus and Manuel Remelhe and Olaf Stursberg}, title = {Verification of {PLC} Programs given as Sequential Function Charts}, booktitle = {Integration of Software Specification Techniques for Application in Engineering}, publisher = {Springer-Verlag}, editor = {Hartmut Ehrig and Werner Damm and J\"org Desel and Martin Gro{\ss}e-Rhode and Wolfgang Reif and Eckehard Schnieder and Engelbert Westk\"amper}, volume = 3147, year = 2004, pages = {517--540}, series = {Lecture Notes in Computer Science}, keywords = {Analysis, Automata, Model Checking, Logic Control}, 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.} } @Article{BHLL04, author = {Nanette Bauer and Ralf Huuck and Sven Lohmann and Ben Lukoschus}, title = {{Sequential Function Charts: Die Notwendigkeit formaler Analyse}}, journal = {atp -- Automatisierungstechnische Praxis}, year = 2004, month = aug, keywords = {Sequential Function Charts, IEC 61131-3, Semantics, Verification, Model-Checking}, abstract = {The international standard IEC 61131-3 defines the coordination and programming language Sequential Function Charts (SFCs) for programmable logic controllers (PLCs). The standard however defines the SFC semantics in natural and informal language, which tends to be ambiguous and partly incomplete. We show that in consequence PLC development tools of different manufacturers implement slightly different technical realizations of the standard such that issues of functionality and portability are questionable. This article points out some of these ambiguities and suggests programming methods to ensure the desired functionality. Furthermore we present a formal analysis approach for SFCs which, unlike traditional testing methods, provides automatic verification of program properties.}, schlagwoerter = {Sequential Function Charts, IEC 61131-3, Semantik, Verifikation, Model-Checking}, zusammenfassung = {Sequential Function Charts (SFCs, im Deutschen auch als Ablaufsprache bezeichnet), stellen eine in der Norm IEC 61131-3 definierte Koordinations- und Programmiersprache f\"ur speicherprogrammierbare Steuerungen (SPS) dar. Gerade f\"ur 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\"age zur Umgehung von Mehrdeutigkeiten. Au\ss{}erdem wird ein Ansatz zur formalen Analyse von SFCs vorgestellt, der im Gegensatz zu herk\"ommlichen Testverfahren eine weitgehend automatisierte Verifikation von Programmeigenschaften erm\"oglicht.} } @InProceedings{HLB03, author = {Ralf Huuck and Ben Lukoschus and Nanette Bauer}, title = {A Model-Checking Approach to Safe {SFCs}}, booktitle = {CESA 2003: IMACS Multiconference on Computational Engineering in Systems Applications, Lille, France, July 9--11, 2003}, editor = {Pierre Borne and Etienne Craye and Nathalie Dangoumau}, year = 2003, isbn = {2-9512309-5-8}, 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 \emph{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.} } @InCollection{HLFE02, author = {Ralf Huuck and Ben Lukoschus and Goran Frehse and Sebastian Engell}, title = {Compositional Verification of Continuous-Discrete Systems}, booktitle = {Modelling, Analysis and Design of Hybrid Systems}, pages = {225--246}, publisher = {Springer-Verlag}, month = jan, year = 2002, editor = {S. Engell and G. Frehse and E. Schnieder}, volume = 279, series = {Lecture Notes in Control and Information Sciences}, issn = {0170-8643}, isbn = {3-540-43812-2}, 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.} } @InProceedings{BHL02, author = {Nanette Bauer and Ralf Huuck and Ben Lukoschus}, title = {A Stopwatch Semantics for Hybrid Controllers}, booktitle = {b '02: The XV. IFAC World Congress, Barcelona, Spain, July 21--26, 2002}, year = 2002, keywords = {Programmable Logic Controllers, Linear Hybrid Systems, Sequential Function Charts, Stopwatch Semantics}, 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.} } @InProceedings{FSEHL02, author = {Goran Frehse and Olaf Stursberg and Sebastian Engell and Ralf Huuck and Ben Lukoschus}, title = {Modular Analysis of Discrete Controllers for Distributed Hybrid Systems}, booktitle = {b '02: The XV. IFAC World Congress, Barcelona, Spain, July 21--26, 2002}, year = 2002, keywords = {Abstraction, Assumption/Commitment, Discrete Controllers, Model Checking, Verification}, 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 \textit{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.} } @InProceedings{FSEHL01, author = {Goran F. Frehse and Olaf Stursberg and Sebastian Engell and Ralf Huuck and Ben Lukoschus}, title = {Verification of Hybrid Controlled Processing Systems based on Decomposition and Deduction}, booktitle = {ISIC 2001: 2001 IEEE International Symposium on Intelligent Control, Mexico City, Mexico, September 5--7, 2001}, year = 2001, pages = {150--155}, organization = {IEEE Control Systems Society}, publisher = {IEEE Press}, isbn = {0-7803-6733-2 (CD-ROM: 0-7803-6735-9)}, keywords = {Abstraction, Assumption/Commitment, Deductive Analysis, Discrete Controller, Hybrid System, Verification}, 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.} } @Article{HLL01, author = {Ralf Huuck and Ben Lukoschus and Yassine Lakhnech}, title = {Verifying Untimed and Timed Aspects of the Experimental Batch Plant}, journal = {European Journal of Control}, editor = {Oded Maler}, year = 2001, volume = 7, number = 4, pages = {400--415}, month = sep, note = {Special Issue: Verification of Hybrid Systems -- Results of a European Union Esprit Project}, organization = {The European Union Control Association}, publisher = {Hermes Science Publishing}, issn = {0947-3580}, keywords = {Controller synthesis, Hybrid Systems, 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.} } @Article{KHEKTLHL01, author = {Stefan Kowalewski and Peter Herrmann and Sebastian Engell and Ralf Huuck and Heiko Krumm and Yassine Lakhnech and Ben Lukoschus and Heinz Treseler}, title = {Approaches to the Formal Verification of Hybrid Systems}, journal = {at Automatisierungstechnik}, publisher = {Oldenbourg Verlag}, volume = 49, number = 2, month = feb, year = 2001, pages = {66--74}, issn = {0178-2312}, note = {Special Issue: Hybrid Systems II: Analysis, Modeling, and Verification}, 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.} } @InProceedings{BHLL00:ADPM, author = {S{\'e}bastien Bornot and Ralf Huuck and Yassine Lakhnech and Ben Lukoschus}, title = {Utilizing Static Analysis for Programmable Logic Controllers}, booktitle = {ADPM 2000: The 4th International Conference on Automation of Mixed Processes: Hybrid Dynamic Systems, Dortmund, Germany, September 18--19, 2000}, pages = {183--187}, year = 2000, editor = {Sebastian Engell and Stefan Kowalewski and Janan Zaytoon}, series = {Berichte aus der Automatisierungstechnik}, address = {Aachen, Germany}, organization = {Universit{\"a}t Dortmund, Lehrstuhl Anlagensteuerungstechnik}, publisher = {Shaker Verlag}, issn = {0945-4659}, isbn = {3-8265-7836-8}, 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.} } @InProceedings{BHLL00:WODES, author = {S{\'e}bastien Bornot and Ralf Huuck and Yassine Lakhnech and Ben Lukoschus}, title = {An Abstract Model for Sequential Function Charts}, booktitle = {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}, year = 2000, editor = {Ren{\'e} Boel and Geert Stremersch}, series = {The Kluwer International Series in Engineering and Computer Science}, address = {Boston, Dordrecht, London}, publisher = {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.} } @InProceedings{BHLL00:PDPTA, author = {S{\'e}bastien Bornot and Ralf Huuck and Yassine Lakhnech and Ben Lukoschus}, title = {Verification of Sequential Function Charts using {SMV}}, booktitle = {PDPTA 2000: International Conference on Parallel and Distributed Processing Techniques and Applications, Monte Carlo Resort, Las Vegas, Nevada, USA, June 26--29, 2000}, pages = {2987--2993}, year = 2000, editor = {Hamid R. Arabnia}, volume = {V}, month = jun, publisher = {CSREA Press}, 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).} } @InProceedings{BHL00, author = {S{\'e}bastien Bornot and Ralf Huuck and Ben Lukoschus}, title = {{Statische Analysetechniken f{\"u}r speicherprogrammierbare Steuerungen}}, booktitle = {FBT 2000: 10. GI/ITG-Fachgespr{\"a}ch: Formale Beschreibungstechniken f{\"u}r verteilte Systeme, L{\"u}beck, Germany, June 22--23, 2000}, pages = {175--181}, year = 2000, editor = {Jens Grabowski and Stefan Heymer}, series = {Berichte aus der Informatik}, address = {Aachen, Germany}, month = jun, publisher = {Shaker Verlag}, issn = {0945-0807}, isbn = {3-8265-7491-5}, abstract = {Speicherprogrammierbare Steuerungen (SPS) unterliegen einer stark zunehmenden Verbreitung in der Automatisierungstechnik. W{\"a}hrend diese in der Vergangenheit meist nur zur Steuerung einfacher Abl{\"a}ufe eingesetzt wurden, sind sie heutzutage verantwortlich f{\"u}r die Steuerung komplexer hybrider Systeme, sei es in der petrochemischen Industrie oder in Kraftwerken. Daher ist eine korrekt funktionierende Steuerungssoftware von grunds{\"a}tzlicher Bedeutung. In diesem Vortrag wird die Methode der statischen Analyse f{\"u}r eine standardisierte SPS-Sprache, Anweisungsliste (AWL), vorgestellt. Statische Analyse umfa{\ss}t Techniken, die Laufzeitverhalten ermitteln bzw. nachweisen, ohne den Code selbst auszuf{\"u}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{\"u}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\"onnen.} } @TechReport{Lukoschus99:cs1, author = {Ben Lukoschus}, title = {An Abstract Model of {VHS} Case Study 1 (Experimental Batch Plant)}, institution = {Chair of Software Technology, Institute of Computer Science and Applied Mathematics, Christian-Albrechts-University of Kiel}, year = 1999, number = {TR-ST-99-2}, month = may, 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.} } @TechReport{Lukoschus99:ces, author = {Ben Lukoschus}, title = {Composition and Verification of Condition/Event Systems}, institution = {Chair of Software Technology, Institute of Computer Science and Applied Mathematics, Christian-Albrechts-University of Kiel}, year = 1999, number = {TR-ST-99-1}, month = may, 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.} } @InProceedings{KLLU98, author = {Stefan Kowalewski and Yassine Lakhnech and Ben Lukoschus and Luis Urbina}, title = {On the Composition of Condition/Event Systems}, booktitle = {WODES '98: 4th International Workshop on Discrete Event Systems, Cagliari, Italy, August 26--28, 1998}, pages = {349--354}, year = 1998, address = {London}, organization = {IEE}, publisher = {IEE Publishing}, keywords = {condition/event systems, composition, modularity, refinement}, 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.} } @MastersThesis{Lukoschus98, author = {Ben Lukoschus}, title = {{Komposition von Bedingung-/Ereignissystemen und deren Echtzeitvarianten}}, school = {Christian-Albrechts-Universit{\"a}t zu Kiel}, year = 1998, type = {{Diplomarbeit (Master's thesis)}}, month = aug, note = {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.} } @Article{HLLUEKP98, author = {Ralf Huuck and Yassine Lakhnech and Ben Lukoschus and Luis Urbina and Sebastian Engell and Stefan Kowalewski and J\"org Preu{\ss}ig}, title = {Integrating Timed Condition/Event Systems and Timed Automata for the Verification of Hybrid Systems}, journal = {Parallel and Distributed Computing Practices}, year = 1998, month = jun, editor = {Lonnie R. Welch and Dieter K. Hammer}, volume = 1, number = 2, pages = {45--60}, publisher = {Nova Science Publishers, Inc.}, address = {Commack, New York}, issn = {1097-2803}, note = {Special Issue on Engineering of Distributed Control Systems. Also published in \cite[pp. 59--80]{WH01}.}, 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.} } @Book{WH01, editor = {Lonnie R. Welch and Dieter K. Hammer}, title = {Engineering of Distributed Control Systems}, publisher = {Nova Science Publishers, Inc.}, year = 2001, address = {Huntington, New York}, isbn = {1-69033102-8} } @InProceedings{KEHLLU98, author = {Stefan Kowalewski and Sebastian Engell and Ralf Huuck and Yassine Lakhnech and Ben Lukoschus and Luis Urbina}, title = {Using Model-Checking for Timed Automata to Parameterize Logic Control Programs}, booktitle = {ESCAPE 8: 8th European Symposium on Computer Aided Process Engineering, Brugge, Belgium, May 24--27, 1998}, series = {Computers \& Chemical Engineering}, volume = {22 (issue 1001)}, pages = {S875--S878}, year = 1998, publisher = {Elsevier Science}, keywords = {Programmable Logic Controllers, process safety, validation, Timed Automata, HyTech}, 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.} } @InProceedings{KPEHLL97, author = {Stefan Kowalewski and J{\"o}rg Preu{\ss}ig and Sebastian Engell and Ralf Huuck and Yassine Lakhnech and Ben Lukoschus}, title = {{Analyse zeitbewerteter Bedingung/Ereignis-Systeme mittels Echtzeitautomaten-Tools}}, booktitle = {EKA '97: 5. Fachtagung Entwurf komplexer Automatisierungssysteme, Braunschweig, Germany, May 1997}, year = 1997, pages = {180--194}, volume = 1, keywords = {Analyse von Echtzeitsystemen, Bedingung/Ereignis-Systeme, Echtzeitautomaten, KRONOS}, abstract = {Der Beitrag beschreibt, wie aus zeitbewerteten Bedingung/Ereignis-Systemen bestehende, modular aufgebaute Modelle mit Hilfe von Werkzeugen f\"ur Echtzeitautomaten automatisch analysiert werden k\"onnen. Dies geschieht, indem eine \"Ubersetzungsvorschrift angewendet wird, die einem zeitbewerteten Bedingung/Ereignis-System einen Echtzeitautomaten mit \"aquivalentem Verhalten zuordnet. Der Ansatz wird anhand des aus der Literatur bekannten Bahnschranken-Beispiels illustriert. Als Werkzeug wird KRONOS eingesetzt.} }