Abstract. In this work we introduce counterexample guided path reduction based on interval constraint solving for static program analysis. The aim of this technique is to reduce the number of false positives by reducing the number of feasible paths in the abstraction iteratively. Given a counterexample, a set of observers is computed which exclude infeasible paths in the next iteration. This approach combines ideas from counterexample guided abstraction refinement for software verification with static analysis techniques that employ interval constraint solving. The advantage is that the analysis becomes less conservative than static analysis, while it benefits from the fact that interval constraint solving deals naturally with loops. We demonstrate that the proposed approach is effective in reducing the number of false positives, and compare it to other static checkers for C/C++ program analysis.

Paper: [PDF file]

2007

Abstract. The verification of real-life C/C++ code is inherently hard. Not only are there numerous challenging language constructs, but the precise semantics is often elusive or at best vague. This is even more true for systems software where non-ANSI compliant constructs are used, hardware is addressed directly and assembly code is embedded. In this work we present a lightweight solution to detect software bugs in C/C++ code. Our approach performs static checking on C/C++ code by means of model checking. While it cannot guarantee full functional correctness, it can be a valuable tool to increase the reliability and trustworthiness of real-life system code. This paper explains the general concepts of our approach, discusses its implementation in our C/C++ checking tool Goanna, and presents some performance results on large software packages.

Extended Abstract: [PDF file]

Abstract. Software has been under scrutiny by the verification community from various angles in the recent past. There are two major algorithmic approaches to ensure the correctness of and to eliminate bugs from such systems: software model checking and static analysis. Those approaches are typically complementary. In this paper we use a model checking approach to solve static analysis problems. This not only avoids the scalability and abstraction issues typically associated with model checking, it allows for specifying new properties in a concise and elegant way, scales well to large code bases, and the built-in optimizations of modern model checkers enable scalability also in terms of numbers of properties to be checked. In particular, we present Goanna, the first C/C++ static source code analyzer using the off-the-shelf model checker NuSMV, and we demonstrate Goanna’s suitability for developer machines by evaluating its run-time performance, memory consumption and scalability using the source code of OpenSSL as a test bed.

Paper: [PDF file]

2006

Abstract. In this work we present Goanna, the first tool that uses an off-the-shelf model checker for the static analysis of C/C++ source code. We outline its architecture and show how syntactic properties can be expressed in CTL. Once the properties have been defined the tool analyses source code automatically and efficiently. We demonstrate its applicability by presenting experimental results on analysing OpenSSL and the GNU coreutils.

Paper: [PDF file]

2005

Abstract. Automotive components present unique challenges in reliability, security, performance and cost. Consolidation of different functions in multi-purpose units drives up complexity, and raises not only reliability concerns, but also the issue of liability for sub-component suppliers. It is of foremost importance to guarantee reliability and security right from the start when designing such systems. In this work we present a complete approach grounded in a flexible and secure microkernel, supported by a flexible operating system and component architecture on top. This is coupled with rigorous software development to assure the reliability and security.

Paper: [PDF file]

Abstract. This paper describes an approach to developing high assurance system software. We demonstrate how different formal methods can be applied in the development process by matching specific techniques and tools to the different levels of system requirements and how those techniques can complement each other.
Keywords. System software, kernel design, theorem proving, static analysis.

Abstract. Instruction List (IL) is a simple typed assembly language commonly used in embedded control. There is little tool support for IL and, although defined in the IEC 61131-3 standard, there is no formal semantics. In this work we develop a formal operational semantics. Moreover, we present an abstract semantics, which allows approximative program simulation for a (possibly infinte) set of inputs in one simulation run. We also extended this framework to an abstract interpretation based analysis, which is implemented in our tool Homer. All these analyses can be carried out without knowledge of formal methods, which is typically not present in the IL community.

Paper: [PDF file]

2004

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.

Paper: [Link to Electronic Version]

Abstract. Programmable Logic Controllers (PLC) are widespread in the manufacturing and processing industries to realize sequential procedures and to avoid safety-critical behavior. For the specification and implementation of PLC programs, the graphical and hierarchical language Sequential Function Charts (SFC) has an increasing importance. To investigate the correctness of SFC programs with respect to a given set of requirements, this contribution advocates the use of verification techniques. In detail, we present two different approaches to algorithmically convert the SFC program 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. Using the example of a controlled chemical processing system, we illustrate the complete procedure consisting of controller specification, model transformation, consideration of plant models, and identifying design failures by the use of verification.

Paper: [Link to Electronic Version]

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.

2003

