Safe controllers design for industrial automation systems

Abstract

The design of safe industrial controllers is one of the most important domains related to Automation Systems research. To support it, synthesis and analysis techniques are available. Among the analysis techniques, two of the most important are Simulation and Formal Verification. In this paper these two techniques are used together in a complementary way. Understanding plant behaviour is essential for obtaining safe industrial systems controllers; hence, plant modelling is crucial to the success of these techniques. A two step approach is presented: first, the use of Simulation and, second, the use of Formal Verification of Industrial Systems Specifications. The specification and plant models used for each technique are described. Simulation and Formal Verification results are presented and discussed. The approach presented in the paper can be applied to real industrial systems, and obtain safe controllers for hybrid plants. The Modelica modelling language and Dymola simulation environment are used for Simulation purposes, and Timed Automata formalism and the UPPAAL real-time model-checker are used for Formal Verification purposes.

Introduction

Modern engineered systems have reached a high degree of complexity that requires systematic design methodologies, and model-based approaches to ensure correct and competitive performance. Regarding the use of software controlled devices such as digital controllers, evidence shows that small errors in their design may lead to catastrophic failures (Leveson and Turner, 1993, Nuseibeh, 1997).

Recent years have witnessed a significant growth of interest in the Modelling, Simulation and Formal Verification of physical systems (Schnakenbourg, Faure, & Lesage, 2002). A key factor in this growth was the development of efficient equation-based simulation languages, and formalisms and tools able to deal with the combinatorial explosion of discrete/timed/hybrid systems states.

Safety control has, as its main goal, the assurance of the reliability, availability, and maintainability requirements of automation systems. Because of its direct impact on people and goods safety, the reliability of critical systems (transports, space, nuclear, among others) has been mobilizing the scientific community’s efforts. Assuring system safety, demands the use of a global approach, guaranteeing that weaknesses do not exist. This approach must take into account, first the set of engineering activities used during development, and later, the set of activities of operational exploitation and maintenance. Thus, there is a continuous effort to develop methods and tools enabling the anticipation of possible malfunctioning, and to study how these different methods and tools might complement each other in the context of such a global approach.

Among the several techniques for analysis of industrial controllers: Identification (Klein, Litz, & Lesage, 2005), Simulation (Baresi, Mauri, Monti, & Pezzè, 2000), Formal Verification (Moon, 1994), Model-Based Testing (Cristiá & Monetti, 2009), and Diagnosis (Cabasino, Giua, & Seatzu, 2009); Simulation and Formal Verification are distinguished, by their utility. In the literature on industrial controller’s analysis, these two techniques are rarely used simultaneously. If Simulation is faster to execute, it has the limitation of considering only a subset of all the system behaviour evolution scenarios. Using Formal Verification has the advantage of analyzing all the possible evolution scenarios but it presents some limitations on the dimension and complexity of the models that can be analyzed. Such limitations arise due to the time and computational resources that become necessary for the attainment of Formal Verification results for very large models. This paper shows how it is possible, and desirable, to conciliate these two techniques in the analysis of industrial controllers. With the simultaneous use of these two techniques, the developed industrial controllers are more robust and not subject to errors. This paper is focused on the Formal Verification of real-time systems and considers also important aspects on the plant modelling tasks. The modelling of the plant is crucial for the development of safe controllers (Yalcin & Namballa, 2005).

There are several approaches to applying Formal Verification techniques on automation systems dependability: from Formal Verification by theorem proving (Roussel & Denis, 2002) to Formal Verification by model-checking (Rossi, 2004); and considering (Machado, Denis, & Lesage, 2006a), or not (Rossi, 2004), a plant model. The above approaches, however, do not consider timed aspects. In the Formal Verification of timed systems, several approaches can be used to increase the quality of the verification results. A distinction can be made between the work by Remelhe, Lohmann, Stursberg, and Engell (2004), where the translation of IEC 61131-3 Sequential Function Charts (SFC) into timed automata (Alur & Dill, 1990) is studied, and the work developed by Gaid, Bérard, and Smet (2005) where an approach for constructing the controller model is proposed. This latter work uses the initial approach proposed by Mader and Wupper (1999), and some work hypotheses related to the evolution of the controller model and time aspects, in order to increase the quality of Formal Verification results. In the present work the base system and the work hypothesis considered by Gaid et al. (2005) for the controller behaviour are adopted, and an approach to build timed plant models is proposed.

The paper is organized in eight sections. Section 1 presents the challenge being addressed in this work. Section 2 presents an overview of the most used analysis techniques for Industrial Controllers design, with special focus on Simulation and Formal Verification. Section 3 presents our proposal for the analysis of controllers design based on the complementary use of Simulation and Formal Verification. Section 4 is devoted to the presentation of a case study, involving a system with two tanks, a heating device, level control sensors, and valves to control the liquids’ flow. Section 5 is entirely devoted to plant modelling. Next, in Section 6, a set of properties over system’s behaviour is provided, as well as their formalization in Timed Computation Tree Logic (TCTL). Section 7 presents and discusses the results obtained from Simulation and Formal Verification of the case study’s specification. Finally, Section 8 presents the conclusions and future work.