Abstract. Programmable logic controllers (PLCs) occupy a big share in automation control. Their programming languages are, however, born out of historical needs and do not comply to state-of-the art programming concepts. Moreover, programming is mostly undertaken by the designers of the control systems. In sum this adds to the creation of erroneous software and, even more, unsafe control systems. In this work we focus on the software verification aspects for PLCs. For two selected programming languages, Sequential Function Charts (SFC) and Instruction List (IL) we discuss semantic issues as well as verification approaches. For SFCs we develop a model checking framework while for IL we suggest static analysis techniques, i.e., a combination of data flow analysis and abstract interpretation. Several case studies corrobate our approach.
Keywords. Software Verification, Programmable Logic Controllers, Sequential Function Charts, Instruction List, Model-checking, Abstract interpretation, Data Flow Analysis, Embedded Systems, Control Systems, Semantics

Electronic Version [PDF file]

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 file]

2002

Abstract. Embedded systems have the characteristics of reactive, real-time, distributed systems. For these kind of systems formal verification is by nature complex, even more since the system interaction with its environment is often modeled, e.g., as hybrid systems. However, every embedded control system will certainly fail, if its software fails. In this work we present an approach to the formal verification of Programmable Logic Controller (PLC) software. We present a tool that translates PLC programs written in the language Sequential Function Charts automatically into an abstract model that can be read by a standard model checker. Moreover, we demonstrate its effectiveness by an application to a sorting plant and show that software verification can indeed contribute to system reliability.

[PDF file]

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.

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 standard model checking.

[PDF file]

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 ambiguously and not completely defined. 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.

[ gzip-compressed PostScript]

Abstract. The language Sequential Function Charts (SFC) is one of the five programmable logic controller (PLC) languages defined in the IEC 61131-3 standard. It includes many interesting concepts such as parallelism, hierarchy, priorities, and activity manipulation. However, the standard only gives an informal ambiguous semantics for SFCs, which leads to the implementation of different SFC semantics by PLC tool vendors. The validation and analysis of a given SFC is therefore difficult. This work addresses this point by presenting a formal parameterized semantics coping with the different concepts as well as unifying the various interpretations.

[ gzip-compressed PostScript]

2001

Abstract. The language sequential function charts (SFC) is a programming and structuring language for programmable logic controllers (PLC). It is defined in the IEC 61131-3 standard and includes various interesting concepts such as parallelism, hierarchy, priorities, and activity manipulation. Although SFCs are perpetually used in the engineering community for programming and the design of embedded control systems, there are hardly any specific verification approaches for them. Existing approaches for Petri Nets, Grafcets, or (UML-)Statecharts do not really apply to SFCs, whose structures are similar, but include distinct features. In this work we present a method to model-check SFCs. This is done by defining a translation of SFCs into the native language of the Cadence Symbolic Model Verifier (CaSMV). This translation is specifically tailored to cover all the concepts of SFCs and can be performed automatically. Moreover, we demonstrate our approach by an application to a control process in chemical engineering.

[gzip-compressed PostScript]

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.

[gzip-compressed PostScript]

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.

[gzip-compressed PostScript]

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.

[gzip-compressed PostScript]

2000

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.

[gzip-compressed PostScript]

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.

[gzip-compressed PostScript]

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

[gzip-compressed PostScript]

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.

[gzip-compressed PostScript]

1998

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.

[gzip-compressed PostScript]

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.

[gzip-compressed PostScript]

Abstract. We thoroughly investigate the relationship between timed condition/event systems and timed automata. One result is an effective function mapping to each timed condition/event system an "equivalent" timed automaton, i.e., a timed automaton which has essentially the same real-time behaviors. A benefit from providing such a function is that analysis tools developed for timed automata can now be applied to analyze timed c/e systems. Moreover, we provide another effective function mapping to each timed i/o automaton a timed condition/event system.

[gzip-compressed PostScript]

1997

Abstract. We investigate the relationship between timed c/e systems and timed automata. We provide an effective function that associates to each timed c/e system an "equivalent" timed automaton. Equivalence has to be understood here as describing essentially the same real-time behaviors. A benefit from providing such a function is that analysis tools developed for timed automata can now be applied to analyze timed c/e systems. We also prove that timed automata can be translated into equivalent timed c/e systems.

[ gzip-compressed PostScript]

Abstract. We report on the project "Specification and Verification of Discrete Controllers for Continuous Systems Based on Modular Models and Compositional Analysis". Within this project we aim at developing an automatic verification tool for discrete controllers of technical systems which can be applied to systems of industrial size. To reach this objec tive we combine two different approaches being used in control theory and computer science. These are the "Timed Condition/Event Systems" (TCESs) and the "Timed Automata" (TAs) formalisms. The state of the project is such that, because of the equivalence of TCESs and TAs we have shown in, it is possible to automatically analyze real-time syste ms modeled by TCESs with analysis tools developed for TAs. In this paper we desc ribe in detail motivation, goal and state of our project, and illustrate the equ ivalence of TCESs and TAs.

[ gzip-compressed PostScript]

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.

[gzip-compressed PostScript]