Induction-based Verification of Timed Systems / vorgelegt von Tobias Isenberg, M.Sc.

Induction-based Verification of Timed Systems Dissertation zur Erlangung des akademischen Grades eines Doktors der Naturwissenschaften an der Fakultät für Elektrotechnik, Informatik und Mathematik der Universität Paderborn vorgelegt von Tobias Isenberg, M.Sc. Paderborn, Februar 2016 iii Abstract Computer controlled systems are a foundation to today’s modern society. Their use and impact are ever-growing, in particular when considering trends like smart homes and Industry 4.0. The development of such systems is non-trivial. Correctness of the functionality provided by these systems is of importance, since they are often deployed in safety-critical scenarios, where a failure could lead to a loss in production value or the risk of life. Many of these systems are real-time systems or include some kind of timed behavior. In order to ensure a certain quality of these systems, model-based design approaches can be employed. Within these structured procedures, the systems under development are designed using models that specify certain aspects of them. This structured procedure provides for fewer errors being made. In combination with formal methods, the absence of erroneous behavior can be ensured. To this end, formal languages with a mathematically defined semantics are employed, and formal verification, based on this semantics, is used to reason about the absence of erroneous behavior. There exist several formalisms for the verification of timed systems, e.g., the formalism of networks of timed automata used in this thesis. However, today’s techniques and tools for this task often suffer from the same deficiency. They easily run out of memory when exploring large, complex models due to the enormous amount of states (state explosion problem) they need to keep track of. An additional challenge arises when considering the procedure during the design phase. The models are repeatedly reconfigured, i.e., changed to reflect design choices until a final design is found. In addition, they may also be reconfigured during lifetime, in particular when considering systems of Industry 4.0 that are self-optimizing and adaptable. In consequence, the respective models are reconfigured to reflect these adaptations. These reconfigurations raise the need to redo verifications since the state spaces of the models might have changed. Techniques employed for these redone verifications have to meet specific demands, in particular efficiency, since they might be employed in a sort of online verification during the lifetime of a system. In this thesis, we approach both of the challenges mentioned above. First, we provide a technique for the verification of safety properties specifying the absence of erroneous behavior for networks of timed automata. Our technique deliberately works distinct from other state-of-the-art approaches in this field, as it employs induction and, thus, avoids explicit exploration and storage of states. In consequence, it is a valuable complement to existing technologies as its strengths and weaknesses differ to those of other technologies. Our approach combines the IC3 algorithm, well known in the hardware verification domain, with the Zone abstraction, used for timed verification. The result, IC3 with Zones is competitive and includes the strengths of both components, namely the time abstracting efficiency of zones and the efficiency on discrete structured of IC3. We show the practicality of it in numerous experiments on different aspects of scalability. In our continued work, we employ our algorithm for the verification of reconfigured models. To this end, we reuse an inductive invariant computed by IC3 with Zones. iv This basic idea works particularly well for a special class of systems, denoted Parameterized Timed Systems. They contain an arbitrary, but fixed number of instances of a process as is the case, e.g., in client-server settings with an arbitrary number of clients. We propose an approach to avoid the online verification for such systems, as would be needed whenever the number of processes is changed, e.g., a client is added. Our technique enables an a priori verification of the entire system, irrespective of the actual number of instances. To this end, we verify the safety property for the smaller models of the family and reuse the computed inductive invariants. These are adapted using the symmetry inherent in Parameterized Timed Systems, and employed for the reasoning about the entire system. For this purpose, we propose and prove a Termination Theorem that enables this reasoning. The practicality of our approach is shown using several experiments. In addition, we examine the reusability of the inductive invariant for general models and reconfigurations with the aim to speed up the verification for reconfigured models. To this end, the same acceleration technique is employed as in the special case for Parameterized Timed Systems. We discuss in detail, why it is hardly feasible to adapt the inductive invariant to reflect a reconfiguration in general. As a result, we give a best-guess approach that adapts the invariant where possible. Numerous experiments show that this technique is of value even so, in particular when the reconfigurations are small. v Zusammenfassung Rechnergesteuerte Systeme bilden den Grundstein der heutigen Gesellschaft. Ihr Einsatz und ihre Verbreitung wachsen stetig, unterstützt durch Trends wie Smart Homes und Industrie 4.0. Die Entwicklung solcher Systeme ist jedoch schwierig. Ihre korrekte Funktionalität ist von großer Wichtigkeit, da diese Systeme oftmals in sicherheitskritischen Szenarios eingesetzt werden, in denen eine Fehlfunktion zu finanziellem Schaden oder sogar zu Gefahr für Leib und Leben führen kann. Viele dieser Systeme sind Echtzeitsysteme oder besitzen zeitgesteuertes Verhalten. Um die Qualität der Systeme sicherzustellen, können Modell-basierte Design- Ansätze verwendet werden. In diesen strukturierten Vorgehensweisen werden die zu erstellenden Systeme mithilfe von Modellen entworfen, die ein System unter bestimmten Gesichtspunkten spezifizieren. Ein solch strukturierter Ansatz sorgt dafür, dass weniger Fehler gemacht werden. Durch die zusätzliche Nutzung formaler Methoden kann die Abwesenheit von fehlerhaftem Verhalten sichergestellt werden. Hierzu werden formale Sprachen mit mathematisch definierter Semantik genutzt, sowie formale Verifikation, die basierend auf der formalen Semantik über die Abwesenheit von fehlerhaftem Verhalten schlussfolgert. Etliche Formalismen existieren für die Verwendung zur Verifikation zeitlicher Systeme, zum Beispiel die Netzwerke von zeitlichen Automaten, die in dieser Arbeit verwendet werden. Die meisten der heutigen Techniken für die Verifikation zeitlicher Systeme leiden jedoch unter dem gleichen Problem. Bei der Exploration großer, komplexer Modelle benötigen sie ein enormes Maß an Speicher, um die besuchten Zustände zu speichern. Durch das enorme Anwachsen der Anzahl an Zuständen (Zustandsexplosionsproblem) schlägt die Verifikation oft fehl. Eine zusätzliche Herausforderung entsteht durch den Ablauf der Design- Phase. Bis das finale Design entschieden ist, können die Modelle wiederholt rekonfiguriert, d.h. geändert, werden um Designentscheidungen umzusetzen. Zusätzlich kann dies auch zur Laufzeit der Systeme auftreten, insbesondere bei Systemen der Industrie 4.0, die selbstoptimierend und anpassungsfähig sind. Dementsprechend können sich die entsprechenden Modelle zur Laufzeit ändern. Diese Rekonfigurationen verlangen eine erneute Verifikation, da sich der Zustandsraum geändert haben kann. An die Techniken, die für diese erneuten Verifikationen eingesetzt werden, werden spezielle Anforderungen gestellt, insbesondere Effizienz, da sie während der Laufzeit als Online-Verifikationen durchgeführt werden. In dieser Arbeit werden beide zuvor genannten Herausforderungen angegangen. Es wird eine Technik zur Verifikation von Sicherheitseigenschaften, die die Abwesenheit von fehlerhaftem Verhalten definieren, in Netzwerken von zeitlichen Automaten vorgestellt. Diese Technik hat ein grundlegend anderes Funktionsprinzip als andere aktuelle Ansätze, da sie Induktion nutzt und somit die explizite Exploration und Speicherung von Zuständen umgeht. Hierdurch ist sie eine wertvolle Ergänzung zu den bestehenden Ansätzen, da die Stärken und Schwächen unterschiedlich ausfallen. Der Ansatz kombiniert den IC3 Algorithmus, der in der Hardware Verifikation erfolgreich eingesetzt wird, mit der Zonen-Abstraktion, die Grundlage vieler zeitlicher Verifikationsverfahren ist. Der resultierende Algorithmus IC3 mit Zonen ist wettbewerbsfähig und enthält vi Stärken von beiden genannten Komponenten. Dies sind insbesondere die gute Fähigkeit zur Zeit-Abstraktion von Zonen und die Effizienz auf diskreten Strukturen von IC3. Die Anwendbarkeit und Skalierbarkeit der Technik wird in vielen Experimenten gezeigt. Aufbauend auf dieser Technik werden Ansätze vorgestellt, die auf die Verifikation von rekonfigurierten Modellen abzielen. Sie nutzen dazu die induktive Invariante, die von IC3 mit Zonen berechnet wird. Die Idee der Wiederverwendung der Invariante ist besonders gut einsetzbar bei einer speziellen Art von Systemen, genannt Parametrisierte Zeitliche Systeme. Diese enthalten eine beliebige, aber feste Anzahl an Instanzen eines Prozesses, wie beispielsweise in einem Client-Server System mit beliebiger Anzahl Clients. Unser Ansatz umgeht die Notwendigkeit einer Online-Verifikation für solche Systeme, die beispielsweise notwendig wäre, wenn die Anzahl an Clients geändert würde. Die Technik basiert auf einer Verifikation der gesamten Familie an Modellen, die von vornherein ausgeführt wird. Hierzu wird die Sicherheitseigenschaft für die kleineren Modelle verifiziert. Die dabei berechneten induktiven Invarianten werden anhand der Symmetrie, die durch die Parametrisierung gegeben ist, angepasst und danach verwendet, um über die gesamte Familie an Modellen zu urteilen. Hierfür wird ein Terminierungstheorem gegeben und bewiesen. Etliche Experimente zeigen den Nutzen der Technik. Zusätzlich wird untersucht, wie man die induktiven Invarianten für allgemeine Rekonfigurationen und Modelle nutzen kann, so dass die Verifikation für rekonfigurierte Modelle schneller wird. Es werden die gleichen Techniken zur Beschleunigung von Verifikationen mithilfe der Invarianten benutzt, wie in der Arbeit zu parametrisierten Systemen. Detailliert wird dargelegt, warum diese Invarianten im allgemeinen Fall kaum an die Rekonfiguration angepasst werden können. Schließlich wird ein Ansatz vorgestellt, der die Invariante soweit wie möglich anpasst. Experimente zeigen, dass diese Technik eine Bereicherung im Kontext der Online-Verifikation darstellt. vii Acknowledgments Most importantly, I would like to express my sincere gratitude to my supervisor Prof. Dr. Heike Wehrheim for her guidance and support. The last three years have been a rewarding, interesting time and I am very thankful for the opportunity to work in her research group and to write my thesis. I also want to express my gratitude to my second supervisor Prof. Dr. Oliver Niggemann for his support. Sincere thanks go to Prof. Dr. Hans Kleine Büning, Jun.-Prof. Dr. Heiko Hamann and Dr. Theodor Lettmann for being part of my PhD committee. In addition, I want to thank all current and former members of the research group that have crossed my path: Steffen Beringer, Dr. Galina Besova, Marie- Christine Jakobs, Julia Krämer, Dr. Thomas Ruhroth, Elisabeth Schlatt, Alexander Schremmer, Dr. Dominik Steenken, Dr. Nils Timm, Manuel Töws, Oleg Travkin, Sven Walther and Steffen Ziegert. They provided for a pleasant atmosphere and a great time. Furthermore, I owe special gratitude to Dennis Wolters and Anna Lena Isenberg for proof reading parts of this thesis. Finally, I want to thank my parents, Werner and Ulrike Isenberg, for always encouraging me and providing, together with my twin brother Florian and my sister Anna Lena, for an amazing childhood that made me who I am. Last, but not least, I want to express my loving gratitude to my girlfriend Nadja. She knows how to make me smile and she has always been there to support me. Contents List of Figures xiii List of Tables xv 1 Introduction 1 1.1 ProblemDefinition .............................. 3 1.2 Contribution.................................. 5 1.3 ThesisOutline................................. 9 2 Background 11 2.1 TimedAutomata ............................... 11 2.1.1 Decidability and Abstractions . . . . . . . . . . . . . . . . . . . 19 2.1.2 Relatedwork ............................. 20 2.2 SAT-&SMT-Solving ............................. 23 2.2.1 SAT-Solving.............................. 23 2.2.2 SMT-Solving.............................. 24 2.3 Induction based Reasoning . . . . . . . . . . . . . . . . . . . . . . . . . 25 2.4 IC3 ....................................... 28 2.4.1 Algorithm and Explanation . . . . . . . . . . . . . . . . . . . . . 28 2.4.2 Optimizations............................. 35 2.4.3 IC3withSMT............................. 37 2.4.4 IC3forTA............................... 38 3 Timed Automata Verification via IC3 with Zones 41 3.1 SMT-Encoding................................. 42 3.1.1 Variables................................ 43 3.1.2 Encoding of the Initial States . . . . . . . . . . . . . . . . . . . . 44 3.1.3 Encoding of Clock Constraints . . . . . . . . . . . . . . . . . . . 45 3.1.4 Encoding of Integer Constraints . . . . . . . . . . . . . . . . . . 46 ix xvi List of Tables A.4 Results of experiments with IC3 with Zones (Fischer_Bmodel) . . . . . . . 164 A.5 Results of experiments with IC3 with Zones (Lamport_Bmodel) . . . . . . 164 A.6 Results of experiments with IC3 with Zones (Lamport_Smodel) . . . . . . 165 A.7 Results of experiments with IC3 with Zones (ShavitLynch_Bmodel) . . . . 165 A.8 Results of experiments with IC3 with Zones (ShavitLynch_Pmodel) . . . . 166 A.9 Results of experiments with IC3 with Zones (FDDIcount model) . . . . . . 167 A.10 Results of experiments with location identifiers (Fischer_Umodel) . . . . 168 A.11 Inductive strengthenings: Validation and size (Fischer_Umodel) . . . . . 169 A.12 Inductive strengthenings: Validation and size ( Fischer_U(switched) model) 170 A.13 Inductive strengthenings: Validation and size (CSMA/CD model) . . . . 171 A.14 Inductive strengthenings: Validation and size (FDDI model) . . . . . . . 171 A.15 Inductive strengthenings: Validation and size (FDDIcount model) . . . . 172 A.16 Inductive strengthenings: Validation and size (Fischer_Bmodel) . . . . . 172 A.17 Inductive strengthenings: Validation and size (Lamport_Bmodel) . . . . . 172 A.18 Inductive strengthenings: Validation and size (Lamport_Smodel) . . . . . 172 A.19 Inductive strengthenings: Validation and size (ShavitLynch_Bmodel) . . 173 A.20 Inductive strengthenings: Validation and size (ShavitLynch_Pmodel) . . 173 A.21 Inductive strengthenings: Validation and size (Lemgo model) . . . . . . . 173 1 Introduction More than ever does today’s society rely on the correct functionality of software and hardware, as more and more tasks are carried out by computer-controlled systems. This trend can be observed in everyones personal environment, as well as in the industry. Examples of importance are the usage of connected controllers in smart homes, e.g., for doors and radiators, or the paradigm of Industry 4.0 that facilitates the interconnection and adaptation of all components engaged in a production system. As a result, the systems and their interaction grow more and more complex. The increased complexity poses a serious threat to the correct functionality of the systems, as a mistake might more easily stay unnoticed within a large system. With most of the systems being safety critical, every possible effort must be made to avoid and find such mistakes that result in unintended, erroneous behavior. Considering again the above examples, a mistake might result in the smart door opening erroneously, or a sudden, undesired stop in a production system. The consequence might be a loss in production value or the risk of life. In response to this problem, an increasing effort is made to research and introduce structured approaches that are able to ensure a certain quality of a system. One such approach for software is the model driven software development (MDSD) [B+05] that starts as early as possible during development, namely in the design phase. In such structured approaches, a system is specified via models that depict different aspects of it. For example, the unified modeling language (UML) [RJB04] is typically employed for this task during the development of software systems. UML contains numerous types of diagrams to specify different aspects of the system, e.g., use case diagrams to capture behavioral requirements or class diagrams to capture structural relations. These diagrams are not only employed for specification, but are also used for documentation purpose and are often involved in the construction of the final system. To this end, automated transformations and generators are employed that fully automate the task of transformation into other modeling formalisms, or the generation of code. This structured procedure for specification and generation of 1 2CHAPTER 1. INTRODUCTION parts of a software system is often used and helps to achieve a good code quality and architecture. However, every manual specification and modeling might introduce unintended, erroneous behavior in the models and, using the automated generators and transformations, into the final system. For this reason, formal methods are employed that are able to guarantee the absence of such behavior in the models and, in consequence, in the final system, provided the transformations are correct. These formal methods basically draw on three important elements. First, the unintended, erroneous behavior has to be specified. Second, the models that are to be checked need to be specified using a formalism based on a rigorous mathematical semantics in order to enable reasoning about erroneous behavior. Third, the methods that check the absence of the unintended behavior in the given model are required to be sound. There exist many distinct formalisms for modeling the system under development. Many of them are specifically designed to capture certain aspects of the system, e.g., its structure, communication or timed behavior. They are based on a rigorous defined mathematical semantics that allows the reasoning about properties. Using the mathematical foundation, the reasoning about properties of the models can be done using one of the approaches for formal verification. There exist several such techniques, where deductive verification and model checking represent the most well-known categories. Among the most common modeling formalisms are automata, petri nets [Mur89], process calculi [Mil80; Mil99], Z [SA92] and the B-method [AAH05]. In addition, there exist formalisms that encompass an explicit notion of time, e.g., timed automata [AD90], hybrid automata [Hen00], timed petri nets [Ram73], Timed CSP [RR86], Duration Calculus [CHR91] and Timed Graph Transformation Systems [HHH10]. These are of special interest, as real-time systems are of growing importance. As an example, consider the numerous embedded real-time controllers that operate many safety-critical systems, e.g., the time-critical sensing of a car accident with almost immediate inflation of an air bag. Additionally, in the industry more and more real-time systems are employed, as the paradigm of Industry 4.0 often requires the components to communicate using real-time protocols in order to achieve adaptivity and self-optimization of all components in a plant. There exist several additional examples that illustrate today’s importance of real-time systems and time based behavior. In general, such behavior is of interest in many development scenarios and so are the respective formalisms and formal verification methods. As in the untimed case, the formalisms are employed to model specific aspects of the system under development, and verification is employed to check whether specified properties hold true for the model. As explained above, the systems and their interaction grow more and more complex. In consequence, the respective models of these systems become increasingly complex. The formal verification carried out to ensure the quality of the system needs to be able to handle such large models. But with models growing intensely, the verification of properties for them becomes even more challenging due to the 1.1. PROBLEM DEFINITION 3 state explosion problem. An additional problem is the fact that models are often reconfigured, i.e., changed. In the MDSD process mentioned above, reconfigurations may occur repeatedly in the design phase until a final design is found. A reason might be that required properties are not met or that additional parts have to be included. In addition, there exist scenarios in which a model is reconfigured at lifetime of a developed system. These reconfigurations, i.e., changes, to the model reflect changes to the running system. They are of huge importance, in particular, when considering the adaptivity and self-optimization proposed for Industry 4.0 plants. Examples for such reconfigurations at runtime are the adaptation of a plant in which it switches to another operating mode in order to save energy, or the modification of the plant including new components. Furthermore, the substitution of mechanical parts might result in a different timing behavior if the parts possess distinct operating characteristics. In such cases, the system is reconfigured at lifetime, possibly in ways that could not be foreseen within the design-phase. There exist works that are concerned with intelligent assistant systems for such scenarios [JN12], but they do not consider the context of formal verification. Every change in the system might lead to unintended behavior. Thus, there exists a need to verify the properties, which have already been verified for the original model, again for the reconfigured one. To this end, the reconfigured model could be provided manually by a model designer, or even be learned automatically by machine learning algorithms, e.g as timed automata [Mai14] or hybrid automata [Nig+12]. In any case, the verification should be as efficient as possible, in particular, when considering that the properties have already been verified for the original model that might be very similar. Moreover, when taking into account that the reconfigured system might already be running, the urgency of this task becomes obvious. Either way, a reconfigured model would result in a renewed need for verification. With the growing complexity of systems and their models in mind, these verifications should be as efficient as possible. It is, thus, not desirable that these verifications for reconfigured models employ techniques that start from scratch. 1.1 Problem Definition Many of today’s systems exhibit timed behavior. They rely on time in diverse ways, e.g., using real-time communication protocols as can be found for example in the PROFINET standard [Fel04]. Furthermore, the interaction of several components can be seen as timed interdependency, e.g., since the distribution of a product in the plant relies on its completed creation. The quantity of systems with such behavior shows the significance of timed verification. For this task, models are created that reflect the time-based aspects of the system. As illustrated above, the formal modeling and verification can be done at design time of the system, e.g., in the context of model-based design processes, or later on during runtime, e.g., using learned models. Either way, a formal modeling language is required in order to 4CHAPTER 1. INTRODUCTION model the mentioned timed behavior. There exist formalisms that are capable of modeling continuous real-time since the early 1990s. They offer various levels of expressiveness and usability. In this thesis, we employ the formalism of networks of timed automata [AD90]. It is one of the most well-known formalisms with roughly 25 years of research. The modular structure as a network consisting of several timed automata enables an elaborate way of modeling individual components, e.g., representing software processes or different hardware controllers. It is, thus, well suited for the modeling of interconnected components as is the case in Industry 4.0 plants or smart homes. The decidability of reachability questions in this formalism enables the use of formal verification [AD90]. In networks of timed automata, the interconnection of the distinct components’ behaviors is given implicitly via time. In addition, the formalism allows an explicit interaction enforced via synchronization and shared variables. Like in other automata formalisms, timed automata are based on a discrete structure that offers an easy means to specify distinct states of the various components. This discrete structure captures the overall, untimed behavior of the system. However, in timed systems, this behavior highly depends on time. To this end, constraints are introduced that restrict the allowed behavior as a function of the elapsed time. This intuitive mechanism of observing the progress of time and, in dependence, limiting the allowed behavior is a basic concept, also included in several other timed formalisms, e.g., timed petri nets or timed graph transformation systems. In this thesis, we are concerned with the verification of safety properties that specify the non-reachability of error states. These error states are an intuitive way to specify unintended or undesired behavior. The absence of such erroneous behavior can be guaranteed via a formal verification of the safety properties. For the formalism of networks of timed automata, there already exist techniques and tools to verify such properties. Considering the requirements of today’s systems and Industry 4.0, these approaches are not well suited. Most of them are optimized for runtime, i.e., they are fast at the expense of used memory, mostly due to explicit exploration. Taking into account the increasing size of the systems and their interconnectivity, an approach is desirable that is capable of verifying large models without running out of memory easily. Furthermore, most of the current techniques are not suited to cope with reconfigured models as may happen often, e.g., during model-based design processes. These approaches require a verification of the properties for the reconfigured model that starts from scratch. These are the two problems we approach in this thesis. They are summed up in the following. • The verification of large models, in particular those with a large set of reachable states, poses a problem for many existing techniques. Many of these techniques rely on an explicit exploration and representation of the forward or backward reachable states. These states have to be stored in order to know which states 1.2. CONTRIBUTION 5 have already been explored. Trivially, a large number of such states results in huge memory requirements, which is often the reason that a verification is aborted. We will focus on a technique that does not require the exploration of each reachable state. To this end, it employs induction. We seek to develop an approach that handles complex, large models well. • The second problem in the above setting is that many models might be reconfigured during design time or lifetime. Current verification techniques for timed automata are not designed for an efficient verification of the reconfigured models. They will start a verification from scratch and, thus, waste the chance to reuse a previous verification result. Even if they would be capable of reusing a previous outcome, their explicit method would need to check every such state again, as the state space has changed. Our focus on an inductive method establishes a distinct chance, as it can be reused in a more elaborate way. We seek to develop a technique that efficiently verifies safety properties for reconfigured models in order to support repeated reconfigurations during design time, and in order to enable online verification, i.e., verifications during lifetime of a system. In the following, we will state our contributions for these two problems. 1.2 Contribution This thesis is concerned with both of the problems pointed out above. We propose a novel technique for the verification of safety properties for networks of timed automata. Based on an inductive invariant computed by this technique, we accelerate the verification of safety properties for reconfigured models. In detail, our contribution is as follows. IC3 with Zones As mentioned above, many of the verification techniques for safety properties in networks of timed automata suffer from large memory requirements. When handling large models with a huge set of reachable states, the explicit exploration that is used in many state-of-the-art approaches easily runs out of memory. The reason is that the algorithm needs to store the already explored states in order to detect whether a new state was already discovered. Thus, their memory need can be seen as one of the most important weaknesses of the current verification techniques. We avoid the explicit exploration and discovery of every reachable state. To this end, we transfer the IC3 algorithm to the domain of timed verification in a competitive way. We present, implement and evaluate a concept that combines the strengths of the following two elements. • The IC3 algorithm [Bra11] has proven to be successful and efficient, both regarding runtime and memory, for the verification of safety properties on discrete structures. It is based on induction and SAT-solving and, thus, works differently than the exploration algorithms usually employed in timed verification. Its mechanisms avoid the discovery and storage over every reachable 6CHAPTER 1. INTRODUCTION state, but instead compute an inductive invariant stored as a compact propositional formula. We employ this efficiency and distinctiveness in our approach in order to avoid the common problem of storing explicitly explored states. • The Zone abstraction has been employed numerous times for timed verification. It is versatile in that it can be very fine grained or very coarse and there exist sophisticated algorithms to efficiently manipulate zones. Using these efficient algorithms and the proper coarseness, we employ this abstraction in order to handle the infinite state space imposed by the semantics of timed automata. By combination of these two elements, we achieve a transfer of the IC3 algorithm to the domain of timed verification, which is competitive, unlike previous attempts. The result is a technique that works in a way distinct than other state-of-the-art techniques in timed verification, namely by using induction. It combines the strengths of the two included elements and, thus, avoids the weakness of storing explicitly explored states, i.e., the enormous need for memory. Our technique employs SMT-solving [BST10] and is based on induction. The main challenge is the infinite state transition system imposed by the semantics of timed automata. As explained, we employ the Zone abstraction in order to cope with this problem and ensure termination. The integration of this abstraction into the IC3 algorithm is based on the structure of the SMT-queries. Our combination achieves termination and efficiency. We show this efficiency and practicality of our proposed technique in numerous experiments. Using standard examples from literature, we illustrate that our approach is able to outperform state-of-the-art tools by models up to three times as large. We present experiments to examine the scalability of our approach with regard to the model size, the used location encoding and the usage of integer variables. Summing up, we present a combination of two techniques from distinct domains. It does, unlike most other techniques in the domain, not explicitly explore and store the reachable state space. Instead, our technique employs induction for the verification of safety properties in timed systems modeled as networks of timed automata. Due to its distinct working paradigm, the presented technique is well suited to be used for large, complex models as in today’s systems. It is a relevant alternative to long-established approaches and might give thoughtprovoking impulses. Our technique yields a valuable additional outcome in case of verification success, which we employ for the second problem defined above (Section 1.1). It computes an inductive invariant that we store and reuse for the verification of properties for reconfigured models. In the following, we state our contribution in this direction. The first work deals with specific reconfigurations that add an instance of a process to an already existing number of such instances. Doing so numerous times creates a system with an arbitrary large, but fixed number of processes. These systems are denoted parameterized timed systems. 1.2. CONTRIBUTION 7 Parameterized Timed Systems Parameterized Timed Systems occur frequently in modern systems. For example, consider a scenario in which a number of robots requires the exclusive access to a resource, e.g., to the top element of a pile of raw materials in order to start working. In order to avoid problems, the decision which robot gains access can be negotiated by their controllers using a mutual exclusion algorithm. To ensure error-free functioning, the involved controllers might have been modeled and mutual exclusion has been verified. However, if an additional robot is added, e.g., to increase the productivity, the same property needs to be verified again for the reconfigured system including the additional controller. There exist many other scenarios that also raise the need for a new verification whenever the system is reconfigured with a new number of processes. We have proposed a novel approach for the verification of safety properties for such parameterized timed systems that consist of an arbitrary, but fixed number of instantiations of a process. Our technique enables an a priori verification of the entire system, where the actual number of instances during runtime does not matter. Thus, the system can be reconfigured by addition or deletion of processes without raising the need for a new verification. Instead, based on the a priori verification one can be sure that the safety property holds irrespective of the number. This technique avoids the need for online verification for systems that can be modeled as such a parameterized timed system. It is competitive and able to reason about the entire family of models in the system by considering only a few fixed instances. To this end, it reuses verification results obtained during the verification for these fixed instances in order to reason about all larger models. This reuse is extremely efficient. Our approach consists of several important parts. We propose a workflow that incrementally verifies the safety property in question for models with increasing size. It employs our algorithm IC3 with Zones presented in the previous paragraph and, thus, profits from possible improvements in the future. The inductive invariants computed by the algorithm are adapted using the symmetry inherent in parameterized timed systems and later on used to reason about the entire system. To this end, we propose and prove a Termination Theorem that is the basis for this reasoning. Additionally, we reuse the adapted inductive invariants in order to accelerate subsequent verifications of the safety property for reconfigured models, which means in this context that they include an additional process. Both reuses of previously computed results are extremely successful as shown in numerous experiments. We were able to verify mutual exclusion for all considered parameterized timed systems, i.e., for any number of instances. This ability is a significant benefit over the single verification for a fixed model. As an example, consider a model with one million timed automata, which can be verified by our technique in the context of parameterized timed systems. Summing up, we present an approach that entirely avoid the need for online verification in the context of parameterized timed systems. Using an a priori verification, it allows the reconfiguration of the system in terms of the number of 8CHAPTER 1. INTRODUCTION processes without raising the need for a new verification. It is competitive and efficient in that it reuses computed inductive invariants. Reusing previously computed inductive invariants to accelerate the verification of reconfigured models does not only work in the parameterized setting, but also in a general one. We denote this reuse as Feedback-mechanism and apply it in the following work for general models and reconfigurations. Verification in the Event of General Reconfigurations In the previous setting, the specific kind of systems allows an easy estimation of the effects of a reconfiguration based on the inherent symmetry. For generic reconfigurations, however, the effects can not be estimated in general. For example, consider a self adaptation of a system in a plant. Although the future behavior mode is determined by this adaptation, it can not be estimated how this behavior will work out considering the entire system in the future. In general, a reconfiguration as little as the change of a timing constant might ultimately lead to unintended behavior. As the effect on the entire system can not be estimated, we propose a best-guess approach that tries to adapt the inductive invariant as good as possible. Afterwards the adapted invariant is used in the Feedback-mechanism in order to accelerate the verification of the property for the reconfigured model. Based on the reconfigurations that have been carried out, we adapt the invariant such that it is usable in the new verification and reflects the changes applied to the model. However, due to the IC3 algorithm and the zone computation, this adaptation is extremely limited. Even so, often the adapted inductive invariant can successfully be applied to accelerate the verification of the safety property for the reconfigured model. We have conducted several experiments to show the value of this technique. Even with a reconfiguration that introduces a violation of the safety property, our feedback mechanism has shown to be of help. Clearly, the value of this technique in general is limited. Reconfigurations that introduce too much change in the model will ultimately result in a useless reuse of the inductive invariant. Nevertheless, we have introduced and examined a reuse mechanism that is able to accelerate the verification of safety properties for reconfigured timed systems in general. It is successful for many instances, in particular, when considering small reconfigurations for large models as might often be the case in model-based design processes or reconfigurations of timed systems during lifetime. The technique gives an important impulse for online verification of reconfigured models, as might be needed increasingly in the future due to paradigms like Industry 4.0. In summary, the following contributions are made. We successfully transfer the IC3 algorithm into the domain of timed systems, such that it is competitive. To this end, we propose a combination with the Zone abstraction, which works in a distinct way than other techniques and, thus, gives new impulses and is of value as 1.3. THESIS OUTLINE 9 a complement to existing approaches. Numerous experiments show its value and practicality. Using the inductive invariant computed by the proposed approach, we introduce an approach for a priori verification of an entire parameterized timed system. It allows the verification of safety properties for any number of instantiations of a processes in these systems, such that the addition or deletion of a process does no longer raise the need for a new verification. Several experiments are employed to show the practicality, in particular when reusing previously computed inductive invariants for the acceleration of new verification runs for reconfigured models. Finally, we employ this reuse in a general setting. We present a best-guess approach that allows an efficient verification of safety properties for reconfigured models and, thereby, enables online verification for reconfigurations during lifetime of a system. Our experiments are promising, even though general reconfigurations are hard to handle. Our work is, thus, of value for the intended use, namely the verification of large, complex models in the context of reconfigurations. The contributions are presented in the thesis in the following order. 1.3 Thesis Outline Following this introduction, Chapter 2 introduces the formalism used throughout this thesis. We formally define the employed modeling formalism and its semantics before specifying the considered safety properties. Elaborating the related work, we highlight important work during the 25 years of research in this field. Afterwards, we start with an introduction to SAT-based verification, which includes a detailed section about the employed IC3 algorithm. Its optimizations and related work are given subsequently. We finish the chapter with relevant related work that employs IC3, e.g., for timed verification using the region abstraction. Chapter 3 contains our work on the combination of the IC3 algorithm with the Zone abstraction. We start with the encoding of our formalism via SMT-formulae. Subsequently giving a detailed explanation of our integration of the zone computation in IC3, we close the chapter with a thorough section showing the practicality and value of our work including numerous experiments. Chapter 4 presents our work on parameterized timed systems. It starts with a general introduction of parameterized systems, before defining the models considered in this work. To this end, we introduce some restrictions necessary to yield the notion of symmetry we intent and exploit in our approach. We illustrate the incremental workflow that is the heart of our approach, before giving the Termination Theorem that enables our reasoning about the entire parameterized system. Subsequently, we introduce two promising optimizations that accelerate the workflow and increase the applicability of the theorem. Next, we present the numerous experiments we have conducted and their results. In the next chapter, we propose an extension to the formalism used in our incremental workflow for parameterized timed systems. It significantly improves the 16 CHAPTER 2. BACKGROUND In addition the clock is reset once more. To gain access to the critical section (location l3 ), the process must wait for more than 1024 time units, forcing other processes requesting access to update the value of id . If there are no other processes, id still contains the same identifier (1) and the process is allowed to take the edge leading from l2 to l3 . Otherwise, he would have to take the edge leading again to l1 , which may only be taken after the process in the critical section left it and reset the shared variable id to 0. Note, that the variable cnt counts the number of processes in the critical section. The semantics illustrated above can be formalized as a transition system as was done, e.g., by Behrmann [Beh+04]. It is denoted as concrete semantics due to a state containing only concrete values, meaning a single location, clock and integer valuation. Definition 2.1.10. Let A= (L , l0 , C , IV , Σ , Invc , Invi , E) be defined over Cg , IV and Σ as in Def. 2.1.8. The transition system TS = (S , s0 , →) defines the concrete semantics: •S=L×RC ≥0×ZIV is the set of states, •s0= (l0,vc 0,vi 0)∈Sis the initial state, •→⊆ S×Scontains delay transitions →dand edge transition →e: –(l,vc,vi)→d(l,vc+δ,vi)iff ∀0≤δ0≤δ:(vc+δ0)|=Invc(l) –(l , vc , vi)→e(l0 , vc0 , vi0) iff ∃(le,φ,ψ,ω,R −−−−−→ l0)∈E , s.t. vc|=φ , vc0=vc[R] , vc0|=Invc(l0),vi|=ψ,vi0=vi[ω],vi0|=Invi(l0). As can be seen only unsynchronized edges (with synchronization label e ) can be taken in a single timed automaton since no synchronization partner is available. However, one of the most convenient aspects in modeling timed automata is the ability for compositional modeling. We call a composed model, consisting of several timed automata running in parallel, a network of timed automata. These automata are modeled separately, but interact with each other via clocks, integer variables and synchronized edges. The downside, however, is the exponential blowup of states, as the semantics of such a network equals the product automaton. We formally define the composition of timed automata A1,...,Anas follows. Definition 2.1.11 (Network of Timed Automata) . Let Cg , IV and Σ be given, as well as the timed automata A1 to An defined over them. For distinction, their parts are marked with subscripts such that Aj= (Lj , l0j , Cj , IV , Σ , Invcj , Invij , Ej) . All sets of clocks ( Cg , Cl 1 , . . . Cl n ) are required to be mutually distinct. The product automaton defining the network of timed automata NTA =hA1 ,..., Ani is defined over Cg , IV and Σas A= (L,l0,C,IV,Σ,Invc,Invi,E)with 2.1. TIMED AUTOMATA 17 •L=L1×... ×Lnwith initial state l0= (l01,..., l0n)∈L, •C=Cg∪Cl 1∪... ∪Cl nwith initial valuation according to local valuations vc 0, •Invc(l1, ..., ln) = Invc1(l1)∧... ∧Invcn(ln), •Invi(l1, ..., ln) = Invi1(l1)∧... ∧Invin(ln), •Eis defined as –∀i∈ {1, ..., n}:((..., li,...)σ,φ,ψ,ω,R −−−−−→ (..., li0,...)) ∈E if (liσ,φ,ψ,ω,R −−−−−→ li0)∈Ei –∀i6=j∈ {1, ..., n}:((..., li, ..., lj,...)e,φ,ψ,ω,R −−−−−→ (..., li0, ..., lj0,...)) ∈E if (lia!, φ1,ψ1,ω1,R1 −−−−−−−−→ li0)∈Eiand (lja?, φ2,ψ2,ω2,R2 −−−−−−−−→ lj0)∈Ej with φ=φ1∧φ2,ψ=ψ1∧ψ2,ω=ω1;ω2,R=R1∪R2. The product automaton contains a non-synchronized edge (with synchronization label e ) wherever two edges have successfully been synchronized, i.e., that edge is allowed to be taken. Note, that the assignments of the sender edge ( m! ) are applied before those of the receiver edge ( m? ). Additionally, it still contains the original edges (see the first bullet point defining E above) including those requiring a synchronization partner. These are included for further composition, but are not allowed to be taken as defined in the concrete semantics in Definition 2.1.10 since they contain a synchronization label distinct from e. Verification of properties for timed automata was done right from the start supported by decidability results of Alur and Dill in 1990 [AD90]. One of the most important and interesting verification question is reachability of a state s . It asks whether there exists a finite number of transition steps leading from an initial state to s . This verification question is challenging not only due to the infinite transition system introduced by the real valued clocks, but also due to the state explosion problem in general. The notion of reachability allows for the definition of safety properties, which specify that something bad should never happen. To this end, error state specifications are defined that describe the bad situation. The safety property holds true, i.e., the model is safe w.r.t. the safety property, if no error state is reachable. The verification of safety properties is of fundamental importance [Hal93] as many verification questions of interest can be expressed as safety properties. We formally define reachability and safety properties as follows. Definition 2.1.12 (Reachability) . Let a timed automaton A be given with concrete semantics TS = (S , s0 , →) . A state s∈S is reachable, if there exists a finite number of transitions leading from the initial state to s, formally s0→s1→... →sn→s. When considering some states as bad, or error states, we employ reachability to define safety properties that require these error states to be unreachable. To this end, 18 CHAPTER 2. BACKGROUND we define error state specifications that are able to efficiently characterize error states. We employ integer and clock constraints, which allows us to specify more than a single concrete state at once. Definition 2.1.13 (Error State Specification) . Let a network of timed automata NTA =hA1 ,..., Ani be given as in Def. 2.1.11 with concrete semantics TS = (S , s0 , →) . An error state specification is an abstract formalization of a set of undesired states. The set of error state specifications is defined as ERR = ((L1∪ {∗})× · · · × (Ln∪ {∗})) ×Φ(C)×Ψ(IV) . Each error state specification err = (¯ l , φ , ψ)∈ERR includes a clock and an integer constraint and additionally a (partial) location vector ¯ l∈(L1∪ {∗})× · · · × (Ln∪ {∗}) specifying at most one location for each timed automaton. The element ∗ stands for an undefined location. To refer to specific locations in the vector, we denote the location specified for automaton Ai as ¯ l[i] . A state s= ((l1 ,..., ln) , vc , vi)∈S is included in an error state specification err = (¯ l , φ , ψ) , denoted s|=err, iff •∀i∈ {1, . . . , n}:¯ l[i] = ∗or ¯ l[i] = li, •vc|=φ, •vi|=ψ. The states that satisfy an error state specification are called Error States. The safety properties used within this thesis specify that no reachable state is allowed to be an error state. We formally define it as follows. Definition 2.1.14 (Safety Property) . Let a network of timed automata NTA = hA1 ,..., Ani be given as in Def. 2.1.11 with concrete semantics TS = (S , s0 , →) . Using the notation of of the LTL-operator G, we define a safety property ρ:= G(¬err1∧ ¬err2. . . ) to be the conjunction of the negations of error state specifications err1 , err2 , . . . . It holds true, when no reachable state in S is an error state, formally ∀s∈S:s is reachable ⇒(s2err1∧s2err2∧. . . ) . Then, we say the safety property is invariant. Otherwise, at least one state s∈S is reachable via a finite number of transitions s0→s1→ · · · → sn→s and satisfies one of the error state specifications s|=erri . This path violates the safety property and is, thus, called a counterexample trace for the given safety property. Usually, the verification of properties for networks of timed automata is done on-the-fly without the computation of the product automaton, due to the enormous increase in size of states. However, it still needs to take into account the interdependencies of the individual automata resulting in enormous effort. Thus, since the beginning diverse attempts have been made to establish the practicality of verification for timed automata. 2.1. TIMED AUTOMATA 19 2.1.1 Decidability and Abstractions The feasibility of verifying reachability properties for timed automata was established in 1990 by Alur and Dill [AD90]. They proved decidability, which is not intuitive due to the real valued clocks. To this end, they proposed a finite abstraction of the clock valuations based on the observation that some of them have equal characteristics. Given the fact that clocks are only compared to integer constants within clock constraints the actual fractional part of a clock value does not matter. This fractional part is only of interest to identify which clock will change its integral part first. Taking into account that time progresses simultaneously for all clocks, Alur et al. described the region abstraction, which partitioned the clock valuations into equivalence regions. Definition 2.1.15. Let A be a given timed automaton as in Def. 2.1.8. For every clock x∈C let nx be the largest constant with which x is compared to. Two clock valuations vcand vc0are in the same region, iff: •∀x∈C:bvc(x)c=bvc0(x)cor vc(x)>nx∧vc0(x)>nx, •∀x , y∈C with vc(x)≤nx and vc(y)≤ny : fract(vc(x)) ≤f ract(vc(y)) iff fract(vc0(x)) ≤f ract(vc0(y)), •∀x∈Cwith vc(x)≤nx:fract(vc(x)) = 0 iff fract(vc0(x)) = 0. with fract meaning the fractional part of the value. Since the number of clocks and the largest constants are fixed within a timed automaton, the number of regions is finite [AD94]. Thus, decidability of reachability was shown since every reachability question for a timed automaton can be decided via this finite abstraction. Unfortunately, the number of regions grows exponentially with the size of constants and number of clocks [AD94]. Hence, decidability via region abstraction is an interesting theoretical result, but not of substantial value for practical verification purposes. This drawback is tackled by the zone abstraction. Definition 2.1.16. AZone Z is a convex set of clock valuations, specified as a conjunction of clock difference constraints xi−xj./ n with xi , xj∈C∪ {x0= 0},./ ∈ {<,≤} and n∈Z. Each zone is a convex union of regions and can be described via upper and lower bounds on single clocks and clock differences. It can efficiently be stored as a Difference Bound Matrix (DBMs) [Dil90], which allows for an efficient computation of the zones of predecessor or successor states. Thus, it gives rise to a significantly coarser symbolic transition system that is of practical relevance. It is used within many algorithms and tools. In the following, we survey the research that was done to establish practicality of the verification for timed systems. 20 CHAPTER 2. BACKGROUND 2.1.2 Related work We start with a discussion of some algorithms for the verification of safety properties for timed automata, followed by special data structure and tools. The same sequence was also used in a survey paper by Yovine in 1998 [Yov98]. There exist various approaches for the reachability analysis of timed automata. Given that standard exhaustive exploration on the region abstraction is not efficient, some tools apply digitization to completely abstract away the time domain. To this end, a finite set of representatives is computed to represent each region [Göl+94]. In general, digitization enables the use of untimed verification algorithms, which are often more sophisticated than simple exhaustive search. For some restricted subclasses of timed automata, a BDD-based fixpoint analysis [Bey01] has proven to be specifically successful. However, these techniques still suffer from a search space exponentially in the size of the used constants in the model. Hence, coarser abstractions were sought after. One way is to find an equivalence relation that is smaller and, thus, better suited for verification. There exist various approaches searching the minimal finite transition system equivalent to the region graph up to time-abstracting bisimulation [Yov98; TY96; Alu+92]. Other approaches try to minimize the timed automaton itself, while maintaining a similar notion of bisimulation [DY96]. When considering basic forward or backward search, the utilization of clock constraints to describe sets of clock valuations comes naturally. Their conjunction, denoted a Zone, describes a convex set of clock valuations. Due to being closed under time elapse and transition steps, zones are optimally suited for exhaustive exploration of the search space. Furthermore, the resulting zones are efficiently computable. All these different ways of abstraction show the non-triviality of timed verification. In the end, the success of the abstraction strongly depends on its combination with clever verification algorithms and data structures. Most often, in particular in combination with the region or zone abstraction, a basic exhaustive search is performed. Starting from the initial state, all successor states are computed and added to the queue of unprocessed states. This queue is worked off until there are no states left that have not been processed before. Upon discovery, every single state is checked for violation of the safety property. Exhaustive search can also be done in a backwards-manner, where states are discovered starting from the error states. Especially when using the zone abstraction, this basic algorithm provides for an easy and efficient analysis. Stored in DBMs, the memory usage is passable, while providing easy mechanisms to compute successor-, predecessor- or time-elapse-zones [Dil90; DT98]. More sophisticated approaches try to minimize memory usage by exploiting the fact, that most often some clock constraints in a DBM are redundant. There exist various publications on how to compute and maintain a minimal list of such constraints [YPD94; Lar+97]. Despite these optimizations in memory efficiency, one major problem of the exhaustive search approach in combination with zones remains difficult. Each discovered state is stored to be able to tell whether a state has already been explored. A short check if a new state 2.1. TIMED AUTOMATA 21 is already stored suffices to stop further exploration on this state. Considering zones, however, a simple check whether a zone (for a specific location and integer valuation) has already been stored is inefficient. The reason is that the zone could be covered by the union of several previously explored zones. Hence, a suitable coverage check might be needed that stops the exploration of zones covered by the union of previously explored zones. With zones not being closed under union, several data structures have been proposed offering efficient mechanisms to store and maintain non-convex unions of zones with a fast inclusion check. However, in the end these data structures only provide for a trade-off reducing the enormous amount of memory needed for storing each single zone, but (most often) slightly increasing the runtime. Most of these non-convex data structures are build as decision diagrams. Proposed in 1997, numerical decision diagrams were the first data structure aiming at a small representation of unions of zones [Asa+97]. The approach is based on discretization of time and employs binary decision diagrams [Lee59; Ake78] for storing a bitwise encoding of the time values. Thus, it heavily depends on the size of the encoded constants rendering it inefficient for the verification of safety properties for most timed automata. The same disadvantage is observed in region encoding diagrams [Wan00]. They represent a region by the integer parts of the clock values and the ordering of the fractional parts. Given all the necessary algorithms for data manipulation, it is suitable as a decision diagram, but as mentioned lacks the capability to handle large constants. Later approaches are not tied to a discretized time or region encoding and are, thus, independent of the size of timing constants. Larsen et al. introduced clock difference diagrams (CDD) in 1998 [Lar+98; Beh+99] pursuing the goal of a data structure for completely BDD-based verification approaches. Clock difference diagrams are defined over the real valued difference of clock values. In addition, they branch with regard to intervals of the reals, while previous techniques branched only for single values. This makes them significantly less dependent on the size of constants. Designed to share redundant substructures, clock difference diagrams are well suited for space-efficient coverage decisions. Other approaches were not optimized for coverage checks, but more on space efficiency. Reduced clock restriction diagrams [Wan01a] utilize the small number of constraints needed to represent a zone [Lar+97]. Given such a minimal constraint system, a compact representation is achieved, which lacks the capability for efficient determination of zone containment. Thus, Wang enhanced his approach resulting in cascading clock restriction diagrams [Wan02; Wan03]. The technique is based on the cascading form of zones, which may require more constraints than the reduced form, but still less than a complete DBM. All these data structures aim to reduce the memory required for verification, mostly as a trade-off to a slightly increased runtime. While the presented data structures were able to reduce memory consumption in general, they still run out of memory easily when verifying properties for large models. Despite these shortcomings, they have been applied in various verification tools, which we show in the following. The implementations of all the different concepts and algorithms 22 CHAPTER 2. BACKGROUND have been extremely successful in the verification tasks both for academic and real world models. Over the last 20 years, research has led to the creation of several tools, most of which are not actively maintained any more. The concepts used in these tools are very diverse resulting in different modeling and verification capabilities. In the following, we give a brief survey. The development of the first tools started in the early 1990s. Kronos [Daw+96; Boz+98] uses several of the techniques presented above. It implements symbolic analysis, as well as time-abstracting bisimulation. It employs several data structures, e.g., DBMs and NDDs and triggered a lot of research. The last release of Kronos has been in 2002 and since then it has not been developed any further. Another early tool for the verification of safety properties for timed automata is called Uppaal [LPY95; LPY97] developed by researchers from the universities of Uppsala and Aalborg. It is actively developed and maintained down to the present day. Given its graphical user interface it offers an easy mechanism for modeling and verification, which might be one of the reasons for its success even in commercial applications. The other reason for its huge success is the efficient verification, which has been applied to several interesting real-world studies [Hav+97; LPY98; Ben+96]. It is based on constraint solving with DBMs represented as minimal constraint systems. Furthermore, it can apply CDDs and several options for optimization and approximation. With more than 15 years of development [Beh+11], it includes a lot of great ideas and has become the most well known tool and also quasi-standard for the verification of safety properties for timed automata. Thus, later tools most often had to compare their performance with Uppaal. The tool Red [Wan01b] that was first implemented using region encoding diagrams was developed in the early 2000s. Later its verification engine was based on the presented clock restriction diagrams. The development of Red, however, was discontinued in 2003. Other tools are based on other techniques. A perfect example for this sort of diversity is the tool Rabbit [BR00], which is based on digitization in order to apply BDD-based techniques. Thorough investigations into the best variable orderings, and adjusted BDD-based algorithms showed a great performance. However, the approach is still unsatisfying as it highly depends on the size of time constants. In the last few years, two new tools have been developed that are capable of verifying timed automata. Synthia [PEM11] is one of these tools, but has only been actively developed for 2 years, being discontinued in 2011. The tool PAT [Sun+09], however, is developed and maintained starting in 2009 up to now. It includes a wide variety of verification techniques including digitization and BDD-based algorithms. In summary, there has been an enormous amount of research in the field of timed automata over the last 25 years. Many techniques have been investigated and implemented in various tools. However, today only two tools are left that are actively maintained. These two represent the most successful verification approaches, as Uppaal heavily relies on zone based verification and PAT utilized digitization 2.2. SAT- & SMT-SOLVING 23 with BDD-based verification. With the latter being dependent on the size of time constants, it is conceptually less relevant. Thus, we will examine the techniques presented in the following chapters in comparison with Uppaal. Even after 15 years of research, Uppaal can easily be pushed to its limits. As a reason for failed verification attempts, most often its enormous need of memory has to be named. In consequence, for this thesis we are interested in techniques with better memory efficiency. 2.2 SAT- & SMT-Solving In addition to the techniques presented before, there exist various concepts employing SAT- or SMT-solvers for verification. We present a short overview on SAT- and SMT-solving that might be helpful to understand Chapters 3 to 6. 2.2.1 SAT-Solving The boolean satisfiability problem is defined as follows: Definition 2.2.1. Let a boolean formula be given. The boolean satisfiability problem ( SAT ) asks whether there exists an interpretation, meaning a consistent assignment of truth values true or f alse to the propositional variables, that evaluates the formula to true. It is called a satisfying interpretation. If there exists a satisfying interpretation, the formula is said to be satisfiable, otherwise it is called unsatisfiable. Various tools, called SAT-solvers, exist that try to answer the boolean satisfiability problem. The problem is fundamental for complexity theory and has been subject to research for many decades. In 1971 it was proven to be NP −complete [Coo71], however, a lot of research on efficient algorithms and heuristics build up the practicality of today’s tools, e.g., MiniSAT [ES05], PicoSAT [Bie08] or others [Bie12; AS12; LP10]. Most of the tools are based on conflict-driven clause learning algorithms building on the DPLL approach, named after the researchers Martin Davis, Hilary Putnam, George Logemann and Donald W. Loveland [DP60; DLL62]. The algorithm assigns a truth value to literals and afterwards propagates them to simplify the remaining clauses. Upon discovery of a conflict, the algorithm learns a clause representing the cause of the conflict and backtracks. Most SAT-solvers require the boolean formula to be in conjunctive normal form, which is not a problem due to algorithms for satisfiability-preserving transformations [Tse83; PG86] in polynomial time. In 1999 the usage of SAT-solvers found its way into the domain of untimed formal modeling and verification for finite state transition systems. The reason was that earlier techniques such as explicit model checking or BDD-based approaches reached their limits due to scalability issues. Biere et al. [Bie+99] introduced the concept of Bounded Model Checking in order to check transition systems for counterexample traces of bounded length. The technique relies on an encoding of a bounded unrolling of the transition relation as a boolean formula to check for an error path of 24 CHAPTER 2. BACKGROUND fixed length in the model. The formula is issued to a SAT-solver. In case the solver returns unsatis f iable , there exists no such path. Otherwise, the returned satisfying interpretation embodies the found error path. Due to the success of Bounded Model Checking, the application of SAT-based techniques for formal verification advanced. Concepts were presented that were not limited to a bounded exploration of the state space, e.g., by McMillan [McM02]. Other work extended the capabilities of bounded model checking by computing Craig Interpolants from unsatisfiability proofs [McM03]. Integrated in an iterative fixpoint computation, these are used to compute an over-approximation of the reachable states and prove the absence of counterexample traces. In addition, SAT-solving is applied also in abstraction-based reasoning, called counterexample-guided abstraction refinement (CEGAR) [Cla+02; Cha+02]. To this end, abstract counterexamples are checked for spuriousness using SAT-queries and possible refinements are done based on the results of the solver. Further applications of SAT-solving include approaches relying on induction. We discuss these techniques in more detail in Section 2.3. Many of the above techniques have been transfered to the domain of timed systems. However, with time being represented by unbounded real valued clocks, an encoding using boolean variables is non-trivial. Thus, most approaches rely on an extension of boolean satisfiability, which we present in the following. 2.2.2 SMT-Solving The Satisfiability Modulo Theories-problem is a generalization of the boolean satisfiability problem. It denotes the search for a satisfying interpretation for a formula in first-order logic, where some symbols have fixed interpretations determined by background theories. There exists a large variety of such theories, some of which are specifically designed to reason about data structures like bit vectors or arrays. In the context of this work, however, we are most interested in the theory of reals, which enables the SMT-solver to handle real-valued variables in combination with operators, e.g., addition and multiplication. Furthermore, the theory of integers may be employed to encode integer variables. The use of these theories results in an easy and natural way to encode timed systems as logical formulae. These can be issued to an SMT-solver asking for satisfiability. If the SMT- formula is satisfiable, the satisfying interpretation, also called SAT-Model is returned. Otherwise, the formula is unsatisfiable and the solver may return an UNSAT-Core, which identifies those parts of the formula that take part in its unsatisfiability. Various SMT-solvers exist [DB08; Dut14; CHN12; Cim+13b; Bar+11] and although most of them accept the same input format, standardized as SMT-Lib [BST10], they differ in their capabilities and algorithms. Most modern SMT-solvers use the lazy approach, which is based on an extension of the DPLL-algorithm, called DPLL(T) [NOT06]. In general, a run of a SAT-solver determines candidate assignments of the boolean structure whose satisfiability would result in the satisfiability of the whole formula. Afterwards, these assignments are checked by theory solvers 2.3. INDUCTION BASED REASONING 25 whether they comply with the theories. A close integration of those theory solvers within the DPLL-algorithm has shown as successful basis for SMT-solvers. Further improvements and the rich use of heuristics led to a huge success of these tools. Although their efficiency is a bit behind the one of SAT-solvers, SMT-solvers are employed efficiently in many domains and are capable of solving very diverse SMT-instances. Given their expressiveness, they are an easy and natural way of encoding timed systems. Thus, many of the SAT-based model checking approaches have been transferred to the domain of SMT, including their employment for the verification of safety properties for timed automata. Bounded Model Checking has been one of the first employments of SMT-solvers for the verification of safety properties for timed automata. Starting in 2002, a large number of works has been published from a variety of researchers [PWZ02; Aud+02; Sor03; KJN12a]. All these works use SMT-encodings of paths in the timed systems, but differ in nuances and research focus. SMT is the enabling technique for these contributions, as they employ the theory of reals to encode the real-valued clocks. Interpolation-based reasoning has also been transferred to be used with infinite systems [McM05] like timed automata. However, apart from the mentioned approach for infinite systems in general, it was not in the focus of research. In addition to the presented work, a lot of techniques based on induction have been transferred from the SAT domain to SMT-solving. 2.3 Induction based Reasoning Induction is a proof-principle of high interest. Checking whether a property is inductive or not is efficient and trivial since it does not involve an unrolling of the transition system. The following explanations rely on the notion of a transition system, which may be infinite, as can be seen in Definition 2.1.10. Definition 2.3.1 (Transition System) . A transition system A= (S , I , T) is defined over a set of states S with initial states I⊆S . A transition relation T⊆S×S defines the passage from state to state. We denote a transition system to be a finite state transition system (FTS), whenever Sis finite. We define induction and related concepts using SAT- or SMT-encodings. These encodings usually employ distinct sets of variables x , x0 , x00 , . . . to encode the different states occurring on a path. We let kI(x)k and kρ(x)k denote the encodings of the initial states, and those states that satisfy the property ρ , respectively. Additionally, kT(x , x0)k encodes the transition relation, where the primed variables refer to the next state as explained above. Using these encodings within queries to SAT- or SMT-solvers, their unsatisfiability can be used to check whether certain properties like induction are satisfied. 32 CHAPTER 2. BACKGROUND This blocking process can be seen as a sequence of exclusions starting from F0 up to Fn . With s being no initial state, it is not a member of F0 . The unsatisfiability of kF0k ∧ ¬ksk∧kTk∧ksk0 assures that s is unreachable in one transition from F0 and can be excluded in F1 . The unsatisfiability of kF1k ∧ ¬ksk∧kTk∧ksk0 assures that s is unreachable in one transition from F1\ {s} and can be excluded in F2 . The sequence goes forth until scan be excluded from Fn. However, the query for inductive relativeness might be satisfiable for some obligations. In that case, a state t (distinct to s ) exists that is a predecessor of s and is a member of Fn−1 . The state t prevents the exclusion of s from Fn , since it hinders ¬s from being inductive relative to Fn−1 . It is, thus, a Counterexample to Induction and needs to be excluded from Fn−1 in order to be able to eventually exclude s from Fn . Line 39 shows the creation of a new obligation (t , n− 1 ) that expresses this fact. In a very specific case, such an obligation does not need to be created as the exclusion of t from Fn−1 is not possible. Line 33 checks whether Fn−1=F0 , which means we need to block a state from F0 , which is not possible since F0 contains exactly the initial states (cf. line 6). Thus, IC3 found the predecessor t of another CTI s, which is itself a predecessor. Following the found list of predecessors creates a path from an initial state to an error state, meaning a counterexample trace has been found and IC3 terminates (lines 35, 23 and 9). If no such counterexample is found, eventually all obligations are worked off (line 31 reduces the number of obligations) and the blocking procedure finishes. It returns to the strengthenClauses procedure, which checks for further predecessors of error states to be blocked in order to eventually create the next frame. One of the most important aspects of IC3, however, is the fact that it does not exclude a single state s . Instead, it generalizes the state s into a set of states that are to be blocked (line 32). To this end, it employs a Generalization procedure depicted in Listing 2.4. Listing 2.4: Generalization algorithm in IC3 44 generalizeAndBlock ( s,n ) { 45 find minimal subclause kckof ¬ksk, s . t . 46 kF0k ∧ ¬kckis unsatisfiable 47 kFn−1k ∧ kck ∧ kTk ∧ ¬kck0is unsatisfiable 48 for ( int i =1; i≤n ; i ++) 49 kFik:=kFik ∧ kck; 50 } Employed prior to blocking the state s from Fn , it searches a minimal subclause of ¬ksk that is inductive relative to Fn−1 . Such a minimal subclause always exists, since ¬s itself is inductive relative to Fn−1 (line 30). However, the search is non-trivial since monotonicity is not given for the consecution query of relative inductiveness of the subclauses. The removal of a single literal in the subclause might destroy the consecution property although it held before. In addition, the removal might also 2.4. IC3 33 re-establish consecution although it did not hold for the subclause before removing the literal. The reason is c and ¬c0 being altered at the same time, where the removal of a literal strengthens c , but weakens ¬c . Thus, the search for such a minimal subclause is hard. Most implementations rely on two or more combined approaches. On the one hand, the manual dropping of single literals one by one can be checked with a short query to the solver. If the query returns unsatisfiable, the subclause is still inductive relative, otherwise, the dropped literal is put back in the clause. This manual removal relies on heuristics to determine the order in which literals are tried to be dropped. While this is a valid approach, it is only capable of testing the removal of one literal at a time. Using extended concepts of SAT-solving, this drawback can be reduced. In case the subclause is still inductive relative after the removal of a literal, the query is found to be unsatisfiable, which allows the extraction of an unsatisfiability core (UNSAT-Core). Such a core is used to delete all those literals of the subclause that are not needed in proving the formula unsatisfiable. The removal of these literals is a safe option if the initiation property is not violated by doing so. Using this approach, most implementations do not actually care to find the minimal subset, but in contrast search for a small one in reasonable time. Due to this non-optimality and the removal of several literals determined by the UNSAT-core, the heuristics play an important role in steering of the generalization. Having found a generalized clause kck of ¬ksk , it is conjoined to every formula kF0k up to kFnk (lines 48 and 49). This conjunction excludes the state s from the frames, as well as many more states (in case cis a strict subclause). The benefit of this generalization procedure is a fast refinement and small clauses computed in a fairly efficient way. In addition, a second procedure exists that provides for a fast refinement. The pseudocode depicting this Propagation step is shown in Listing 2.5. Listing 2.5: Propagation algorithm in IC3 51 propagateClauses( int k){ 52 for ( int i =1; i<k ; i ++) 53 for each clause kckin kFik: 54 i f (kFik ∧ kTk ∧ ¬kck0unsatisfiable) 55 kFi+1k:=kFi+1k ∧ kck; 56 } The procedure pushes learned clauses to subsequent frames whenever possible, providing strengthened frames for the next cycle and, thus, a better guided refinement. To this end, IC3 checks all clauses of each frame for relative induction. If a clause c is inductive relative to a frame Fi , it can be propagated to Fi+1 , refining Fi+1 via conjunction as depicted in line 55. Since no state outside of c can be reached from Fiwithin one transition, this refinement does not destroy the 4 properties. The propagation procedure is subject to several tricks in efficient implementations. By storing clauses in a data structure that associates them only with the largest frame with which they are conjoined, each clause is tested only once for propagation. 34 CHAPTER 2. BACKGROUND Furthermore, subsumption checks are often applied in this phase in order to filter out obsolete clauses that are not needed any longer. Correctness All these different procedures and phases maintain the four properties of the frames, such that in the end IC3 is a successful algorithm for computing inductive strengthenings. We will shortly give an intuition why these properties hold during all the phases and why the algorithm terminates for finite state transition systems. These can be found in more detail in the work of Bradley et al. [Bra11]. During the initial phase of the algorithm (lines 1 to 6), IC3 ensures that there exist no error states that are initial or reachable from an initial state by a single transition step. Thus, the first two frames F0=I and F1=ρ can be created and adhere to the four given properties. In particular, Property 1 is ensured by F0 being equal to the initial states. Property 2 is ensured in line 2 since ρ includes all initial states, while Property 3 is ensured in line 4. The last property is obviously true due to Property 2 and F1being equal to ρ. These properties are maintained during each cycle of the main algorithm (lines 7-15). They are not violated by the call of function strengthenClauses and remain intact during the call of propagateClauses as we will see below. Finally, the creation of a new frontier Fk+1=ρ adheres to the properties. Since it does not alter the other frames, it remains to show that kFkk ∧ ¬kFk+1k , kFkk∧kTk ∧ ¬kFk+1k0 and kFk+1k ∧ ¬kρk are unsatisfiable before the incrementation of k (line 14) and starting a new loop. The latter is true by definition of Fk+1 and the first one is true by Property 4 for all smaller frames. The fact that kFkk∧kTk ∧ ¬kFk+1k0 is unsatisfiable has been established by strengthenClauses(), as it ensured that no direct predecessor of an error state is included in Fk(line 18). We now consider the method strengthenClauses(). During its run, the 4 properties are preserved and when returning true, there exists no state in the frame Fk that is a direct predecessor of an error state. The method itself does not alter the frames, but however calls function blockCTIs({(s,k)}) to block the direct predecessor s of an error state in the frame Fk . This is done until no such predecessors are left. What remains to be shown is that blockCTIs successfully blocks the found CTIs while preserving the 4 properties. The function blockCTIs() works off a list of obligations until none is left. The frames are only altered when calling the function generalizeAndBlock(s, n ). This is only done when ¬s was found to be inductive relative to Fn−1 in which case it is also inductive relative to all smaller frames. The function generalizeAndBlock(s, n )searches for a minimal subclause c of ¬s that is still inductive relative. This clause is added to F1 up to Fn altering the frames and successfully blocking s from Fn . The 4 properties, however, are preserved. In particular, Property 1 still holds, as F0 is untouched and Property 4 holds due to frames being strengthened. Property 2 still holds since kF0k ∧ ¬kck is unsatisfiable (line 46) and c is added to all F1 up to Fn . Since Property 3 previously held true and relative consecution (line 47) of clause c holds, the refined frames still satisfy Property 3. Thus, the methods generalizeAndBlock, blockCTIs and strengthenClauses preserve the 4 properties for the frames. 2.4. IC3 35 In addition, the function propagateClauses also preserves these properties due to the same reasoning over relative inductiveness. Hence, in total, the 4 properties are maintained for the frames after and during the main loop, allowing the algorithm to find an inductive strengthening, if one exists. Termination The algorithm will always terminate for a finite state transition system. With the frames being a non-decreasing sequence of sets of states and the algorithm still running, meaning it did not terminate due to two frames being equal, each frame has to include at least one additional state compared to the next smaller frame. That means there can only exist |S| frames at the same time for a finite state transition system as defined in Definition 2.3.1. Thus, the main loop of the algorithm will eventually terminate, provided that the functions strengthenClauses and propagateClauses terminate. StrengthenClauses will terminate when no direct predecessor of an error state remains in frame Fk . Assuming the function blockCTIs successfully blocks each found predecessor, strengthen must terminate after at most |S| runs of its while loop. The function blockCTIs will always terminate. The list of obligations can only contain |S| × k obligations. Provided that the call to generalizeAndBlock terminates and indeed blocks the state s from frames F0 to Fn , the list of obligations will eventually be worked off or a counterexample is found. Due to the blocking, an obligation can not be found again in the same run of blockCTIs after being worked off. Thus, the method will terminate. Each call of function generalizeAndBlock terminates and successfully blocks state s in frames F0 to Fn . The reason is that only a finite number of subclauses exist and, thus, the minimal subclause can be found. Such a minimal subclause always exists, since ¬s itself is inductive relative to Fn−1 . In summary, each call of strengthenClauses will terminate. In addition, each call of the function propagateClauses terminates since k is finite and the number of clauses in a frame is finite. Summing up, all functions called by the main loop terminate and the main loop itself also terminates due to adding a new frame each cycle, of which there are only finitely many. The argumentations about termination and correctness are carried out formally and in more detail in the first paper on IC3 by Aaron Bradley [Bra11]. 2.4.2 Optimizations As mentioned above, there exists a large community of researchers trying to improve and optimize IC3 or transfer it to different domains. Some of the optimizations and improvements are specifically tailored to the domain of application (for example ternary simulation in hardware verification), while others are more general. In the following, we present and discuss some of them. Many optimizations target the method of generalization (Listing 2.4). Hassan et al. [HBS13] proposed to utilize Counterexamples to Generalization, meaning predecessor 36 CHAPTER 2. BACKGROUND states found during the generalization procedure. These are used in order to infer additional clauses that adhere to the relative inductiveness property. Thus, the approach utilizes unsuccessful tries for finding subclauses, however, it is not guaranteed that the inferred clauses are indeed helpful. In general, the optimization is evaluated as successful. Chockler et al. [Cho+11] utilize an additional SAT-query as a preliminary step to generalization. Designed for hardware verification they search for partial assignments of a CTI by encoding the transition with which the CTI is found, but negating the successor state. Due to being deterministic for the specific set of input values, no distinct successor state exists, rendering the SAT-query unsatisfiable. Chockler extracts a partial assignment of the CTI from the UNSAT-Core, thereby potentially generalizing the CTI. A similar effect is the result of ternary simulation, as proposed for use in IC3 by Een et al. [EMB11]. Using three valued logic, the effect of removing literals is propagated through the hardware circuit and in the end defines whether the removed literal is of use or not. The same paper also proposed several other optimizations, including a variation of the four properties for the frames and a variant of the algorithm that does not need the two basic checks (lines 2-5). In addition, they propose clever ways of organizing obligations, as well as the clauses in the frames. The resulting implementation, called Property Directed Reachability (PDR) proved to be superior to the original implementation and, thus, got adapted as a synonym for IC3. Other improvements use the propagation phase as starting point. Suda [Sud13] proposed to trigger the propagation of clauses only if possible. To this end, he keeps track of witnesses that hinder the propagation of a clause. Only if such a witness is not valid any more, the propagation of the clause is tried. The approach seems to work well. Other variants, however, did not prove to be of substantial value, as can for example be seen in the original paper by Bradley [Bra11]. He proposed a variation of the blocking procedure that searches a subclause inductive relative to a larger frame than Fn−1 (cf. Listings 2.3 and 2.4). Its performance, however, was worse for specific hardware designs due to being unable to use the UNSAT-Core. In summary, a lot of research has been successful to various extend in improving and optimizing IC3 itself. There also exists work on the reusage of verification results as is of interest in this thesis. With hardware models changing often during the design process, Chockler et al. [Cho+11] utilize a previously computed inductive strengthening for the re-verification of the changed model. They apply an optimized SAT-encoding in order to find a subset of clauses of the inductive strengthening that are still inductive in the changed model. The found (inductive) clauses are then injected in the re-verification in order to speed it up. In addition to this incremental way of using IC3, the algorithm has also been applied in completely different contexts and domains. Some work was done on 2.4. IC3 37 transferring IC3 to domains distinct from hardware verification and on combinations of IC3 with other techniques. Hassan et al. [HBS12] utilize the idea of IC3 being incremental and inductive for CTL-model checking. They successfully build a property-directed abstracting model checker for CTL with fairness. Baumgartner et al. [Bau+12] apply IC3 in the hardware verification domain in order to compute abstractions. They analyze the frames in an incomplete run of IC3 using heuristics in order to obtain priorities for state variables. On the basis of these priorities, a localization abstraction refinement is guided. Another approach directly combines IC3 with abstraction and utilizes CTIs for refinement. In contrast to the original CEGAR approach, the technique of Birgmeier et al. [BBW14] utilizes single states (the CTIs) for refinement of the abstraction, while the original approach uses counterexample traces. The focus on CTIs enables two distinct points for triggering the refinement of the abstraction and, in addition, enables a choice of delaying the refinement. More general work examines IC3 from a broader perspective. Bayless et al. [Bay+13] introduce the concept of SAT modulo SAT, which works similar to lazy SMT-solvers. They utilize the concept for their implementation of IC3, which proves to be successful. IC3 is also applied as coverability check of well structured transition systems, in particular petri nets. Kloos et al. [Klo+13] propose an IC3-based algorithm for this task. Their implementation is SAT-based with predecessor and relative inductiveness computations being directly applied on the petri net. The concepts of IC3 have also been transferred to domains that require other concepts than SAT-solving. For example, the application of IC3 for game solving (Morgenstern et al. [MGS13]) requires a QBF-solver. As a second example, the usage of IC3 for planning problems (Suda [Sud14]) sticks out with the absence of a solver. Instead, Suda delegates the tasks of the solver to a specific planning procedure. In general, most approaches that do not rely on SAT-solving apply the concept of SMT-solving. 2.4.3 IC3 with SMT Cimatti et al. were the first to combine IC3 with the concept of SMT-solving in order to model check software [CG12]. Apart from changes to the algorithm in order to support software model checking based on the control-flow graph, they apply a quantifier elimination procedure in linear real arithmetic to cope with the potential infinity of CTIs in a single blocking phase. Other approaches try to be less theory-specific. A combination of IC3 using SMT with abstraction also proposed by Cimatti et al. [Cim+14] allows to handle a wide range of background theories. During the run of the algorithm an implicit abstraction is computed that is refined, whenever a spurious counterexample is found. The work can, thus, be seen as an instance of CEGAR. 38 CHAPTER 2. BACKGROUND Cimatti also applied IC3 with SMT in order to synthesize parameters [Cim+13a]. Relying on a quantifier elimination procedure, the algorithm searches for parameter combinations that allow counterexample traces. Gradually excluding these combinations, the tool in the end returns a set of safe parameter combinations. With timed systems in mind, we are specifically interested in applications of IC3 using linear real arithmetic, of which some exist. Hoder et al. [HB12] generalized the PDR algorithm for usage with nonlinear transformers (used, e.g., for modeling software with procedures), in which counterexamples unfold to trees instead of paths. In the same work they apply PDR for linear real arithmetic. Their work applies interpolation in the generalization procedure in order to ensure decidability of the reachability of timed push-down systems. Bjørner et al. extend the previous concept [BG14]. They propose three variations of the generalized PDR algorithm for linear real arithmetic. The first one is basically a redefinition of the pure generalized PDR algorithm applying quantifier-elimination-based projection to extract CTIs, while the other two restrict themselves to find specific inductive invariants. In the second algorithm, the frames are defined as convex polyhedra, meaning conjunctions of linear inequalities. Thus, the algorithm is able to compute a convex polyhedron as inductive invariant. Contrary to this approach, the authors also present a variant of generalized PDR that is able to compute co-convex invariants, denoting the complement of a convex polyhedron. The latter two techniques are, however, not suited for timed automata verification as they do not reason about discrete parts, e.g., locations of a timed automaton. The approaches mentioned prior to these two include such capabilities. However, their usage of interpolation and quantifier elimination is a generic mechanism. In contrast, we expect more specific techniques designed for timed automata to be better suited. The combination of discrete and continuous components in a timed automaton permits adjusted mechanisms, which is done in the approach presented below. 2.4.4 IC3 for TA Kindermann et al. [KJN12b] applied IC3 specifically tailored to timed systems. As explained before, this design decision allows several general optimizations of IC3. His approach, however, was not competitive. The infinity of clock valuations inherent in continuously timed systems poses the main challenge to IC3. When lifting the algorithm to SMT by encoding the system via SMT-formulae, the strengthen phase is no longer guaranteed to terminate. The blocking phase blocks the CTI, which is a single concrete state of the infinite transition systems as defined in Definition 2.1.10. Since there possibly exist infinitely many states all satisfying the query in line 18, the strengthen phase might never terminate or only if the generalization blocks all of them by chance. The same arguments can be used in order to explain a possibly infinite run of the blocking phase, where also infinitely many CTIs might exist. Thus, modifications to the algorithm are needed to ensure termination. To this 2.4. IC3 39 end, the decidability result of reachability properties for timed automata might have led the way for the approach of Kindermann et al. [KJN12b]. With decidability being proven via a finite, reachability equivalent abstraction, the idea of composing all clock valuations that are indistinguishable for the timed automaton seemed like a good candidate. Thus, the region abstraction was employed due to being finite and easily computable for a single state. Kindermann uses the original IC3 approach, but encodes the timed system via SMT-formulae. The algorithm is run as usual, but whenever a CTI is extracted, a specific technique is applied. As in the original approach, he extracts the concrete state from the satisfying SMT-interpretation. Afterwards he applies an abstraction procedure that replaces the concrete clock valuation of the concrete state with its unique, surrounding region in order to form an abstract state used as CTI. With only finitely many regions, the abstraction eliminates the risk of possibly having infinitely many CTIs, ensuring the termination of the algorithm. Although the surrounding region of a concrete clock valuation is efficiently computable, the region abstraction is not well suited to be used in practical application, as has been explained before. The abstraction is very fine grained and the number of regions heavily depends on the constants used in the timed automaton. The combination of these two characteristics ensures a huge number of regions, rendering the algorithm ineffective, in particular for large constants. Kindermann’s evaluation of his approach showed a good scalability in terms of model size, but does not deal well with large constants. While being a nice theoretical concept, the combination of IC3 with the region abstraction for timed systems proved to be of no practical value. Kindermann proposed some specific optimizations generalizing the CTI upfront before the generalization procedure of IC3 was applied. However, these suggestions could not establish practicality. Yet, the basic idea has shown to be very interesting since it allows to benefit from future, general IC3 improvements and optimizations. For this reason, our approach presented in Chapter 3 builds on it. Summing up, the work closest to ours is the one of Kindermann et al. [KJN12b] proposing to use IC3 with the region abstraction for timed system verification. In addition, the work of Chockler et al. [Cho+11] is closely related to our objective of handling reconfigurations. In Chapters 4 to 6 we will pick up this concept in order to improve the verification of safety properties for reconfigured timed models. 3 Timed Automata Verification via IC3 with Zones Many of today’s systems are safety critical, which expresses the need for their correct functioning at all times. Otherwise, undesired behavior could result in a loss in value, e.g., when a production is stopped, or even be a thread to life and physical condition. As a countermeasure, model-based design processes introduce a structured procedure in which models of the systems are built. Then, formal methods are employed to check whether specified properties are fulfilled. With an increasing number of systems relying on real-time communication, or being real-time operating system, there exists a demand for timed models and verification. As detailed in the previous chapter, networks of timed automata are amongst the most important modeling formalisms that incorporate time. With roughly 25 years of research, this modeling formalism is well understood and there exist many sophisticated algorithm for the verification of safety properties for these models. However, these algorithms reach their limits for large models, in particular due to an enormous need of memory during verification. In the following, we will employ the IC3 algorithm for the verification of safety properties in the domain of timed automata. IC3 originates from hardware verification, in which it has proven to be extremely efficient, both regarding time and memory requirements. We aim for it to be of value also in the domain of timed automata. Its huge success for hardware verification has led to a large amount of optimizations and, in addition, it has been successfully transfered and applied in many other, very diverse domains. Its first usage in the domain of timed automata by Kindermann et al. [KJN12b], however, remained unsatisfying, as it was not competitive. In this chapter, we introduce our concept combining the IC3 algorithm with the zone abstraction in order to verify safety properties for networks of timed automata [IW14]. We first present the basic components, i.e., the SMT-encoding and zone computation, and afterwards explain their integration in the IC3 algorithm. Lastly, we present the promising results of numerous experiments. We discuss for which 41 48 CHAPTER 3. TIMED AUTOMATA VERIFICATION VIA IC3 WITH ZONES In addition, the extraction of the taken edges needed for the computation of the CTIs might be more difficult. Thus, we compute the combinations of edges, as defined in Def. 2.1.11. As described in the semantics, only those edges of the product automaton can be taken that are not synchronized (marked by the synchronization symbol e ). We encode these edges by enforcing the source and target locations of those timed automata, in which the edges are taken. Furthermore, we encode the constraints and integer assignments and resets of clocks. In addition, we ensure all unused clock, integer and location variables to keep their values, meaning they have the same value in their unprimed and primed versions. We first describe how integer assignments and resets of clocks are encoded. 3.1.6 Encoding of Clock and Integer Updates Encoding updates on the clocks and integer variables inherently makes use of both the unprimed and primed versions of the variables, representing the current and the next state values, respectively. First, we define the encoding of integer assignments. Encoding of Integer Assignments As mentioned before, we can combine each sequence of assignments (Definition 2.1.5) into a sequence, in which the order does not matter, since each integer variable exists at most once in a left hand side of an assignment. This fact results in a simple encoding using conjunction to combine the assignments without the need for intermediate steps. Note, however, that the encoding of a sequence, in which the order is essential, can easily be done using auxiliary variables and intermediate steps. The following definition shows the simple encoding. Definition 3.1.10. Let an integer assignment ω be given as defined in Def. 2.1.5. The SMT-formula kωkencoding it depends on the assignment. If ωequals •iv :=nfor some integer variable iv ∈ IV and n∈Z, then kωk:=kivk0=n, •iv :=iv +nfor some integer variable iv ∈ IV and n∈Z, then kωk:=kivk0=kivk+n, •ω1;ω2for some integer assignments ω1and ω2, then kωk:=kω1k ∧ kω2k, •true, then kωk:=true. For an assignment true , the same arguments applies as for an invariant true . It is ignored and, thus, all integer variables are to keep their value. This process of keeping the value is encoded separately (as kivk0=kivk ) in each of the edges for all integer variables iv ∈ IV that are not changed by the assignment. We illustrate the encoding with the following example. 3.1. SMT-ENCODING 49 Example 3.1.11. Consider again the Fischer model as depicted in Figure 3.1. The integer assignment id := 0; cnt :=cnt − 1 can be seen on the edge between location l3 and l0 in each of the automata. With integer variable id having identifier 0 and cnt having identifier 1, the integer assignment is encoded as kωk:= (int0 0=0)∧(int0 1= (int1−1)). The encoding is straight-forward for the integer assignments. However, clock updates can not be encoded this way due to always considering the combination of an edge-transition with a subsequent time elapse step. To this end, we create an additional real-valued variable δ denoting the time elapse after the edge has been taken. Encoding of Clock Resets Given the set R⊆C of clocks to be reset, the update of each clock is encoded dependent on it being an element of R or not. All members are reset to value 0, while the remaining clocks keep their value. Afterwards all clock values are increased by a time delay step, encoded as the addition of a real valued variable δ. Formally, the update for each clock c∈Cis encoded as kck0=δif c∈R, kck0= (kck+δ)else. Using the above encodings, we can finally formalize the encoding of edges. 3.1.7 Encoding of Edges When encoding the edges of an NTA, we distinguish between the encoding of edges that originate from synchronization and those that don’t. We start with the latter, denoting such edges that can be found in single timed automata in the network, marked by symbol e, meaning no synchronization takes place. Unsynchronized Edges These edges are related only to a single timed automaton Ai ( i∈ { 1,..., n} ) in the network NTA =hA1 ,..., Ani . Thus, they do not consider the locations of the other timed automata, as well as their local clocks. These values do not matter, as they are unchanged when the edge is taken (not taking into account successive time elapse). Hence, our encoding does not need to compute the product automaton with all its combinations of locations. Instead, we demand Ai to be in the source location before taking the edge and to be in the target location afterwards. In addition, the clock and integer constraints have to be met, as well as the reset of clocks and the integer assignments. The encoding is presented in detail below. Definition 3.1.12. Let a network of timed automata NTA =hA1 ,..., Ani be given as in Def. 2.1.11. Each unsynchronized edge e= (l1e,φ,ψ,ω,R −−−−−→ l2)∈Ei of each timed automaton Ai(i∈ {1, . . . , n}) is encoded as follows. 50 CHAPTER 3. TIMED AUTOMATA VERIFICATION VIA IC3 WITH ZONES kek:=kl1ki∧ kl2ki0 ∧ kφk ∧ kψk ∧ kωk ^ c∈R kck0=δ^ c∈C\R kck0=kck+δ ^ j∈{1,...,n} j6=i mx(Aj) ^ m=0 lj m 0=lj m ^ iv∈IV,iv/∈ω kivk0=kivk We explain the encoding in the following. The first line encodes the automaton Ai being in location l1 before the edge is taken and in l2 afterwards, which is encoded via the primed variables. The next line demands the constraints ψ and φ to hold before the edge is taken and the assignment ω being applied to the integer variables. The third line demands the clocks in R to be reset, while all others keep their value. In addition, a time elapse of δ is encoded, where the requirement of the delay being nonnegative ( δ≥ 0) is encoded separately, together for all edges. Finally, the locations of the timed automata other than Ai are preserved, as well as the values of the integer variables that are not updated in the assignment ω. We illustrate the encoding with the following example. Example 3.1.13. Consider the Fischer model as depicted in Figure 3.1. We show the encoding of the edge e leading from l2 to l3 (with identifiers 2 and 3, respectively) in the first automaton. It requires A1to be in the respective locations before and after the transition, encoded as kl2k1:=l1 1∧ ¬l1 0 and kl3k0 1:=l1 1 0∧l1 0 0 . Furthermore, it requires integer variable id , encoded as int0 , to have value 1 ( kψk:=int0= 1) and local clock c of A1 , encoded as c1 0 , to be of value larger than 1024 ( kφk:=c1 0> 1024). The integer assignment ω increments the variable cnt by one, encoded as kωk:= int0 1= (int1+ 1 ) . All other variables keep their value during the transition step. The entire encoding looks as follows. kek:=l1 1∧ ¬l1 0∧l1 1 0∧l1 0 0 ∧(c1 0>1024)∧(int0=1)∧(int0 1= (int1+1)) ∧(c1 0 0= (c1 0+δ)) ∧(c2 0 0= (c2 0+δ)) ∧(l2 0 0=l2 0)∧(l2 1 0=l2 1) ∧int0 0=int0 As explained before, our encoding does not need to compute any product of locations and is, thus, very scalable. The same holds true for the encoding of synchronized edges, which we describe below. However, we need to compute all combinations of synchronized sender and receiver edges, which results in a bad scalability for models with many sender and receiver edges synchronized via the 3.1. SMT-ENCODING 51 same channel. As noted above, a different kind of encoding without the need for such a computation might be feasible, but results in an encoding way more complex with some sort of signaling between sender and receiver that ensures exactly one edge of each kind. Thus, we compute the combination of synchronized edges upfront end encode them similar to the previous encoding. The main differences are the usage of two source and target locations, as well as two constraints and assignments due to the sender and receiver edges belonging to two distinct timed automata. In the following, the encoding is formally defined. Definition 3.1.14. Let a network of timed automata NTA =hA1 ,..., Ani be given as in Def. 2.1.11. Each synchronized edge e combined from sender edge es= (l1a!, φ1,ψ1,ω1,R2 −−−−−−−−→ l2)∈Ei and receiver edge er= (l3a?, φ2,ψ2,ω2,R2 −−−−−−−−→ l4)∈Ej of timed automata Aiand Aj(i6=j∈ {1, . . . , n}) is encoded as follows kek:=kl1ki∧ kl3kj∧ kl2ki0∧ kl4kj0 ∧ kφ1k ∧ kφ2k ∧ kψ1k ∧ kψ2k ∧ kω1;ω2k ^ c∈R1∪R2 kck0=δ^ c∈C\(R1∪R2) kck0=kck+δ ^ h∈{1,...,n} h/∈{i,j} mx(Ah) ^ m=0 lh m 0=lh m ^ iv∈IV,iv/∈ω1;ω2 kivk0=kivk Using these encodings of the edges, we can encode the transition relation. It is explained below. 3.1.8 Encoding of Transition Relation The transition relation consists of all unsynchronized edges and the combined synchronized ones. When the transition relation is applied, the current state in the concrete transition system is changed according to the taken edge. Thus, an edge must be taken, which is encoded as a disjunction of the formulae representing the edges. The variable δ modeling the elapsed time is used within all the encodings of the edges and, thus, the requirement that a nonnegative amount of time has passed is encoded together once for all edges. Definition 3.1.15. Let a network of timed automata NTA =hA1 ,..., Ani be given as in Def. 2.1.11. Let {e1 , . . . , em} be the set of unsynchronized edges and combined synchronized edges as in the previous definitions. The transition relation describing the application of one of them is encoded as kTransk:=(ke1k ∨ · · · ∨ kemk)∧δ≥0. 52 CHAPTER 3. TIMED AUTOMATA VERIFICATION VIA IC3 WITH ZONES All the above definitions are employed to encode the concrete semantics of a network of timed automata as explained. For our verification approach, however, the safety property must also be encoded as SMT-formula. This encoding is defined below. 3.1.9 Encoding of Safety Property A safety property is defined as a conjunction of negations of error state specifications. Each error state specification is defined as a triple of partial location vector, clock constraint and integer constraint. We have described above, how all these parts are encoded. They are simply combined via conjunction to encode an error state specification. Definition 3.1.16. Let a network of timed automata NTA =hA1 ,..., Ani be given as in Def. 2.1.11. Let err = (¯ l , φ , ψ) be an error state specification as given in Definition 2.1.13. It is encoded using the above definitions as kerrk:=^ j∈{1,...,n} ¯ l[j]6=∗ k¯ l[j]kj∧ kφk ∧ kψk, where the encoding of the partial location vector encodes only those locations that are specified. In addition, constraints φand ψare discarded, if they specify true. As stated before, the encoding of the safety property is simply the conjunction of negations of the error state specifications. We formally define it in the following. Definition 3.1.17. Let a network of timed automata NTA =hA1 ,..., Ani be given as in Def. 2.1.11. Let the safety property ρ=G(¬err1∧ · · · ∧ ¬errx) be given specifying that no reachable state should satisfy one of the error state specifications err1 to errx . It is encoded as kρkas follows. kρk:=¬kerr1k ∧ · · · ∧ ¬kerrxk We illustrate the encoding with the following example. Example 3.1.18. Consider again the Fischer model as depicted in Figure 3.1. It models the Fischer mutual exclusion algorithm that ensures only a single process to be in a critical section. The critical section is modeled as location l3 and the number of processes in the critical section is counted via integer variable cnt . Let cnt > 1 be the error state specification considered here. It specifies that more than a single automaton is in its critical section at the same time. The safety property of interest denotes that no such error state can occur, formally ρ:=G(¬(cnt > 1 )) . It is encoded as kρk=¬(int1>1). Finally, all formulae needed are explained and defined. We briefly summarize their usage within IC3 below. To this end, we give an overview over the queries issued to the SMT-solver. 3.1. SMT-ENCODING 53 3.1.10 Usage of the Encodings in the Queries As stated before, the SMT-formula encoding the transition relation, as well as those for the initial states or the safety property rely on the combination with the unprimed and primed invariant formulae. In consequence, we create these formulae modularly in order to combine them when needed. We briefly recall the queries issued by IC3 (upper formula) and show how they are build using our encoding (lower formula). • (An error state is initial.) kIk ∧ ¬kρk: kInitk ∧ kInvark ∧ ¬kρk • (A predecessor of an error state is initial.) kIk ∧ kTk ∧ ¬kρk0: kInitk ∧ kInvark ∧ kTransk ∧ kInvark0∧ ¬kρk0 • (A predecessor of an error state is a member of Fk.) kFkk ∧ kTk ∧ ¬kρk0: kFkk ∧ kInvark ∧ kTransk ∧ kInvark0∧ ¬kρk0 • (A predecessor of state s that is distinct from s is a member of Fn−1.) kFn−1k ∧ ¬ksk ∧ kTk ∧ ksk0: kFn−1k ∧ ¬ksk ∧ kInvark ∧ kTransk ∧ kInvark0∧ ksk0 • (An initial state is a member of ¬c.) kF0k ∧ ¬c: kF0k ∧ kInvark ∧ ¬c • (A predecessor of a state in ¬cis a member of cand of Fn−1.) kFn−1k ∧ c∧ kTk ∧ ¬c0: kFn−1k ∧ c∧ kInvark ∧ kTransk ∧ kInvark0∧ ¬c0 • (A predecessor of a state in ¬cis a member of Fi.) kFik ∧ kTk ∧ ¬c0: kFik ∧ kInvark ∧ kTransk ∧ kInvark0∧ ¬c0 The above formulae encode states and transitions in the concrete transition system, as explained in Definition 2.1.10. It might be feasible to encode an abstraction of the clock valuation space directly, e.g., by introducing variables for bounds of clock valuations. However, the encodings would most probably grow far more complex. In particular, the transition relation encoding would do so and, thus, slow down the generalization step. Our encoding refrains from introducing this additional complexity and, instead, favors an auxiliary step outside the scope of IC3’s generalization procedure. This additional step is vital for our approach. Since our encoding represents a concrete transition system with clocks having values from R≥0 , there might be infinitely many satisfying interpretations to a satisfiable query. This infinity poses 54 CHAPTER 3. TIMED AUTOMATA VERIFICATION VIA IC3 WITH ZONES a problem, especially when considering the queries asking for counterexamples to induction (CTIs). There might exist infinitely many satisfying interpretations and, in consequence, infinitely many CTIs, e.g., within one run of strengthenClauses. Hence, the algorithm would have to exclude infinitely many CTIs for termination. Even when taking into account the generalization procedure, termination can not be ensured. This is due to the fact, that the generalization algorithm is only capable of deleting literals (for example c= 1.771). Tackling this problem by altering the generalization algorithm to shift values is hardly feasible. Thus, we employ an abstraction in order to ensure termination. First, we need to obtain the concrete states that the solver has computed in form of a satisfying interpretation. This step, called state extraction, is detailed below. 3.2 State Extraction Executing the IC3 algorithm using an SMT-solver with the above encoding results in CTIs being concrete states. Each satisfying interpretation is inspected to extract values for the location variables, clock variables and integer variables. These represent the clock valuation, integer valuation and locations of a state in the concrete transition system (or two states - predecessor and successor - in case of an encoded transition step). The clock and integer valuations can be extracted directly, however, the locations need to be computed from the boolean values of the location variables. The boolean values represent the identifier of the location encoded as integer value in binary form. The extraction of the concrete state is exemplified in the following. Example 3.2.1. Let the network of timed automata be given as depicted in Figure 3.1. The query kFkk ∧ kInvark ∧ kTransk ∧ kInvark0∧ ¬kρk0 asks the solver for a predecessor state (in Fk ) of an error state. Consider the following part of a satisfying interpretation returned by the solver. (de f ine −f un int0() Int 1) (de f ine −f un int1() Int 1) (de f ine −f un l1 1() Bool true) (de f ine −f un l1 0() Bool f alse) (de f ine −f un l2 1() Bool true) (de f ine −f un l2 0() Bool f alse) (de f ine −f un c1 0() Real 1025.0) (de f ine −f un c2 0() Real 1.0) . . . Note, that the format of the satisfying interpretation depends on the used solver. The presented interpretation represents only values for the predecessor state. We extract the following state: Both integer variables int0 and int1 have value 1 and, thus, the integer valuation vi for the integer variables of the model is set accordingly ( vi(id) = 1, vi(cnt) = 1). The extraction of the clock valuation vc is done in exactly the 3.2. STATE EXTRACTION 55 same way ( vc(c1) = 1025.0, vc(c2) = 1.0), where c1 and c2 denote clock c in automata A1 and A2 , respectively. The extraction of the locations is a bit more involved. Taking the values for the boolean variables, we build the binary representations of the identifiers. In this example, both binary representations are 10 representing location l2for A1and A2. As explained above, the concrete clock valuation poses a potential thread to the termination of the algorithm. In the following, we show an example having infinitely many such valuations for CTIs all taking the same edge to an error state. Example 3.2.2. We consider the same example as above with query kFkk∧kInvark ∧ kTransk ∧ kInvark0∧ ¬kρk0 asking for a predecessor state (in Fk ) of an error state. The satisfying interpretation represents an edge transition from location l2 to l3 in the first timed automaton, while the second one keeps its location l2 . The integer valuation changes from vi(id) = 1, vi(cnt) = 1 to vi0(id) = 1, vi0(cnt) = 2. The respective concrete clock valuation found by the solver is vc(c1) = 1025.0, vc(c2) = 1.0 and does not change ( vc=vc0 ) with δ= 0. It is easy to see, that the locations and valuations enable the given edge with the given successor state being an error state, i.e., satisfying cnt > 1. Clearly, there exist infinitely many other satisfying interpretations for the query: Keeping all the above values, but changing vc(c1) to any arbitrary value strictly larger than 1024.0. Figure 3.2 shows the computed concrete clock valuation (marked as x), as well as the other valuations that could be used in a satisfying interpretation (marked gray). c1 10241023 . 1 2 1025 ... ... 0 c2 . . . . .. . . . .. . . . .. . . . Figure 3.2: An infinite number of satisfying interpretations can exist: When changing the clock valuation found by the solver for Example 3.2.2 (marked as x) to any other one of those marked gray, the respective interpretation still satisfies the issued query In 2012, Kindermann et al. [KJN12b] proposed a solution to circumvent infinitely many CTIs by using the region abstraction. They extract the concrete state, as shown above, and afterwards compute the region surrounding the found clock valuation. The computation is straight-forward, in particular, due to each concrete clock valuation belonging only to a single, unique region. This region is used in lieu 56 CHAPTER 3. TIMED AUTOMATA VERIFICATION VIA IC3 WITH ZONES of the concrete clock valuation forming an abstract CTI. The essence of his approach is that termination is ensured due to the fact that there exist only a finite number of distinct regions. Thus, when blocking an abstract CTI, none of the concrete clock valuations included in the entire region can occur again as CTI (for a specific frame) in the current cycle of the strengthenClauses procedure. Accordingly, with abstract CTIs being blocked, only a finite number of distinct frames can be created until two of them are found to be equal (or a counterexample trace is found). As a result, termination is guaranteed. Kindermann examines his approach thoroughly leading to the conclusion that it scales similar to the state of the art tool Uppaal, but is not competitive to it due to larger runtimes in general. The main reason for the performance issues is the use of the region abstraction. Although being finite, the number of CTIs may still be enormously large due to exponential growth of the employed abstraction regarding time constants and clocks. Thus, the approach is irrelevant in practice. In general, however, Kindermann’s approach points out a valuable direction. By applying finite abstraction, IC3 can be utilized for the verification of timed automata. Such an abstraction should be coarse and efficiently computable in order to be better suited for practical purposes. In our approach, detailed below, we apply the zone abstraction. We believe that this abstraction is particularly suitable for application in IC3 due to its properties. It is coarser than the region abstraction, it is finite since a zone is the union of regions and there exist sophisticated algorithms for computation and manipulation of zones. Even though it is coarse, it is exact enough to describe exactly all those clock valuations that reach a specific zone of a successor state via the same edge. Note, that none of the problems of storing disjunctions of zones occurring in other approaches (see the related work in Chapter 2) are present in the IC3 approach. However, applying the zone abstraction is not as straight-forward as the region abstraction, since there is no unique surrounding zone for each clock valuation. We explain this issue and our solution in the following. 3.3 Zone Abstraction Our SMT-formulae as shown above encode the concrete semantics of a timed automaton. The states extracted from satisfying interpretations are, thus, concrete states with a single clock valuation. Unlike in Kindermann’s approach, one can not simply compute a surrounding zone for such a clock valuation as there might exist several surrounding zones. We exemplify the ambiguity in the following example. Example 3.3.1. Let the set of clocks be given as C={c1 , c2} . A concrete clock valuation vc extracted from a satisfying interpretation of a query might contain the values vc(c1) = 1.5, vc(c2) = 0.75. It is depicted in Figure 3.3 marked as x , together with several surrounding zones. Each such zone is a convex union of clock valuations (defined as a clock constraint) including the found clock valuation. Some of these zones are very fine grained and some are extremely coarse. The difficulty here is to chose the right one. 3.3. ZONE ABSTRACTION 57 c1 3 c2 21 1 2 3 (a) The zone c1≥1∧c2≤1∧c1−c2≤1 c1 3 c2 21 1 2 3 (b) The zone c1≤2∧c2−c1≤1 c1 3 c2 21 1 2 3 (c) The zone true Figure 3.3: A concrete clock valuation, as extracted from a satisfying interpretation of an SMT-query, might be included in numerous surrounding zones with different size We search for a zone that includes the concrete valuation found by the solver, and is as large as possible, while permitting only relevant behavior. The last two properties are opposed, but reasonable. A zone that is too small may result in impracticality of the approach, while a zone that is too large would break the IC3 algorithm. For illustration consider computing a zone that equals the region surrounding the concrete clock valuation. Clearly, this choice results in impracticality due to being too fine grained. It depicts exactly the approach proposed by Kindermann et al. [KJN12b]. On the other hand, a zone true allowing all valuations would be too coarse and disallow the selective blocking of specific clock valuations and, in consequence, break the IC3 algorithm. We denote behavior as relevant, if is analog to the one found via the SMT-query, meaning the same edge is taken with the same error state or CTI as successor. Thus, the zones we are interested in contain exactly those clock valuations that enable the same edge and reach the same (abstract) successor state as the clock valuation found by the query. Due to the abstraction of the found concrete clock valuation into a zone, the IC3 algorithm no longer deals with concrete states as CTIs, but with abstract states. We denote these states as abstract CTIs, as opposed to the previously used concrete CTIs. Abstract CTIs are abstract states as defined below. Definition 3.3.2 (Abstract State) . Let there be given a network of timed automata NTA =hA1 ,..., Ani as in Def. 2.1.11 with concrete semantics TS = (S , s0 , →) . The set of abstract states is defined as Sa=L×Φ(C)×Ψ(IV) . An abstract state sa= (l , φ , ψ)∈Sa denotes the set of concrete states {(l , vc , vi)∈S|vc|=φ∧vi|=ψ} . By taking into account the definition of safety properties and abstract CTIs, it is easy to formalize the above intuition of the largest zone with relevant behavior. 64 CHAPTER 3. TIMED AUTOMATA VERIFICATION VIA IC3 WITH ZONES integer invariant exists for the predecessor location, the above constraint is returned as depicted. Similarly, the computation of clock constraints includes clock invariants, guards and resets. It entirely relies on manipulations of difference bound matrices representing the involved zones. Listing 3.4: Algorithm: Computing the weakest precondition of integer constraints 93 wpClocks ( l , e , l ’ , φ’){ 94 / / i n t e r s e c t i o n with c l o c k i nv a ri a n t o f l ’ 95 φ:=and(φ0,Invc(l ’ )) ; 96 / / backwards computation using edge e 97 φ:=backwards(l,l0,e,φ); 98 / / i n t e r s e c t i o n with c l o c k i nv a ri a n t o f l 99 φ:=and(φ,Invc(l)) ; 100 return φ; 101 } Before using the backwards computation algorithm as explained in Subsection 3.3.1, the algorithm limits the allowed clock valuations according to the clock invariants of location l0 . To this end, the intersection of the DBMs representing both zones is build. Subsequently, backwards computation is employed as defined in Definition 3.3.4 based on edge e . The result is the set of clock valuations that enables the clock guard of edge e , whose application leads to a valuation, which respects the clock invariant of l0 and is included in the successor’s zone. Finally, this set is intersected with the clock invariants of location l in order to include only valuations respecting the predecessor’s invariants. For illustration, we again extend the above example. Example 3.4.3. Consider the same situation as in the previous example. The found error specification includes no specified clock constraints and, in consequence, the successor zone includes all valuations. The extracted successor locations are (l3 , l2) and the predecessor locations are (l2 , l2) with the clock constraint c1> 1024 restricting the application of the taken edge. Applying the procedure wpClocks results in the following computation. The intersection with the successor’s clock invariant does not alter the set of valuations, as no such invariant exists. Then, the past is computed, which still includes all clock valuations. The application of free and reset is also without any effect, since no clocks are reset. Afterwards, the zone is restricted to only include clock valuations respecting the predecessor’s clock invariant and the clock constraint of the edge ( c1> 1024). Thus, after the application of procedure wpClocks , the resulting set of clock valuations can be specified by constraint c1>1024. In summary, both procedures computing the sets of predecessor valuations are designed to include the maximal sets of valuations that enable edge e while reaching 3.4. ALGORITHM 65 a successor valuation as specified by φ0 and ψ0 . Thus, they are extremely important, both related to efficiency and also termination of our approach. They are likewise used in the blockCTIs procedure whenever the contained query is satisfiable and a predecessor of a CTI needs to be computed. In contrast to the above case using the error state specifications, no search of a successor state is necessary here, since it is known in form of an abstract CTI that already includes a zone and integer constraint. These informations are, thus, exploited to compute the predecessor’s constraint and zone. Listing 3.5 shows the changed pseudocode. Listing 3.5: Algorithm: Excluding states from the frames in IC3 for timed automata 102 blockCTIs ( Set Q) { 103 while(Q6=∅) { 104 / / l e t abstract CTI sa=( l ’ , φ0,ψ0) 105 get (sa,n ) ∈Q with smallest n; 106 i f (kFn−1k ∧ ¬ksak ∧ kTk ∧ ksak0unsatisfiable) 107 Q : = Q\{(sa,n ) } ; 108 generalizeAndBlock(sa,n) ; 109 else i f (n−1==0) 110 / / found counterexample 111 return f alse ; 112 else 113 / / e x t r a c t from s a t i s f y i n g i n t e r p r e t a t i o n 114 concrete predecessor st ate t =( l , vi,vc) ; 115 / / e x t r a c t from s a t i s f y i n g i n t e r p r e t a t i o n 116 taken edge e ; 117 integer constraint ψ= wpIntegers ( l , e , l ’ , ψ0); 118 clock constraint φ= wpClocks ( l , e , l ’ , φ0) ; 119 combine into abstract CTI ta=( l , φ,ψ) ; 120 Q : = Q ∪{ ( ta,n−1 ) } ; 121 } 122 return true ; 123 } As can be seen, the same mechanisms are employed in blockCTIs in order to compute the predecessor state. With the successor state being an abstract CTI, its zone and integer constraints must have been previously computed and we can simply reuse them. This is the only difference to the above case located in the procedure strengthenClauses , in which we previously had to make an effort to find an abstract successor state. The computation and usage of our abstract states serves as means able to ensure termination of the algorithm. However, there exist models for which even this concept can not guarantee it. We will see reasons for this in the following subsection, where we analyze and prove termination under certain restrictions to the models. 66 CHAPTER 3. TIMED AUTOMATA VERIFICATION VIA IC3 WITH ZONES 3.4.1 Termination In Chapter 2, we illustrated the termination guarantee for the original IC3 algorithm. Given that the model is finite, there exist only finitely many states. Since the frames are sets of states and are required to be distinct, there can only be a finite number of frames. The rest of the argumentation is about each procedure call terminating eventually and about progress, meaning at least one of the frames is refined after the blocking phase. In the case of our modified IC3 algorithm for timed automata using Zones, a similar reasoning can be applied, but encounters a couple of problems. The most obvious challenge concerning the infinite state transition system of a timed automata is solved using the Zone abstraction. Each abstract CTI includes a zone instead of a single, concrete clock valuation. When using backwards computation, only finitely many such zones can occur for a given timed automaton as they are unions of regions [Bou09]. Thus, the CTIs in our algorithm can only include one of these finitely many zones. In addition, they can only contain one of finitely many locations. In combination with a finite number of sets of integer valuations encoded in the integer constraints, our CTIs are of finite quantity. The generalization procedure taking place after CTI computation can not destroy finiteness, since it can only delete some of the literals. The result would be a set of locations with an enlarged zone and enlarged set of integer constraints. Hence, the same argumentation holds true as for the original algorithm, stating that there can only be finitely many different frames and, thus, the algorithm will terminate eventually. Theorem 3.4.1. Let a network of timed automata NTA =hA1 ,..., Ani be given as in Def. 2.1.11. If the set of backwards reachable valuations for the integer variables IV is finite, then the presented algorithm IC3with Zones terminates. However, the presumption that there exists only a finite number of sets of integer valuations in a CTI may be incorrect. This difficulty comes from integer assignments iv :=iv +n for some iv ∈ IV and n∈Z\ { 0 } . Whenever a cycle is present in the timed automaton that is able to repeatedly increase or decrease the valuation of an integer variable, there might exist an unbounded number of CTIs. It might occur that these are all ruled out by generalization and the algorithm terminates, but it can not be guaranteed. Thus, the presence of such cycles destroys the guarantee of termination of our modified IC3 algorithm. Contrary, the absence of such constructs inducing infinitely many sets of integer valuations guarantees termination. The following theorem formalizes the above illustration. Theorem 3.4.2. In general, the verification of safety properties for networks of timed automata as presented in this thesis is undecidable. This theorem has been proven for a closely related formalism in 2004 [Bou+04], which relies on updates on the clocks of a timed automaton. It involves a trivial reduction of the halting problem for deterministic 2-counter machines. Our formalism allows a similar reduction, which does not rely on updates on clocks, but instead 3.4. ALGORITHM 67 relies on our integer variables being unbounded and assignments being able to increment and decrement these values. We explain the details below. The reachability problem for deterministic 2-counter machines, which was shown to be undecidable in 1967 [Min67], can trivially be reduced to a safety property verification for networks of timed automata using our formalism. A 2-counter machine (Q , qo , 4) consists of a finite set of states Q with initial state q0∈Q , where 4 ⊆ Q×Op0×Q and Op0= {inc(c1) , inc(c2) , testAndJump(c1) , testAndJump(c2) , condDec(c1) , condDec(c2)} for two counters c1 , c2 that can be incremented, tested for zero or decremented in dependence of the current value. These operations can be described as •inc(ci): Increment counter ci, •testAndJump(ci): Require the value of counter cito be zero, •condDec(ci) : Require the value of counter ci to be strictly larger than zero and decrement it. Note, that the latter two are sometimes combined into a single instruction with two distinct target states in dependence whether the counter can be decremented or not. The reachability problem asks whether an accepting state qf∈Q is reachable in a finite number of steps starting from a given initial state with predetermined counter values. The reduction to a timed automaton is straight-forward. Given any 2-counter machine M= (Q , qo , 4) , we build a timed automaton A= (L , l0 , C , IV , Σ , Invc , Invi , E) and safety property ρ that is not invariant if and only if qf is reachable in M . The two counters are mapped to two integer variables with respective initial values, i.e., IV ={c1 , c2} . There does not exist a clock and the locations represent the states of the 2-counter machine, meaning C=∅ and L=Q with l0=q0 . No synchronization takes place and no invariants are given on the locations, i.e., Σ=∅ , ∀l∈L:Invc(l) = true and ∀l∈L:Invi(l) = true . Furthermore, the instructions that modify the counter values are mapped to updates on the integer variables on the edges between the locations. Formally, for every (q1,op,q2)∈ 4, there exists an edge e∈E. If op equals •inc(ci):e= (q1e,true,true,ci:=ci+1, ∅ −−−−−−−−−−−−−→ q2), •testAndJump(ci):e= (q1e,true,ci=0, true,∅ −−−−−−−−−−→ q2), •condDec(ci):e= (q1e,true,ci>0, ci:=ci−1, ∅ −−−−−−−−−−−−−−−→ q2). The safety property specifies the location representing the accepting state qf to be an error state, formally ρ:=G¬((qf) , true , true) . Checking the reachability of the accepting state in the 2-counter machine is, thus, reduced to checking the violation of the safety property. Trivially, any path of configurations in the 2-counter machine exists as well in the timed automaton and, hence, the reachability problem could be solved if the safety property could be checked for violation. As a consequence, our problem of checking safety properties for timed automata as defined in Chapter 2 68 CHAPTER 3. TIMED AUTOMATA VERIFICATION VIA IC3 WITH ZONES is undecidable in general. Note, that the undecidability is due to the unbounded usage of integer variables and assignments. 3.5 Evaluation The presented approach verifies safety properties for networks of timed automata. One of its design goals is efficiency regarding memory consumption and runtime. The IC3 algorithm underlying our approach is one of the key components to achieve this goal. In addition, the abstraction of concrete clock valuations into zones is equally important, as it efficiently handles the infinity of the clock valuation space. In order to evaluate whether the design goal is met in practice, we implemented the presented technique using Java. Several standard models are employed as benchmarks in order to compare our method with the state of the art tool Uppaal and the previous approach by Kindermann [KJN12b]. These experiments provide a basis to estimate the scalability of the presented approach. The results are very promising, in particular regarding the scalability, but also point out some drawbacks. In the following, we present the models employed in our experiments followed by some details about our implementation. Afterwards, the experiments are presented and discussed. 3.5.1 Benchmark Models We employed several standard models from literature, as well as a smaller one that we developed ourselves considering the context of Industry 4.0. In total, the following benchmarks are subsequently presented and afterwards employed in numerous experiments. • Models obtained from Uppaal website [UPP] –Fischer Mutual Exclusion algorithm –Carrier Sense Multiple Access with Collision Detection protocol –FDDI token ring protocol • FDDI token ring protocol with counting variable • Models obtained from Bruttomesso et al. [Bru+12] –Fischer Mutual Exclusion algorithm –Lamport Mutual Exclusion algorithm –Shavit-Lynch Mutual Exclusion algorithm • A shrunk model of the Lamport Mutual Exclusion algorithm • Model of the Shavit-Lynch Mutual Exclusion algorithm from PAT [PAT] 3.5. EVALUATION 69 Fischer Mutual Exclusion Algorithm (Uppaal) One of the most important models for estimating the scalability of our technique is the network of timed automata, which we have shown previously in the examples. It models the Fischer Mutual Exclusion algorithm [Lam87] that ensures mutually exclusive access to a critical section for several processes. Given its dependency on time, it is a perfect fit to be modeled as a network of timed automata. There exist several models of the Fischer algorithm, most of which only differ in small details. The model we used in the examples and our experiments is taken from Uppaal, found at their website [UPP]. We denote it as Fischer_U_x , where x is the number of timed automata. Mutual exclusion is handled by each process writing its unique identifier to a shared variable when requesting access to the critical section. After waiting a certain amount of time, the process is allowed to proceed only if the shared variable still matches its identifier. To this end, each process is modeled as a timed automaton, each having its own unique identifier. Figure 3.1 shows the model for two processes. The first process has identifier 1, while the second one has identifier 2. In consequence, the edges between locations l1 and l2 , as well as the ones between l2 and l3 are different. Each process has to write its own identifier to the shared variable and accordingly check for its own identifier. All other parts of the model are equal for every timed automaton. The critical section is modeled as location l3 and the integer variable cnt counts the number of processes currently in the critical section. The safety property of interest asks whether at most one of the processes is in the critical section at every point in time. Using the integer variable cnt mentioned above, we can express this safety property as ρ:=G¬((∗,∗),true,cnt >1), abbreviated as ρ:=G¬(cnt >1). With the Fischer algorithm being independent of the number of processes, it provides a perfect opportunity for scalability experiments. To this end, the number of processes, that is, timed automata in the network, is increased while the performance is examined. Furthermore, modifications to the used time constants allow inspections to performance changes caused by time constants. These options are also present in the other models used within our experiments. Carrier Sense Multiple Access with Collision Detection Protocol We adopted a model of the Carrier Sense Multiple Access with Collision Detection Protocol (CSMA/CD) also found at the website mentioned above [UPP]. We denote it as CSMA/CD_x , where x is the number of timed automata modeling stations. It models a broadcasting communication protocol in which several stations are trying to send data over a bus. In this scenario, only one station may send data at a time as otherwise two or more transmissions would be simultaneous and collide, s.t. no data can be received by a station listening to the bus. In this protocol, a station, willing to broadcast data, first senses whether the bus is busy. If so, it waits a random amount of time and then starts over. Otherwise, it starts sending data while listening to the bus for collisions, which may occur due to a propagation delay of the signal, denoting the time until it 70 CHAPTER 3. TIMED AUTOMATA VERIFICATION VIA IC3 WITH ZONES c<26 c<26 c:=0 c:=0 l0 l3 l1 l2 end? c:=0 begin? busy! c≥26 begin? c<26 c:=0 cd1! c≤0 c≤0 c:=0 cd2! l0 l1 l2 c:=0 begin! c=808 c:=0 end! c:=0 cd1? c:=0 busy? c:=0 cd1? c<52 c<52 c:=0 cd1? c≤808 c<52 c:=0 cd1? c<52 c:=0 begin! l0 l1 l2 c:=0 begin! c=808 c:=0 end! c:=0 cd2? c:=0 busy? c:=0 cd2? c<52 c<52 c:=0 cd2? c≤808 c<52 c:=0 cd2? c<52 c:=0 begin! Figure 3.4: Network of three timed automata modeling the CSMA/CD protocol with a bus (left timed automaton) and two communicating stations (other two automata) can be sensed by every station. In case a collision occurs, all stations stop sending and start over again. The model again denotes a mutual exclusion problem, where only one sender should be sending after the propagation delay time has passed. Figure 3.4 shows the model for two stations. This model does not require a shared variable, but makes heavy use of synchronization channels. In particular, all stations are informed of a collision by the bus consecutively firing synchronized edges (using cd1!, cd2!, . . . ), one for each station. The strict sequence of edges fired after a collision reduces the reachable portion of the state space. Our experiments show that the ratio of this reachable portion compared to the entire state space is an interesting characteristic with a wide influence to the utility of our algorithm. The safety property used in this CSMA/CD model specifies that the second station (automaton A3 ) is not allowed to transmit (modeled as location l2 ), when the first station (automaton A2 ) is transmitting since more than 52 time units (the propagation delay). It is formally described as ρ:=G¬((∗,l2,l2),c2≥52), where c2denotes clock cin automaton A2. l5 l0 l3 l1 l2 c:=0 rt2? c≤0 tt2! c≤0 tt1! c:=0 rt1? c≤0 c≤0 l0 l3l1 l2 c1:=0,c2:=0 tt1? c1≤20 l4 c1≥20 ˄ c3<120 c3≤120 rt1! c1≥20 ˄ c3≥120 rt1! c1:=0,c3:=0 tt1? c1≤20 c2≤120 rt1! rt1! c1≥20 ˄ c2<120 c1≥20 ˄ c2≥120 l5 l0 l3l1 l2 c1:=0,c2:=0 tt2? c1≤20 l4 c1≥20 ˄ c3<120 c3≤120 rt2! c1≥20 ˄ c3≥120 rt2! c1:=0,c3:=0 tt2? c1≤20 c2≤120 rt2! rt2! c1≥20 ˄ c2<120 c1≥20 ˄ c2≥120 Figure 3.5: Network of three timed automata modeling the FDDI Token ring protocol with a model of the ring (left timed automaton) and two communicating stations 3.5. EVALUATION 71 FDDI Token Ring Protocol The last benchmark adopted from the above mentioned Uppaal website [UPP] is the Token Ring FDDI Protocol. We denote it as FDDI_x , where x is the number of timed automata modeling stations. It models a situation in which several symmetric stations are ordered as a ring and a token is passed between the stations along the ring. In this scenario, there exist two options for the token passing, one is fast and the other is slow. The ring structure is modeled as a timed automaton that determines the sequence in which the token is passed from station to station, each modeled as an additional timed automaton. Due to the two different passing modes, this model includes many clocks and time constants, one of which is linearly dependent on the number of stations. Thus, the model is specifically suitable to examine the effect of large time constants. Furthermore, the reachable portion of the state space is an extremely small fraction of the entire state space due to the ring structure. This characteristic allows for interesting insight in the applicability of our technique. Figure 3.5 shows the model for two stations. This model does not require a shared variable, but makes use of synchronization channels to enforce the stations only communicating in order of the ring. The safety property specifies that the token is not at two stations at the same time. Thus, there must not exist a reachable state in which two stations are both in one of the following locations: l1 , l2 , l4 , l5 . Considering the mutual exclusion of only the first two stations, this safety property is formalized as ρ:=G¬((∗,l1,l1)) ∧ ¬((∗,l1,l2)) ∧ ¬((∗,l1,l4)) ∧ ¬((∗,l1,l5)) ∧¬((∗,l2,l1)) ∧ ¬((∗,l2,l2)) ∧ ¬((∗,l2,l4)) ∧ ¬((∗,l2,l5)) ∧¬((∗,l4,l1)) ∧ ¬((∗,l4,l2)) ∧ ¬((∗,l4,l4)) ∧ ¬((∗,l4,l5)) ∧¬((∗,l5,l1)) ∧ ¬((∗,l5,l2)) ∧ ¬((∗,l5,l4)) ∧ ¬((∗,l5,l5), where the integer constraint and zone true are each omitted for readability. FDDI Token Ring Protocol with Counting Variable As can be seen, this way of specifying mutual exclusion is lengthy. Thus, we adapted the FDDI model by addition of an integer variable cnt that counts the number of automata currently in any of the mentioned locations. We denote it as FDDIcount_x , where x is the number of timed automata modeling stations. Figure 3.6 shows this adapted model for two stations. The safety property specifying mutual exclusion can, thus, be reduced to ρ:=G¬(cnt > 1 ) . This adaptation allows for an interesting study of the effect of an additional integer variable (with simultaneous reduction of the number of error state specifications). Fischer Mutual Exclusion Algorithm (Bruttomesso) Additional mutual exclusion algorithms have been employed in our experiments. We adopted a different version of the Fischer Mutual Exclusion algorithm as presented by Bruttomesso et al. [Bru+12], denoted as Fischer_B_x , where x is the number of timed automata. It is depicted in Figure 3.7. 72 CHAPTER 3. TIMED AUTOMATA VERIFICATION VIA IC3 WITH ZONES l5 l0 l3 l1 l2 c:=0 rt2? c≤0 tt2! c≤0 tt1! c:=0 rt1? c≤0 c≤0 l0 l3l1 l2 c1:=0,c2:=0 tt1? c1≤20 l4 c1≥20 ˄ c3<120 c3≤120 rt1! c1≥20 ˄ c3≥120 rt1! c1:=0,c3:=0 tt1? c1≤20 c2≤120 rt1! rt1! c1≥20 ˄ c2<120 cnt:=cnt+1 cnt:=cnt+1 cnt:=cnt-1 cnt:=cnt-1 cnt:=cnt-1 cnt:=cnt-1 cnt:=cnt+1 cnt:=cnt+1 cnt:=cnt-1 cnt:=cnt-1 cnt:=cnt-1 cnt:=cnt-1 c1≥20 ˄ c2≥120 l5 l0 l3l1 l2 c1:=0,c2:=0 tt2? c1≤20 l4 c1≥20 ˄ c3<120 c3≤120 rt2! c1≥20 ˄ c3≥120 rt2! c1:=0,c3:=0 tt2? c1≤20 c2≤120 rt2! rt2! c1≥20 ˄ c2<120 c1≥20 ˄ c2≥120 Figure 3.6: Adapted network of three timed automata modeling the FDDI Token ring protocol with two stations as in Figure 3.5 that includes an additional integer variable cnt used to count the number of stations that are in their respective transmitting locations l0 l1 l2 l3 l4 l5 l6 l7 l8 c≤1024 c≤1024 c≤1024 c≤1024 c≤1024 c≤1024 c≥1 id≠0 c:=0 c≥1 id=0 c:=0 c≥1 c:=0 id:=1 c≥1024 c:=0 c≥1 id=1 c:=0 cnt:=cnt+1 c≥1 c:=0 cnt:=cnt-1 c≥1 c:=0 c≥1 c:=0 id:=0 c:=0 c:=0 c≥1 id≠1 c:=0 l0 l1 l2 l3 l4 l5 l6 l7 l8 c≤1024 c≤1024 c≤1024 c≤1024 c≤1024 c≤1024 c≥1 id≠0 c:=0 c≥1 id=0 c:=0 c≥1 c:=0 id:=2 c≥1024 c:=0 c≥1 id=2 c:=0 cnt:=cnt+1 c≥1 c:=0 cnt:=cnt-1 c≥1 c:=0 c≥1 c:=0 id:=0 c:=0 c:=0 c≥1 id≠2 c:=0 Figure 3.7: Network of two timed automata modeling the Fischer Mutual Exclusion algorithm for two processes as presented by Bruttomesso et al. [Bru+12] 3.5. EVALUATION 73 Lamport and Shavit-Lynch Mutual Exclusion Algorithm Bruttomesso’s publication also includes models formalizing two other mutual exclusion algorithms, namely the Lamport and Shavit-Lynch algorithms. The former solely relies on shared variables, while the latter additionally depends on timing constraints. We adopted a model for each of these two algorithms, denoted as Lamport_B_x and ShavitLynch_B_x , where x is the number of timed automata. They are depicted in Figures 3.8 and 3.9. l0 l1 l2 l3 l4 l5 l6 l7 l8 id:=1 id=1 y:=1 cnt:=cnt+1 cnt:=cnt-1 y≠0 id≠1 y=0 y:=0 l0 l1 l2 l3 l4 l5 l6 l7 l8 id:=2 id=2 y:=1 cnt:=cnt+1 cnt:=cnt-1 y≠0 id≠2 y=0 y:=0 Figure 3.8: Network of two timed automata modeling the Lamport Mutual Exclusion algorithm for two processes as presented by Bruttomesso et al. [Bru+12] Shrunk Model of Lamport Mutual Exclusion Algorithm Furthermore, we constructed a shrunk version of the Lamport model since some of the locations are not necessary. It is denoted as Lamport_S_x . The comparison of this shrunk version with the original one allows us to draw conclusions about the impact of a large number of locations in a model. The shrunk model is presented in Figure 3.10. Shavit-Lynch Mutual Exclusion Algorithm (PAT) Additionally, we employ a version of the Shavit-Lynch algorithm in our experiments that includes fewer locations. The model is taken from the PAT website [PAT], denoted as ShavitLynch_P_x . It is depicted in Figure 3.11. We augmented all these models with a counting variable, s.t. the safety property specifying mutual exclusion can be formalized as ρ:=G¬(cnt >1). Lemgo Model The applicability of our technique in real world scenarios is checked with an additional model. We developed it to represent a part of the Lemgo Smart Factory [inI] of the Hochschule Ostwestfalen-Lippe [Hoc]. It is similar in terms of size and structure to those timed automata models that are automatically learned from existing real world systems [Mai14]. It might, thus, be suitable to estimate the real world practicality of our approach. 80 CHAPTER 3. TIMED AUTOMATA VERIFICATION VIA IC3 WITH ZONES 0.1 1 10 100 1000 10000 5 10 15 20 25 30 35 40 Runtime([seconds] Number(of(timed(automata FDDI IC3Zone(LCI) Uppaal (a) Runtime of verification 0 100 200 300 400 500 600 700 5 10 15 20 25 30 35 40 UsedCmemoryC[MB] NumberCofCtimedCautomata FDDI IC3Zone(LCI) Uppaal (b) Max. memory consumption Figure 3.15: Results of the experiments using the FDDI model: Runtime and memory consumption of our presented approach IC3 with Zones are compared with state of the art tool Uppaal for models with different number of timed automata always examines the entire state space encoded via the used SMT-formulae, Uppaal only examines the reachable states via (forward) exploration. Thus, it has a huge advantage, if the ratio of reachable states to the entire number of states is small, as is the case in the FDDI model. Due to the ring structure, the order in which the automata’s edges may be taken is very strict, reducing the number of reachable states. As an example, consider the FDDI model with 20 stations. During the entire verification of the safety property Uppaal explores only 8061 states, while the entire state space includes 4 ∗ 6 20 possible location combinations, not taking into account the additional clock space. It has, thus, an enormous advantage over our approach exactly for those models with a small number of reachable state, where the entire state space is large. The two distinct ways of exploring the model’s states result in different suitabilities of the approaches for different models. In summary, we would recommend using Uppaal for smaller models and those with a small set of reachable states (hard to estimate upfront). Nevertheless, this characteristic might be guessed by means of the structure of the model, e.g., when the model allows only very specific sequences of edges being taken. On the other hand, we recommend the approach presented in this chapter to be used for larger models. It has shown to scale well and is competitive to Uppaal for some of the benchmark models. We emphasize the fact that it was capable of verifying safety properties for models three times larger than Uppaal was capable of for the Fischer_Umodel. Next, we examine the impact of integer variables on our technique. 3.5. EVALUATION 81 Integer Variable Experiments Scaling up the number of integer variables may have various effects depending on their usage. It may entirely change the state space, or may only be of little effect. Thus, we can only exemplify possible impacts of integer variables here. To this end, we will examine the change introduced by the addition of the integer variable cnt in the FDDI model. Our adapted FDDI model includes an additional integer variable cnt that counts the number of automata in transmitting locations. Six out of eight edges are extended by an integer update in each of the automata modeling a station. The introduction of this additional variable has an interesting effect. It simplifies the found inductive strengthening for every number of automata to include only two clauses. The first one is the safety property ¬(int0> 1 ) with int0 encoding the integer variable cnt . The second one ¬(¬l1 0∧(int0> 0 )) specifies (via the least significant bit of the location identifiers) that no location of the first automaton (the ring structure) with an even identifier ( l0 , l2 , . . . ) is reachable when cnt > 0. Since these are the only locations with outgoing edges incrementing cnt , the counter can not be larger than 1. The conjunction of these two clauses is inductive. This verification heavily profits from the SMT-encoding of locations via boolean variables, as well as the ring structure of the model including two locations for each station. It allows a found CTI to be generalized, s.t. it reasons about all locations of A1 with even location identifier. Figure 3.16 shows the impact on the runtime, which is extremely improved, actually able to outperform Uppaal. 0.1 1 10 100 1000 10000 5 10 15 20 25 30 35 40 45 50 Runtime([seconds] Number(of(timed(automata FDDIcount IC3Zone(LCI) Uppaal (a) Runtime of verification 0 50 100 150 200 250 300 350 400 5 10 15 20 25 30 35 40 45 50 UsedCmemoryC[MB] NumberCofCtimedCautomata FDDIcount IC3Zone(LCI) Uppaal (b) Max. memory consumption Figure 3.16: Results of the experiments using the FDDIcount model: Runtime and memory consumption of our presented approach IC3 with Zones are compared with state of the art tool Uppaal for models with different number of timed automata in the NTA The positive impact of the location encoding in combination with the generalization procedure becomes apparent by this example. Yet, the presented encoding introduces additional interesting effects. 82 CHAPTER 3. TIMED AUTOMATA VERIFICATION VIA IC3 WITH ZONES Location Identifier Experiments With our SMT-encoding relying on boolean variables to encode the identifiers of locations, we were interested whether the actual assignment of identifiers to locations affects the performance of our approach. To this end, we examined the runtimes for the verification of the mutual exclusion property for the Fischer_U models as above, where each location li ( i∈ { 0,1,2,3 } ) has identifier i . Additionally, we performed experiments with a model Fischer_U(switched) , where location l0 and l2 switched identifiers, meaning l0 has identifier 2 and l2 has identifier 0. The results are shown in Figure 3.17. 0.1 1 10 100 1000 10000 100000 5 10 15 20 25 30 35 40 45 50 Runtime([seconds] Number(of(timed(automata Fischer(different(Identifiers IC3Zone(LCI)(original(identifiers IC3Zone(LCI)(switched(identifiers (a) Runtime of verification 0 200 400 600 800 1000 1200 1400 1600 1800 5 10 15 20 25 30 35 40 45 50 Usednmemoryn[MB] Numbernofntimednautomata FischerndifferentnIdentifiers IC3ZonelLCIwnoriginalnidentifiers IC3ZonelLCIwnswitchednidentifiers (b) Max. memory consumption Figure 3.17: Results of the experiments using the Fischer_U models (Figure 3.1) with distinct assignment of identifiers to the locations: The verification has been executed using the assignment of location identifiers as used before, where li ( i∈ { 0,1,2, 3 } ) is assigned identifier i , and also with switched assignments of identifiers for l0 and l2, s.t. l0is assigned identifier 2 and l2is assigned 0 Clearly, the assignment of identifiers is of importance, as the runs with switched identifiers exhibit worse performance. Comparing and analyzing these runs did not result in a definite answer to why the runs differ that much. In these experiments, switching the identifiers reduced the number of cycles of the main loop with fewer CTIs found. Thus, the loss of performance must have different reasons. We noticed that the instances with switched identifiers show a significantly larger number of SMT-queries. This increase might be due to the generalization procedure needing more attempts to discard literals, or due to frames and CTIs being different resulting in the procedures blockCTIs and strengthenClauses issuing more queries. In general, it is not feasible to chose the assignment of identifiers upfront such that the performance is optimized. This drawback of the location encoding via boolean variables is opposed to the wider generalization capabilities as presented before. Thus, the encoding can be summarized as ambivalent. Below, we will examine the effects of the number of locations in a model. 3.5. EVALUATION 83 Location Experiments Our encoding introduces many variables by relying on the locations being encoded via boolean variables. Thus, more literals have to be tried to be discarded during generalization, leading to diverse effects. On the one hand, the increased number of variables introduces additional overhead in the SMT-formulae and in the generalization procedure. However, as seen above it can be extremely beneficial in reasoning about several locations in a single automaton during generalization. In the following, we examine models with additional locations to get a more general view on the impact of locations. To this end, we compare the Fischer_B model with the Fischer_U model since they both model the same algorithm. They use the same number of clocks and integer variables, which are used in the same way, only differing in smaller details, e.g., the invariants. The most important distinction, however, is that the larger model includes five additional location, which is more than twice as much as the smaller model. Figure 3.18(a) shows the comparison of both models for up to 15 automata in the NTA. Note, that the safety property could be proved for Fischer_U models up to 50 automata as shown above. In order to relate the performance change of our algorithm for the larger model Fischer_B , Figure 3.18(b) shows the comparison with Uppaal’s performance. 0.1 1 10 100 1000 10000 100000 2 4 6 8 10 12 14 RuntimeB[seconds] NumberBofBtimedBautomata Fischer_UBvs.BFischer_B IC3Zone(LCI)BforBFischer_U IC3Zone(LCI)BforBFischer_B (a) Runtime of IC3 with Zones for both models 0.1 1 10 100 1000 10000 100000 2 4 6 8 10 12 14 RuntimeC[seconds] NumberCofCtimedCautomata Fischer_B IC3ZonelLCI) Uppaal (b) Runtime of IC3 with Zones and Uppaal for Fischer_B Figure 3.18: Results of the experiments comparing the performance of the verifications using the two Fischer models: IC3 with Zones performs significantly worse for the Fischer_Bmodel The experiments show that our approach performs significantly worse in the presence of many locations. The decline is more intense than the one observed for Uppaal, possibly due to our location encoding being based on boolean variables, which introduces overhead if the number of locations is large. The deterioration might, however, also be due to an unsuitable location identifier assignment as seen in the previous paragraph or due to the general size of the model. We extend this insight with the comparison of runtimes for the verification experiments using the Lamport_B and Lamport_S models, which only differ by the 84 CHAPTER 3. TIMED AUTOMATA VERIFICATION VIA IC3 WITH ZONES number of locations. The runtimes of our approach for both models are compared in Figure 3.19, as well as the runtimes of Uppaal for both models. 0.1 1 10 100 1000 10000 100000 2 4 6 8 10 12 14 16 18 RuntimeB[seconds] NumberBofBtimedBautomata Lamport_SBvs.BLamport_B IC3Zone(LCI)BforBLamport_S IC3Zone(LCI)BforBLamport_B (a) Runtime of IC3 with Zones for both models 0.1 1 10 100 1000 10000 100000 2 4 6 8 10 12 14 16 18 RuntimeB[seconds] NumberBofBtimedBautomata Lamport_SBvs.BLamport_B UppaalBforBLamport_S UppaalBforBLamport_B (b) Runtime of Uppaal for both models Figure 3.19: Results of the experiments comparing the performance of the verifications using the two Lamport models: IC3 with Zones performs significantly better for the shrunk Lamport model Clearly, our presented approach reacts worse to the additional locations in the larger model. The increase of runtime is worse than the one for Uppaal. The conclusion drawn before is, thus, supported by this experiment. Our algorithm handles models with many locations (in the single automata) worse than Uppaal. Experiments with the two distinct Shavit Lynch models reach the same conclusion (see Tables A.7 and A.8 in the Appendix). We checked whether the bad scalability in terms of locations is caused by the location encoding via boolean variables. To this end, we replaced this encoding via several boolean variables with an alternative encoding of the locations via a single integer variable per automaton. The resulting performance was better, but the increase was not as significant as expected. However, the loss of the ability to generalize the locations within a single automaton (as possible with boolean variables) led to a significantly worsened performance with the FDDIcount model. In summary, the usage of an adapted encoding is possible and might even yield a better performance for some models, but we recommend the usage of the encoding presented in this chapter due to the improved generalization ability. In the following, we compare our approach with the previous attempt to utilize IC3 for timed automata verification in order to point out the advancement of our approach. We compare it with Kindermann’s IC3 approach using the region abstraction [KJN12b]. For a fair comparison regarding the used programming language, SMT-solver, encoding and heuristic, we reimplemented his approach. 3.5. EVALUATION 85 Used Constant IC3Regions(LCI) IC3 with Zones(LCI) Runtime (s) Memory (MB) Runtime (s) Memory (MB) 1 1186,2 669,6 480,2 264,4 4 2174,3 740,2 483,2 262,6 16 2179,7 741,3 482,6 263,9 64 2860,0 779,7 481,5 263,1 256 2628,4 742,3 483,0 263,7 1024 2860,5 778,3 481,9 264,6 Table 3.2: Scalability experiments with distinct time constants in the Fischer_U_15(switched)model with 15 processes Experiments with the used Abstraction The employed region abstraction renders Kindermann’s approach non-practical due to the enormous number the regions. This insignificance of the region abstraction for practical purposes has been explained in the previous chapter. In particular, its exponential growth in dependence on the size of time constants is a crucial argument. Table 3.2 illustrates this significant drawback. The safety property is verified for Fischer_U(switched) models with 15 processes and different time constants. This experiment perfectly shows the lack of the region-based technique to cope with large constants, while our approach is unaffected. For illustration of this advantage, we present the runtimes of Kindermann’s approach for the Fischer_U(switched) , CSMA/CD and FDDI model in Figures 3.20, 3.21 and 3.22. These experiments clearly show the improvement accomplished by using the zone abstraction. 0.1 1 10 100 1000 10000 100000 5 10 15 20 25 RuntimeZ[seconds] NumberZofZtimedZautomata Fischer_U IC3Zone(LCI) IC3Region(LCI) (a) Runtime of verification 0 200 400 600 800 1000 1200 1400 1600 5 10 15 20 25 UsedImemoryI[MB] NumberIofItimedIautomata Fischer_U IC3ZoneRLCIg IC3RegionRLCIg (b) Max. memory consumption Figure 3.20: Results of the experiments using the Fischer_U(switched) model: Runtime and memory consumption of our presented approach IC3 with Zones are compared with the previous approach using the region abstraction for models with different number of timed automata in the NTA 86 CHAPTER 3. TIMED AUTOMATA VERIFICATION VIA IC3 WITH ZONES 0.1 1 10 100 1000 10000 100000 5 10 15 20 25 30 RuntimeI[seconds] NumberIofItimedIautomata CSMA/CD IC3Zone(LCI) IC3Region(LCI) (a) Runtime of verification 0 200 400 600 800 1000 1200 1400 1600 1800 5 10 15 20 25 30 Used/memory/[MB] Number/of/timed/automata CSMA/CD IC3ZoneRLCIg IC3RegionRLCIg (b) Max. memory consumption Figure 3.21: Results of the experiments using the CSMA/CD model: Runtime and memory consumption of our presented approach IC3 with Zones are compared with the previous approach using the region abstraction for models with different number of timed automata in the NTA 1 10 100 1000 10000 2 4 6 8 10 12 14 16 18 20 Runtime([seconds] Number(of(timed(automata FDDI IC3Zone(LCI) IC3Region(LCI) (a) Runtime of verification 0 100 200 300 400 500 600 700 2 4 6 8 10 12 14 16 18 20 UsedImemoryI[MB] NumberIofItimedIautomata FDDI IC3ZonegLCI) IC3RegiongLCI) (b) Max. memory consumption Figure 3.22: Results of the experiments using the FDDI model: Runtime and memory consumption of our presented approach IC3 with Zones are compared with the previous approach using the region abstraction for models with different number of timed automata in the NTA 3.5. EVALUATION 87 In order to test the practicality one last time, we verified the mentioned safety property for the Lemgo model presented above. Table 3.3 shows the runtime and memory of our approach when verifying the real world example from Lemgo. It is apparent, that the performance is sufficient and the presented approach is of practical value. IC3 with Zones(LCI) IC3 with Zones(CLI) Uppaal Runtime Memory Runtime Memory Runtime Memory Lemgo model 0,7 79,1 0,7 75,2 0,1 35,1 Table 3.3: Experiments using our Lemgo model (Figure 3.12): The runtimes (seconds) and memory consumption (MB) are depicted for our approach IC3 with Zones with two distinct heuristics for variable ordering ( LCI and CLI ), as well as for the tool Uppaal 3.5.5 Inductive Strengthening Experiments In addition to the verification results that are "There exists a counterexample trace, i.e., the property is not invariant" or "The property is invariant", our technique yields an extra outcome in the latter case. It computes an inductive strengthening of the safety property, which is a formula encoding an inductive set of states that all satisfy the safety property. Due to its inductiveness, it trivially includes all reachable states (which means it is an overapproximation). It can, thus, be used as an easy means to validate a successful verification. To this end, the three properties of inductive strengthenings (Definition 2.4.1) have to be checked. This check again employs SMT-solving and usually significantly outperforms a complete re-verification. As a result, the additional outcome in form of an inductive strengthening can be of huge importance. For illustration, consider the following scenario that involves two parties. On the one hand, there exists a client that wants to verify a safety property for a specific model. However, his resources in form of time and memory are usually restricted, s.t. he cannot execute the verification himself. On the other hand, there exists a provider, e.g., a computing center, that possesses the necessary resources and is, thus, capable of executing the desired verification. The important aspect in such scenarios is the question whether the provider is trustworthy and the client can trust the result of the provider. At this point a certificate, here the inductive strengthening, can be employed. To this end, the provider ships the certificate to the client. Since the validation of the certificate is by far easier than the entire verification, the client is able to validate it using his limited resources. If the shipped formula is indeed an inductive strengthening of the desired safety property, the client can be sure that the safety property is invariant. Such approaches are called proof-carrying and are widely employed in several domains [Nec02], [DKP09]. We have performed a validation of the inductive strengthenings found during our experiments in the previous chapter. The benefit of validation compared to 88 CHAPTER 3. TIMED AUTOMATA VERIFICATION VIA IC3 WITH ZONES verification is obvious when considering the runtimes in Tables A.11 to A.21 with Tables A.1 to A.10. As can be seen, most inductive strengthenings found in our experiments can be validated within seconds. The speed up in comparison with an entire verification run is significantly better, the larger the instance. In particular, there exist smaller instances, where almost no speed up was measurable. In contrast, in some larger instances the required time for validation was as small as roughly 0,02% of the time required for verification. With its small size (max. 2 MB in our experiments) the inductive strengthenings computed by our technique are perfectly suitable to be used in certifying scenarios. In addition, they are of value in other scenarios, where we speed up the verification of a reconfigured model or reason about an entire family of models. These approaches are presented in the subsequent chapters. 3.6 Summary In summary, we have presented an approach for the verification of safety properties for networks of timed automata. To this end, we have developed a concept that combines the successful algorithm IC3 with the Zone abstraction to employ the runtime and memory efficiency of it for the verification of timed systems. We have given an SMT-encoding that is designed with IC3’s generalization procedure in mind. Using backwards computation, we have shown how to incorporate the Zone abstraction into the algorithm. The necessary modifications are only punctual and, thus, allow the usage of most of the optimizations proposed for IC3 so far and in the future. We have implemented the concept in Java and evaluated its strengths and weaknesses in numerous experiments. The presented technique scales well and shows promising results. It is competitive to state-of-the-art tools in many instances. However, its weakness is the dependence on the size of the entire state space. In contrast, other tools only depend on the size of the reachable portion of the state space. Taking into account the additional outcome for a successful verification in form of an inductive strengthening of the safety property, we conclude that the presented technique is definitely of value (for example in proof-carrying approaches) and yields promising results. This additional outcome is fundamental for the two approaches presented in the next chapters, in which it is used to speed up the verification of a reconfigured model and to reason about a family of models. 4 Incremental Inductive Verification of Parameterized Timed Systems In the previous chapter, we have proposed a novel combination of two well-known techniques that can be used to verify safety properties for timed automata. Aiming at model-based design processes, this technique is well suited to be employed for the formal verification of safety properties for real-time systems. With an increasing number of systems being time-based and safety critical, there exists a large demand for such techniques. In some structured model-based design processes, an iterative procedure triggers a repeated reconfiguration of the model until a final design is found. A similar scenario is the reconfiguration at lifetime of a system, e.g., due to self-adaptation. In these scenarios, there exists a need to verify properties for reconfigured models, which have already been verified before for the original model. Like other state-of-the-art techniques, the previously presented approach does not cover these scenarios. It verifies a safety property for a fixed model. In order to cope with a reconfigured model, it would restart the verification from scratch like in other approaches. It is, however, likely that the reconfigured model is only slightly changed. Thus, it is desirable and promising to reuse the results of the previous verification. We study this reuse in the following. Chapters 4 and 5 propose a workflow for a restricted subset of models and reconfigurations, while Chapter 6 explores the general case. Consider the specific setting, where the system consists of an arbitrary, but fixed number of equal processes. Though this setting is specific, it includes a large number of situations, e.g., processes communicating via a peer to peer protocol or executing a mutual exclusion algorithm. Using the technique from the previous chapter enables us to verify safety properties for each such given model with a fixed number of processes. We are, however, interested in the verification of the safety property for every such model as the number of processes is arbitrary. For illustration consider a system [P1|| . . . ||Pn] with a fixed number n of processes ensuring mutual exclusion. A reconfiguration that adds an additional process requires an new verification for 89 96 CHAPTER 4. INCREMENTAL INDUCTIVE VERIFICATION OF PTS •∀c∈Cg:π(vc)(c) = vc(c). •∀k∈ {1, . . . , n}:∀c∈Cl k:π(vc)(c) =        vc(ci)i f k =j, vc(cj)i f k =i, vc(c)else, where ci and cj refer to the clock c in automaton Ai ( c∈Cl i ) and Aj ( c∈Cl j ), respectively. •∀iv ∈ IV6id :π(vi)(iv) = vi(iv). •∀iv ∈ IVid :π(vi)(iv) =        i i f vi(iv) = j, j i f vi(iv) = i, vi(iv)else. Note, that we also use π(m) to denote the identifier of the automaton with which m has been swapped, formally π(m) =        i i f m =j, j i f m =i, m else. The swap operation swaps the locations of the two automata. Furthermore, it interchanges the values of their local clocks, as well as values for identifier aware integer variables that refer to one of the two automata. The swap operation is applicable, whenever the two swapped automata have the same set of locations and local clocks. However, its applicability does not ensure symmetry as defined below. Note, that a permutation involving more than two automata being swapped can easily be realized via several swap operations in sequence. We employ this swap operation to define the notion of symmetry required in our workflow. Definition 4.2.2 (Symmetry of the State Space) . Let a network of timed automata NTA =hA1 ,..., Ani be given with concrete semantics TS = (S , s0 , →) . It is symmetric, if for any swap π and any states s1 , s2∈S , it holds that s1→s2 with time delay δ and taken edge e of timed automaton Ai if and only if π(s1)→π(s2) with time delay δ and taken edge e of timed automaton Aπ(i) . Furthermore, it must hold that s=s0if and only if π(s) = s0. Our definition of symmetry ensures the initial state to be symmetric, as well as paths to be symmetric. This implies for a state s that is reachable via a path from an initial state, that all its swapped states π(s) are reachable via the respective swapped paths. Note, that the notion of symmetry characterizes π to be an automorphism on the transition system that is the concrete semantics TS (c.f. [Hen+04]). As mentioned above, the applicability of the swap operation is not sufficient to ensure this notion. It can, however, be ensured via the specific restrictions on integer variables as above. To this end, we formalize our models as templates that are bound to these restrictions. We have proven in the Appendix B.1 that all networks of timed automata created via these templates meet our notion of symmetry. 4.3. SPECIFICATION VIA TEMPLATES 97 4.3 Specification via Templates Symmetric networks of timed automata allowed in our incremental approach are defined as instantiations of a template. A template is the abstract specification of a parameterized network of timed automata using the above redefinitions of integer variables. In order to actually create the network, it is instantiated several times with the distinct identifiers of the automata. The resulting timed automata in the network are, thus, distinct in dependence of their identifiers. In summary, templates are an intuitive way of formalizing symmetric models for our approach. We define this concept below. It is closely related to the templates as defined in Uppaal, but imposes the above restrictions on the automata. Definition 4.3.1 (Timed Automaton Template) . Let the set Cg of global clocks be given, as well as the global set of integer variables IV =IV6id ∪ IVid as the union of disjoint sets of identifier unaware ( IV6id ) and aware ( IVid ) integer variables, s.t. IV6id ∩ IVid =∅ . A symmetric timed automaton template A(pid) defined over globally shared Cg and IV is a tuple A(pid) = (L , l0 , C , IV , ∅ , Invc , Invi(pid) , E(pid)) such that •pid ∈N≥1is a unique parameter, called identifier, •Lis a finite set of locations, •l0∈Lis the initial location, •C=Cl∪Cg is the union of the finite and disjoint sets of local and global clocks with initial valuation vc 0, •IV is the finite set of shared integer variables with initial valuation vi 0, •∅is the set of synchronization channels (no synchronization is allowed), •Invc:L→Φ(C)is a total function of clock invariants, s.t. vc 0|=Invc(l0), •Invi(pid):L→Ψ(IV,pid)is a total function of integer invariants, s.t. vi 0|=Invi(pid)(l0), and •E(pid)⊆L× {e} × Φ(C)×Ψ(IV , pid)×Ω(IV , pid)× 2 C×L is the set of edges. Instantiating a template A(pid) with unique identifier pid =j∈N≥1 results in timed automaton Aj . The following example illustrates the process of instantiation. Example Figure 4.3 shows the template representing the Fischer_Umodel shown in the previous chapter (Figure 3.1) modeling the Fischer mutual exclusion algorithm. It can be used to create the symmetric model with any number of automata. There exists only one integer variable ( id ) that is aware of identifiers and the constraints and assignments involving it are parameterized with pid . The template can be instantiated, e.g., with the two identifiers 1 and 2 resulting in the automata depicted 98 CHAPTER 4. INCREMENTAL INDUCTIVE VERIFICATION OF PTS in Figure 3.1. When instantiating the template with a unique identifier, e.g., pid = 2, a timed automaton A2 is created in which the parameter pid is replaced by the actual identifier 2. For instance, the automaton contains the constraint id = 2 instead of the parameterized one id =pid. cnt:=cnt+1 id:=0; cnt:=cnt-1 id=0 c≤1024 c:=0 id=0 c≤1024 id:=pid c:=0 c>1024 id=pid c:=0 l0 l3 l1 l2 Figure 4.3: Example of a timed automaton template that represents the Fischer mutual exclusion algorithm (Fischer_U) We employ templates as intuitive means to specify a parameterized timed system modeled as symmetric network of timed automata. In order to create a model for a fixed number n∈N≥1 of automata, the template is instantiated n timed with the respective identifiers 1 to n . We formalize this creation of a symmetric network of timed automata with fixed number of automata below. Definition 4.3.2 (Symmetric Network of Timed Automata) . Given n∈N≥1 and the timed automaton template A(pid) as defined in Definition 4.3.1. The symmetric network of timed automata with n timed automata is defined as NTAn=hA1 , . . . , Ani , where Aiis the instantiation of A(pid)with pid =i(i∈ {1, . . . , n}). This definition of networks of timed automata via templates ensures the models to be symmetric. Section B.1 in the Appendix proves our notion of symmetry to hold for the models. In addition to symmetric models, our technique relies on the safety property to be symmetric, too. It is defined as follows. Definition 4.3.3 (Symmetry of the Safety Property) . Let a network of timed automata NTA =hA1 ,..., Ani be given with concrete semantics TS = (S , s0 , →) . Given any swap π and state s∈S , a safety property ρ is symmetric if it holds that s|=ρ if and only if π(s)|=ρ. We ensure this symmetry via redefinition of the safety property. The adapted definition includes all permutations of timed automata in the network and, thus, is inherently symmetric. 4.3. SPECIFICATION VIA TEMPLATES 99 Recall the definition of error state specifications (Definition 2.1.13). An error state specification err reasons about the locations, integer and clock valuations of states in a network NTAm of m timed automata. In order to employ the error state specification also for larger models of size n≥m (as in a parameterized system), we create a scaled error state specification errn . To this end, the partial location vector simply needs to be filled with the unspecified location element ( ∗ ) for all additional automata. We obtain a symmetric error state specification by considering all permutations of the ntimed automata. Definition 4.3.4 (Symmetric Error State Specification) . Given an error state specification err = ( ¯ lm , φ , ψ) for NTAm as in Definition 2.1.13, where ψ=ψ0∧ψ1( 1 )∧ · · · ∧ ψm(m) contains parameterized constraints for the m automata. The scaled error state specification for NTAn ( n≥m ) is defined as errn= (¯ l , φ , ψ) with ∀i∈ { 1, . . . , m}: ¯ l[i] = ¯ lm[i]and ∀i∈ {m+1, . . . , n}:¯ l[i] = ∗. The symmetric error state specification for NTAn is defined as errn sym =∃π:errn π for permutation π(cf. Def. 4.2.1) with errn π= (π(¯ l),π(φ),π(ψ)) being defined as •∀i∈ {1, . . . , n}:π(¯ l)[i] = ¯ l[π(i)], •π(φ) =              π(φ1)∧π(φ2)if φ=φ1∧φ2, (π(x)−π(y)) ./ nif φ= (x−y)./ n, π(x)./ nif φ=x./ n, true if φ=true, where π(x) refers to clock x itself if x∈Cg or otherwise refers to the respective clock in Cl π(i)if x∈Cl i, •π(ψ) = ψ0∧ψ1(π(1)) ∧ · · · ∧ ψm(π(m)). With the existential quantification, which is replaced by enumeration and disjunction in the SMT-encoding, any combination of timed automata is possible and, thus, the error state is symmetric. For illustration, consider the following example. Example 4.3.5. Let the model Fischer_U_ 3 be given ( n= 3). Consider an error state specification err = ((∗ , l1) , c1≤ 0, cnt ≤ 1 ∧id = 1 ) referring to m= 2 timed automata, namely A1 and A2 , and c1 denoting clock c in A1 . It specifies that any state is an error state that includes location l1 for automaton A2 , a value for c of A1 less or equal to 0, and cnt ≤ 1 and id = 1. As can be seen, the timed automaton A3 is not referred. The scaled version simply states that the location of A3 is undefined, formally err3= ((∗ , l1 , ∗) , c1≤ 0, cnt ≤ 1 ∧id = 1 ) . When considering the swap π1=swap1,2 the resulting permuted error state specification is err3 π1= ((l1 , ∗ , ∗) , c2≤ 0, cnt ≤ 1 ∧id = 2 ) , where c2 denotes clock c in A2 . Another swap might be π2=swap1,3 resulting in the specification err3 π2= ((∗ , l1 , ∗) , c3≤ 0, cnt ≤ 1 ∧id = 3 ) with c3 denoting clock c in A3 . In order to achieve symmetry, all permutations have to be considered. 100 CHAPTER 4. INCREMENTAL INDUCTIVE VERIFICATION OF PTS With enumeration, the symmetric error state specification is as follows. err3 sym =((∗,l1,∗),c1≤0, cnt ≤1∧id =1) ∨((∗,∗,l1),c1≤0, cnt ≤1∧id =1) ∨((l1,∗,∗),c2≤0, cnt ≤1∧id =2) ∨((∗,∗,l1),c2≤0, cnt ≤1∧id =2) ∨((∗,l1,∗),c3≤0, cnt ≤1∧id =3) ∨((l1,∗,∗),c3≤0, cnt ≤1∧id =3) If any of them is satisfied by a state s , then s is an error state. Trivially, any swap π(s) is also an error state, since all permutations of the error state specification are considered. The above symmetric error state specifications allow for the definition of symmetric safety properties. Definition 4.3.6 (Symmetric Safety Property) . Let NTAn be a given network of n timed automata. The symmetric safety property is defined as ρn=¬(err 1 n sym)∧ ¬(err2n sym)∧. . . for symmetric error state specifications err1n sym,err2n sym,. . . . Given the above definitions, we define the actual verification questions we are interested in when considering parameterized timed systems. Verification Question: Given the timed automaton template A(pid) and a symmetric safety property ρ , does the safety property ρn hold for all networks of timed automata NTAn consisting of n∈N≥1 instantiations of the template? Since the error states in the safety property are defined for models with more than or exactly m timed automata, we say ρn holds for NTAn with n<m , but need to verify the property for all n≥m . In the following, we shortly elaborate on the decidability of this verification question. 4.4 Decidability In general, the above verification question is undecidable. Trivially, the argumentation of the previous chapter (Subsection 3.4.1) can be applied for our symmetric models as well. One reason for undecidability is the existence of updates on the identifier unaware integer variables as has been shown via reduction in the mentioned subsection. An additional issue in the above verification question is the fixed, but arbitrary large number of timed automata. This allows for a reduction that exploits the number of automata as shown by Abdulla et al. [ADM04] for timed networks. Their reduction can be adapted to fit our formalism by representing the controller via an integer variable and using a global clock in combination with additional integer variables for synchronization of edges. 4.5. BASIC APPROACH 101 Thus, the verification question for parameterized timed systems is in general undecidable. However, Abdulla has shown that there exist some decidable instances, e.g., when a process includes at most one clock like in the Fischer models [AJ03]. Our experiments are in line with these insights. Hence, an approach answering the given verification question is reasonable for some models. We show our incremental technique for this problem in the following. 4.5 Basic Approach We propose to incrementally verify the symmetric models with increasing number n of timed automata. To this end, we harness the symmetry and composition aspect resulting in a Termination Theorem that ensures the safety property to hold for all n∈Nupon successful application. Valid for]NTAn+1? Check]Safety]Property for]NTAn] CEX n:=n+1 [no] [yes] Safety]Property]holds]for]all]n Inductive]strengthening n=max(1,m, Extrapolate Figure 4.4: Basic workflow The workflow can be seen in Figure 4.4. It comprises a loop that is indefinitely iterated until the Termination Theorem is applicable, i.e., our extrapolation produces a valid inductive strengthening for NTAn+1 . However, since the verification question is undecidable in general, there exist instances that run indefinitely with our theorem never being applicable. The approach is entirely based on SMT-solving and works as follows. Our workflow starts with the smallest model. Taking into account that the safety property is specified over m timed automata (cf. Definition 4.3.4), we start 102 CHAPTER 4. INCREMENTAL INDUCTIVE VERIFICATION OF PTS with a network of timed automata NTAn , where n=max( 1, m) . The symmetric safety property ρn is verified for NTAn using our IC3-based technique IC3 with Zones presented in the previous chapter providing an inductive strengthening of the safety property in case of success. Otherwise, a counterexample trace is found and the safety property does not hold for all n∈N≥1 . The inductive strengthening is provided as an SMT-formula kFk in conjunctive normal form. It is a conjunction of clauses, which consist of location, clock and integer literals reasoning about the n timed automata in the model NTAn . In order to use it for the next larger model NTAn+1 , we execute a subsequent extrapolation step. Definition 4.5.1 specifies this extrapolation procedure with which we yield an SMT-formula kFkexp(n+1) reasoning about all timed automata in NTAn+1. Definition 4.5.1 (Extrapolation of an Inductive Strengthening) . Given the SMT- formula kFk representing the inductive strengthening F of safety property ρn for the network of timed automata NTAn . kFkexp(x) is the SMT-formula representing the Extrapolation of F to a network NTAx of x≥n timed automata. kFkexp(x) is defined as the SMT-formula representing the conjunction of π(F) for all possible permutations π of the x timed automata. To this end, kFk is permuted according to the operation swap , i.e., location literals are swapped, as well as local clocks and values of identifier aware integer variables different from the neutral element 0. The implementation of the extrapolation procedure permutes clauses separately. To this end, only clauses that are not identical up to permutation are considered. This allows an efficient handling of clauses and results in a low runtime. The following example illustrates the above extrapolation procedure. Example 4.5.2. Consider the timed automaton template depicted in Figure 4.3. The instantiation for n= 2 results in the symmetric network of timed automata depicted in Figure 3.1. The verification of the symmetric safety property ρ:=¬(cnt > 1 ) computes the inductive strengthening as depicted in Table 4.1 in the second column. There exist five clauses that are not identical up to permutation. The first column of Table 4.2 depicts representatives for these clauses. The application of the extrapolation procedure computes all permuted clauses of these representatives for all permutations of the n+ 1 = 3 timed automata. The identifier aware integer variable id is represented in the encoding as int0 and has to be considered in the permutations whenever the compared value in the literal is a specific identifier. The identifier unaware integer variable cnt is represented in the encoding as int1 and must not be considered in the permutations at all. In addition, all location and local clock variables have to be considered for the permutations. The resulting clauses are depicted in the second column of the mentioned table. As can be seen, the extrapolated formula equals the inductive strengthening computed in the previous chapter for Fischer_U_ 3. It shows that it is possible to infer a valid inductive strengthening of the safety property for n+ 1 automata from an inductive strengthening of the safety property for n automata. Our workflow relies on this potential. 4.5. BASIC APPROACH 103 representative clause from kFk kFkexp(3) (int1≤1) (int1≤1) ∧((int06=0)∨(int1≤0)) ∧((int06=0)∨(int1≤0)) ∧(¬l1 0∨l1 1∨(int1≤0)) ∧(¬l1 0∨l1 1∨(int1≤0)) ∧(¬l2 0∨l2 1∨(int1≤0)) ∧(¬l3 0∨l3 1∨(int1≤0)) ∧(l1 0∨(int06=1)∨(int1≤0)) ∧(l1 0∨(int06=1)∨(int1≤0)) ∧(l2 0∨(int06=2)∨(int1≤0)) ∧(l3 0∨(int06=3)∨(int1≤0)) ∧((c1 0≤1024.0)∨(int06=1)∨(c2 0>1024.0)) ∧((c1 0≤1024.0)∨(int06=1)∨(c2 0>1024.0)) ∧((c1 0≤1024.0)∨(int06=1)∨(c3 0>1024.0)) ∧((c2 0≤1024.0)∨(int06=2)∨(c1 0>1024.0)) ∧((c2 0≤1024.0)∨(int06=2)∨(c3 0>1024.0)) ∧((c3 0≤1024.0)∨(int06=3)∨(c2 0>1024.0)) ∧((c3 0≤1024.0)∨(int06=3)∨(c1 0>1024.0)) Table 4.2: Each of the clauses (that are not identical up to permutation) in the computed inductive strengthening for n automata (left) is permuted for all permutations of the n+1 automata in order to create the extrapolated formula (right) The resulting extrapolated formula kFkexp(n+1) is denoted as candidate inductive strengthening for NTAn+1 . It is then checked for validity, i.e., whether all three characteristics of inductive strengthenings hold true for the extrapolated formula kFkexp(n+1) and model NTAn+1 . If invalid, n is incremented and the next iteration of the loop is started. Otherwise, the candidate represents a valid inductive strengthening of ρn+1 for NTAn+1 , in which case our Termination Theorem (Theorem 4.5.1) applies. It states that the safety property holds ∀n∈N≥1 , if the candidate is a valid inductive strengthening. Theorem 4.5.1 (Termination Theorem) . Given the SMT-formula kFk representing an inductive strengthening F of ρn for NTAn . If kFkexp(n+1) is an inductive strengthening of ρn+1for NTAn+1, then kFkexp(n+2)is an inductive strengthening of ρn+2for NTAn+2. The proof of correctness is given in the subsequent chapter for a more general formalism. The incremental design of the workflow yields the benefit of starting with small networks of timed automata, which are efficiently verifiable. Thus, a fast overall performance of our approach is likely in case the Termination Theorem can be applied early. Additionally, our theorem is most suitable for an incremental workflow, being able to reason about all n∈N≥1 by taking into account the results of a specific instance. We illustrate the workflow in the following. Example 4.5.3. As an example consider the Fischer_U template as given in Figure 4.3 with the symmetric safety property ρ:=¬(cnt >1)specifying values for x=0 timed automata. Our workflow starts with the verification of the safety property for the symmetric network of n= 1 timed automata NTAn . After successful verification, the found inductive strengthening kFk= (int1≤ 1 )∧(l1 0∨(int1≤ 0 )) ∧(l1 1∨(int1≤ 0 )) is returned as can be seen in Table 4.1. The extrapolation procedure produces a candidate formula with five clauses, namely kFkexp(n+1)= 104 CHAPTER 4. INCREMENTAL INDUCTIVE VERIFICATION OF PTS (int1≤ 1 )∧(l1 0∨(int1≤ 0 )) ∧(l2 0∨(int1≤ 0 )) ∧(l1 1∨(int1≤ 0 )) ∧(l2 1∨(int1≤ 0 )) . The candidate is not inductive for NTAn+1 , as Consecution fails. Thus, the next cycle starts with the verification of the safety property ρn for NTAn with n= 2. After successful verification the resulting inductive strengthening is again extrapolated into a candidate, which is checked for validity (which means whether Theorem 4.5.1 is applicable). This cycle is iterated indefinitely until the theorem can be applied, a counterexample trace is found during a run of IC3 with Zones or the systems runs out of memory or time. 4.6 Optimizations Technically, the presented workflow can be realized using any verification technique resulting in an inductive strengthening as defined above. However, we designed some optimizations tailored specifically to our algorithm IC3 with Zones shown in Chapter 3. We present these optimizations in the following, namely a Feedback -loop and the Generalization of the found inductive strengthening. These enhancements have distinct aims within the workflow. The latter is designed to increase the applicability of Theorem 4.5.1, while the former is constructed to speed up the verification of models in the IC3 algorithm itself. We start with a detailed description of this speed-up optimization. 4.6.1 Feedback Loop During the basic loop of our workflow, we propose a candidate inductive strengthening kFkexp(n+1) for the next larger model NTAn+1 . In case the Termination Theorem can not be applied, i.e., the candidate is not a valid inductive strengthening, it is discarded so far. It might, however, be of substantial value. Even though it is not a valid inductive strengthening it might be similar to one, as some of its clauses might occur within a valid inductive strengthening. These clauses should be extracted and used to accelerate the verification process. To this end, the proposed candidate is injected into the verification run of IC3 with Zones for NTAn+1 . We call this a Feedback -loop, since the clauses of the candidate are fed back into the cycle instead of simply being discarded. In order to decide, which of the clauses are relevant, i.e., can be reused without breaking the properties of the frames in the IC3 algorithm, we use two distinct methods. On the one hand, we employ the incremental method of Chockler et al. [Cho+11] to inject an inductive subset of the clauses in the candidate formula into each frame of IC3. On the other hand, we employ our own method to inject clauses that are inductive relative to the set of initial states (frame F0 ) into the frame F1. We denote the former one as Chockler-Feedback and the latter one as Frame1-Feedback. Both methods are shown below. Chockler-Feedback The following method is taken from Chockler et al. [Cho+11], where it is used for incremental verification of hardware models. It searches for the largest subset of the clauses in the candidate formula kFkexp(n+1) that is inductive. 4.6. OPTIMIZATIONS 105 This set of clauses can, thus, be conjoined to all frames in IC3 with Zones. As a result, the search space for CTIs in the frames is pruned heavily upfront. Formally, it searches the largest subset C⊆clauses(kFkexp(n+1)) of clauses in the candidate that is inductive, i.e., •Initiation: kIn+1k ∧ ¬kCkis unsatisfiable, •Consecution: kCk ∧ kTn+1k ∧ ¬kCk0is unsatisfiable, with the formulae kIn+1k and kTn+1k denoting the encoding of the set of initial states and the transition relation of NTAn+1 with invariants as shown, e.g., in Subsection 3.1.10. The conjunction of each of the frames with the set C of clauses clearly preserves the four properties of the frames, as C is inductive. It is extremely powerful in pruning the considered states in the frames. However, we observed that the inductive set of clauses C is rather small for some models, since many of the clauses hinder inductiveness. Despite being of value for the IC3 algorithm, these clauses are discarded. For this reason, we constructed a weaker Feedback method detailed below. Frame 1 -Feedback Instead of searching an inductive subset of clauses that are conjoined to every frame, our Frame 1-Feedback searches a subset of clauses that is inductive relative to the set of initial states, but can only be conjoined to frame F1 . Formally, given the proposed candidate formula kFkexp(n+1) , we compute the largest subset C⊆clauses(kFkexp(n+1))of clauses that are initialized and inductive relative to F0=In+1: •Initiation: kIn+1k ∧ ¬kCkis unsatisfiable, •Consecution relative to In+1:kIn+1k ∧ kTn+1k ∧ ¬kCk0is unsatisfiable, with the formulae kIn+1k and kTn+1k denoting the encoding of the set of initial states and the transition relation of NTAn+1 with invariants as shown, e.g., in Subsection 3.1.10. The result is injected into IC3 with Zones as clauses of frame F1 (cf. Section 2.4), which may prevent the costly rediscovery of some of them. Although the conjunction with F1 does not prune the larger frames F2 , . . . the method is of importance. Clearly, the number of clauses in C is not smaller in the Frame 1-Feedback than in the Chockler -Feedback, as an inductive set of clauses is also inductive relative to F0 . Furthermore, the clauses of the latter method can be propagated to larger frames during the run of IC3 with Zones. Thus, the restriction of the Frame 1-Feedback to conjoin clauses only with F1is not a serious cutback. Both these feedback methods can be used separately or in combination. Furthermore, their implementation is simple as the clauses only have to be checked and inserted at the start of IC3 with Zones and the rest of the algorithm proceeds entirely as before. Our implementation is based on the one described by Chockler et al. [Cho+11] using auxiliary variables for finding the injected subsets. 112 CHAPTER 4. INCREMENTAL INDUCTIVE VERIFICATION OF PTS resulting inductive strengthening might be different, which in turn affects the subsequent cycles of our approach. Thus, the Feedback -optimization has a significant impact on our approach. In the following, we evaluate whether the combination of both optimizations further improves the performance. As stated before, this combination allows for two options. On the one hand, the extrapolated generalized set of clauses can be used in the Feedback -loop. On the other hand, the extrapolated non-generalized set of clauses can be used. Table 4.7 shows the performance using the two options. Fischer_U Fischer_U (switched) Fischer_B Lamport_B Lamport_S ShavitLynch_B ShavitLynch_P Feedback using non-generalized set of clauses (all clauses) Chockler - Runtime (s) 1,3 2,0 55,1 OOM 1,3 OOT OOM Chockler - Verified ∀n∈N∀n∈N∀n∈N1-7 ∀n∈N1-3 1-6models NTAn for which n? Frame1 - Runtime (s) 1,2 1,1 34,9 9,0 1,7 199,7 OOT Frame1 - Verified ∀n∈N∀n∈N∀n∈N∀n∈N∀n∈N∀n∈N1-4models NTAn for which n? Both - Runtime (s) 1,3 1,2 36,0 55,7 1,6 958,1 OOT Both - Verified ∀n∈N∀n∈N∀n∈N∀n∈N∀n∈N∀n∈N1-4models NTAn for which n? Feedback using generalized set of clauses Chockler - Runtime (s) 1,3 2,0 50,5 OOM 1,4 OOM 880,3 Chockler - Verified ∀n∈N∀n∈N∀n∈N1-8 ∀n∈N1-3 ∀n∈Nmodels NTAn for which n? Frame1 - Runtime (s) 1,5 1,1 35,4 OOM 1,5 6622,6 OOT Frame1 - Verified ∀n∈N∀n∈N∀n∈N1-8 ∀n∈N∀n∈N1-4models NTAn for which n? Both - Runtime (s) 1,3 1,1 35,7,1 OOM 1,6 6981,5 OOT Both - Verified ∀n∈N∀n∈N∀n∈N1-8 ∀n∈N∀n∈N1-4models NTAn for which n? Table 4.7: Runtime needed for the verification of a symmetric safety property for the parameterized timed systems using the workflow with both optimizations. The safety property was verified for the entire parameterized system (marked as ∀n∈N in the second row) or for only a few instances with fixed n , where we give the sizes of the models that were successfully verified Clearly, the experiments show that the combination of optimizations does not improve the overall performance. The basic workflow optimized only by the Frame 1- Feedback loop still shows the best results. In summary of the above experiments, we conclude that our workflow is of value, even if the verification run is incomplete. It verifies smaller models with fixed n∈N before running out of time or memory and is, thus, not entirely useless in such a 4.7. EVALUATION 113 Fischer_U Fischer_U (switched) Fischer_B Lamport_B Lamport_S ShavitLynch_B ShavitLynch_P Runtime (s) 1,6 1,2 87,8 8,5 1,7 28,1 2778,5 Verified ∀n∈N∀n∈N∀n∈N∀n∈N∀n∈N∀n∈N∀n∈Nmodels NTAn for which n? Uppaal - Runtime (s) 0,7 0,7 17,8 5,3 0,4 0,3 1218,5 Uppaal - Verified 8 8 5 6 6 4 13models NTAn for which n? IC3 - Runtime (s) 0,9 0,8 6,7 5,3 1,1 17,3 149,5 IC3 - Verified 2 2 2 2 2 2 3models NTAn for which n? Table 4.8: Comparison of our workflow (first rows) with verifications for instances with fixed nthat could be verified in the same time case. Furthermore, our proposed Feedback -optimization accelerates the runs of our IC3 with Zones algorithm, which renders larger models verifiable that could not be verified without the injected clauses. The overall performance of the workflow using the optimizations is very promising and the technique, in general, has the benefit of verifying parameterized timed systems for all n∈N . In order to illustrate this benefit, we show a comparison with verifications of models with fixed n∈N below. 4.7.2 Comparison with fixed Models We demonstrate this benefit by comparison with the tool Uppaal and a single verification run of our algorithm IC3 with Zones of the previous chapter. As these tools can only verify models with a fixed n∈N , we show the largest model with fixed n that these tools were able to verify in the same time that the above presented technique requires for the verification of the entire parameterized system for all n∈N. Table 4.8 shows the runtimes and sizes of the verified models. The presented incremental workflow (using the optimization Frame1-Feedback) clearly improves the verification of single models with fixed size. Due to its ability to extrapolate inductive strengthenings for larger models, it is able to reason about all n∈N by only verifying small models. The reuse of previous computation results by injecting clauses of the candidate in the next verification run additionally increases the efficiency. Thus, tools capable of only verifying models with fixed n∈N are not able to compete with the presented approach. In the following, we illustrate the importance of inductive strengthenings for validation and reuse. If known, an inductive strengthening can easily be validated as shown in Subsection 3.5.5. Our approach results in an inductive strengthening that can be extrapolated for any n∈N . We show the validation time for Uppaal’s Fischer model ( Fischer_U ). Note, that Uppaal was only able to verify models up to n= 13 and our approach of the previous chapter has verified models up to 114 CHAPTER 4. INCREMENTAL INDUCTIVE VERIFICATION OF PTS Fischer_Un=10 n=20 n=30 n=40 n=50 n=100 Time (s) 0,8 1,5 3,7 6,8 12,7 135,3 Table 4.9: Validation times for the inductive strengthenings computed and extrapolated by the presented approach n= 50. Table 4.9 shows the time needed to validate the extrapolated inductive strengthenings for models with fixed n. Clearly, the approach presented in this chapter performs well. Due to the presented Termination Theorem, such a validation is not necessary. Our incremental workflow provides for a verification for all n∈Nupon success. 4.8 Related Work The related work for IC3 and verification of safety properties for timed automata has been presented in Chapter 2. The following related work is, thus, only concerned with the verification of safety properties for parameterized (timed) systems and symmetry. Parameterized Systems There exist numerous publications concerning the untimed case. It has been shown that this verification question is, in general, undecidable [AK86]. Yet, several works deal with this verification question, resulting in semi-algorithms or working with restricted families of models. The works for parameterized systems might be categorized as follows. Network Invariants: Many of these approaches require human interaction, e.g., the proposition of an invariant or closure. Wolper et al. [WL90] require the manual specification of a network invariant. The invariants are used to check whether the property holds true for the entire set of models. The manual specification, however, is a drawback. A similar finding has been made by Kurshan and McMillan [KM89], where the invariant is denoted as process invariant. It is used for verification of the entire set of models, but needs to be specified manually. Several approaches try to overcome the problem of manual proposition of an invariant. They synthesize invariants automatically, e.g., based on on network grammars and abstraction (Clarke et al. [CGJ95]) or based on a fixpoint computation using heuristics (Lesens et al. [LHR97]). Regular Model Checking: Other approaches are based on reachability analysis with states represented as words and finite state transducers in between. These techniques are denoted as regular model checking and differ by the employed models, transducers and widening operators. Bouajjani et al. were amongst the first to publish about this technique [Bou+00]. Another representative is Kesten et al. [Kes+97] using symbolic model checking. Abdulla et al. extended the techniques in various directions. They examined the effect of having global conditions [Abd+99], and introduced incremental updates to the 4.8. RELATED WORK 115 transducers [Abd+02b]. Further work concerns other improvements [Abd+03] and specific structures [Abd+02a], [BT02]. Symmetry Reduction: In addition to the above techniques some researchers reduce the verification in parameterized systems to the one in a quotient structure, which only includes representatives for symmetric states. Two important works in this field are Emerson et al. [ES96] and Clarke et al. [Cla+96]. Later, Emerson et al. [ES97] and Gyuris et al. [GS97] introduced fairness and on-the fly model checking to the approach. The usage of symmetry in quotient structures was improved by an explicit modeling of symmetric variables, denoted scalarsets, by Ip and Dill [ID96]. This explicit modeling is close to the one employed in our work, where we explicitly define integer variables IVid that are affected by symmetry. However, the technique closest to ours is the following. Invisible Invariants: Pnueli et al. [PRZ01], [Aro+01] introduced an approach that automatically computes strengthenings of properties that may be used to prove the property for all models. To this end, they employ a project-abstract- procedure, where the set of reachable states is computed, which is projected to a smaller model (some references to variables are deleted). Afterwards, the result is abstracted to again include all processes of the model (similar to our extrapolation procedure). The outcome is checked for inductiveness. Additionally, the authors introduce a Small Model Theorem, which states that an inductive strengthening holds for all models, if it holds in the models up to a specific size depending on the structure of the models. This theorem defines a cutoff up to which the models have to be considered only. It is close in spirit to our Termination Theorem, which also defines sort of a cutoff (dynamically checked every iteration). Our theorem, however, is suitable for the incremental workflow with changing candidate formulae every iteration. Apart from the above method, there exist other works that utilize a cutoff for verification. They require specific families of models (e.g., rings [EN95]) to compute a cutoff [EK00] up to which the model needs to be verified in order to guarantee the property to hold for all models. Parameterized Timed Systems In addition to the above related work aiming for untimed models, there exist various, but fewer, publications aiming for parameterized timed systems. One of the first to actually use this terminology was Mahata [Mah05]. Apart from work with Abdulla [Abd+04] in which they use timed petri nets for the modeling of parameterized timed systems, they also reason about decidability for parameterized timed systems in general. Abdulla et al. showed that reachability analysis for timed networks with only a single clock per process is decidable [AJ03]. However, when increasing the number of clocks the reachability question becomes undecidable [ADM04]. Various other works exist that consider parameterized timed systems. Bruttomesso et al. [Bru+12] and Carioni et al. [CGR10] employ SMT-encodings in a decidable fragment in the theory of array for verification. Astefanoaei et al. [Ast+15] 116 CHAPTER 4. INCREMENTAL INDUCTIVE VERIFICATION OF PTS combine locally computed invariants in order to yield invariants for all models. It builds upon the Small Model Theorem of Pnueli transferred to the domain of hybrid automata by Johnson et al. [JM12]. For their own approach, Johnson et al. employ Pnueli’s Project-Abstract-Procedure in a fixpoint computation that searches an inductive strengthening or a counterexample for a fixed number of processes. With its usage of the small model theorem, this work is closest to our approach. As explained above, our Termination Theorem is similar in that is computes a cutoff up to which size the models have to be considered. The main difference, however, is the incremental nature of our theorem, as its applicability to the current candidate formula is checked every cycle. 4.9 Summary The technique presented in this chapter is capable of verifying safety properties for parameterized timed systems given as networks of timed automata. To this end, we employ an incremental workflow that verifies the safety property for models of a fixed size, starting with the smallest one possible. Using the inductive strengthening computed during this verification, we try to reason about the entire parameterized system. If this step fails, the next cycle of the workflow is started with the next larger model. Otherwise, the reasoning in form of our Termination Theorem could be applied and we successfully verified the safety property for the entire parameterized timed system, i.e., for all its models with any number of timed automata. The ability to reason about an entire parameterized system is of high value, as many mutual exclusion algorithms and peer to peer protocols can be modeled as such a system. The benefit is that properties for these algorithms or protocols can be checked for any number of processes executing them. It is a vital aspect when dealing with adaptive systems, as is the case in the context of Industry 4.0. Using our technique allows the verification of the entire parameterized timed system. As an example for the application context, consider its usage during the design phase, which allows the safe reconfiguration of the system during lifetime without the need for further verification. The addition or removal of one of the processes that execute the mutual exclusion algorithm or protocol has already been proven to be safe. This a priori verification of the entire system is a vital aspect when dealing with adaptive and scalable systems. In the following chapter, we will relax some of the restrictions imposed on the models allowed in the presented approach. Our technique will, thus, be applicable to an even larger set of systems, which will greatly improve its practicality. 5 Verification of Extended Parameterized Timed Systems With most of today’s systems being safety critical, model-based design processes offer a structured procedure to ensure a certain quality. They allow the formal modeling and verification of properties during the design phase of a system. However, during this phase, the models might be repeatedly reconfigured until a final design is found. In addition, such reconfigurations may also occur at lifetime of the system, e.g., due to self-adaptation. Since the system’s behavior might change unexpected, these reconfigurations raise the need to redo verifications that have already been done. In such a setting, a rerun of the verification from scratch is not efficient. We have, thus, proposed to reuse the result from the previous verification run. In the previous chapter, we have successfully introduced an incremental technique that follows this paradigm for parameterized timed systems modeled via a timed automaton template. It can be applied for various mutual exclusion algorithms or peer to peer protocols. Its benefit is the verification of the safety property for systems with an arbitrary, but fixed number of processes executing such an algorithm. Considering a running system of such processes, the system is safe (w.r.t. the verified safety property) irrespective of the number of processes. In particular, it implies that a reconfiguration of the system by adding or removing a process is safe and does not require a new verification run. This approach enables an a priori verification of the entire system and, thereby, avoids online verifications during lifetime. In this chapter, we will relax some restrictions imposed on the models for which our technique can be employed to verify safety properties. We broaden the parameterized timed systems that were considered in the previous chapter ( ∀n∈N:[P1|| . . . ||Pn] ). Up to now they consisted of a parameterized number n of instantiations of a process P , which introduced a symmetric state space. The extended parameterized timed systems ( ∀n∈N:[S|| . . . ||R||P1|| . . . ||Pn] ) now additionally include a finite number of extra processes S to R . We also permit a restricted sort of synchronization. As an example, this extension allows to model 117 118 CHAPTER 5. EXTENDED PARAMETERIZED TIMED SYSTEMS an additional communication medium, e.g., a bus. This relaxation provides for a broader applicability of the technique. Up to now, the models were created as networks of timed automata, where the automata are instances of a timed automaton template. The size of the model was given as parameter denoting the number of automata. In the extended formalism, an additional, fixed number of extra timed automata accompany the parameterized number of automata instantiated from the template. These extra automata allow for the modeling of components associated with the parameterized system, e.g., a communication medium or a server in combination with the parameterized number of timed automata modeling clients. Furthermore, we allow a limited sort of synchronization between the timed automata via channels with the restriction that at most one of the symmetric automata must be involved in the synchronization. In the following, we provide the updated definitions used for the models. Afterwards, we redefine the considered swap operations that are used to define the intended notion of symmetry. We briefly recall the workflow and give the proof for our Termination Theorem, before concluding this chapter with a short experiment using one such extended model specifying a gate and controller for a train crossing with an arbitrary number of trains. Note, that the previous chapter is a special case of the formalism introduced below. When considering models without extra timed automata and without synchronization, we receive the formalism and notion of symmetry as before. We start with the redefinition of the employed models. 5.1 Extension of the Modeling Approach The models considered in this chapter are extensions of those from the previous chapter. They additionally allow extra timed automata in the network that are not instantiated from the template, as well as synchronization with the extra automata. The symmetric automata instantiated from the template can not synchronize with each other, as this would invalidate our Termination Theorem employed for the reasoning about the entire parameterized timed system. We first update the definition of templates in order to reflect the added ability to synchronize edges. Note, that the employed synchronization channel is equal in each instantiation, i.e., the synchronization channel does not depend on the automaton’s identifier. In addition, synchronization is only allowed with the extra automata, not among the instantiations of the template. The definition for templates using synchronization is given below. Definition 5.1.1 (Timed Automaton Template using Synchronization) . Let the set Cg of global clocks be given, as well as the global set of integer variables IV = IV6id ∪ IVid as the union of disjoint sets of identifier unaware ( IV6id ) and aware ( IVid ) integer variables, s.t. IV6id ∩ IVid =∅ . In addition, let Σ be the global set of channels. Asymmetric timed automaton template A(pid) using synchronization defined over glob- 5.1. EXTENSION OF THE MODELING APPROACH 119 ally shared Cg , Σ and IV is a tuple A(pid) = (L , l0 , C , IV , Σ , Invc , Invi(pid) , E(pid)) such that •pid ∈N≥1is a unique parameter, called identifier, •Lis a finite set of locations, •l0∈Lis the initial location, •C=Cl∪Cg is the union of the finite and disjoint sets of local and global clocks with initial valuation vc 0, •IV is the finite set of shared integer variables with initial valuation vi 0, •Σis the finite set of shared synchronization channels, •Invc:L→Φ(C)is a total function of clock invariants, s.t. vc 0|=Invc(l0), •Invi(pid):L→Ψ(IV,pid)is a total function of integer invariants, s.t. vi 0|=Invi(pid)(l0), and •E(pid)⊆L×Σsync ×Φ(C)×Ψ(IV , pid)×Ω(IV , pid)× 2 C×L is the set of edges. It must hold that ∀e1∈E with synchronization label a?∈Σsync , there does not exist an edge e2∈Ewith synchronization label a! and vice versa. As before, instantiating a template A(pid) with unique identifier pid =j∈N≥1 results in timed automaton Aj . Unlike before, the networks of timed automata considered in this chapter do not only include instantiations of a template, but additionally contain a finite number of extra timed automata. These supplementary automata have to obey the restrictions for identifier aware integer variables IVid as defined in the previous chapter. Effectively this means that even in the extra automata the variables that are aware of the automata’s identifier can only be applied in restricted constraints and assignments (using each automaton’s own identifier). Otherwise, the symmetry of the state space, on which our approach is based, could be destroyed. We formalize our extended formalism with extra automata below. Definition 5.1.2 (Extended Symmetric Network of Timed Automata) . Given x∈N≥0 extra timed automata A1 to Ax with unique identifiers 1 to x that are defined as in Definition 2.1.8, but with the restrictions on integer variables IVid as above, where in each automaton Ai ( i∈ { 1, . . . , x} ) only instantiated constraints Ψ(IV , i) and assignments Ω(IV , i) are allowed. Given parameter n∈N≥1 and the timed automaton template A(pid) using synchronization as defined in Definition 5.1.1. The Extended Symmetric Network of Timed Automata with x+n timed automata is defined as NTAn=hA1 , . . . , Ax , Ax+1. . . , Ax+ni , where Ai ( i∈ {x+ 1, . . . , x+n} ) is the instantiation of A(pid)with pid =i. Note, that the definition of symmetric networks of timed automata in the previous chapter is a special case of the above redefinition, in which no synchronization is used and x=0 extra automata are given. 120 CHAPTER 5. EXTENDED PARAMETERIZED TIMED SYSTEMS In the following, we illustrate the concept of extra automata in the network with an example first proposed in 1994 [AD94] (here slightly changed). Figure 5.1: Illustration of the Train-Controller-Gate model Example 5.1.3. Consider a train crossing that contains a gate actuated by a controller as depicted in Figure 5.1. Whenever one of a fixed, but arbitrary number of trains is crossing a sensor, the controller receives the signal approaching. It requires 1 time unit to send the lowering signal to the gate. The gate needs at most 1 additional time unit, until the gate is lowered. The train reaches the crossing after at least 3 time units and exits it after at most 5 time units. When exiting, a sensor tells the controller that the train has exited, which needs up to 1 time unit to signal the gate that it should raise. This finishing move requires 1 to 2 time units. Figure 5.2 shows the two timed automata representing the gate (Figure 5.2(a)) and the controller (Figure 5.2(b)), as well as the template that is instantiated to represent the trains (Figure 5.2(c)). Clearly, no identifier aware integer variable is needed in this scenario. It does, however, make use of the added synchronization capabilities introduced in this chapter. As can be seen, all trains use the same synchronization with the extra automata. l0 l2 l1 l3 lower? c:=0 c≤1 raise? c:=0 c≤2 c≥1 (a) Gate l0 l2 l1 l3 approach? c:=0 c≤1 c=1 lower! exit? c:=0 c≤1 raise! (b) Controller l0l1 l2 approach! c:=0 c≤5 c≥3 c≤5 exit! cnt:=cnt+1 cnt:=cnt-1 (c) Train Template Figure 5.2: Train Template and extra timed automata modeling the Controller and Gate The introduction of extra automata in the models does not comply with our previous notion of symmetry, as these extra automata can not be swapped with any other one. Thus, we redefine the intended notion such that it only covers the instantiations of the template. To this end, the swap operation needs to be adapted. 5.2. SYMMETRY 121 5.2 Symmetry The extra automata introduced above are not instantiated from the template like all the other automata. They are, thus, not symmetric, i.e., they can not be used interchangeably and must not be taken into account in the swap operation. The necessary adaptation to the swap operation is given below. It restricts the swap to be only applicable to symmetric timed automata, i.e., those that are instantiated from the same template. As explained, the intuition behind this restriction is that the symmetric automata can be used interchangeably, while all others can’t. Definition 5.2.1 (Swap) . Let an extended network of timed automata NTAn= hA1 ,..., Ax+ni be given as defined in Definition 5.1.2 with concrete semantics TS = (S , s0 , →) . Let A1 to Ax be the extra timed automata and Ax+1 to Ax+n the symmetric timed automata instantiated from template A(pid) as defined in Definition 5.1.1. Aswap π=swapi,j swaps two timed automata Ai and Aj ( i , j∈ {x+ 1, . . . , x+n} ) instantiated from A(pid) . It changes the state s= ((l1 ,..., lx+n) , vc , vi)∈S into the state π(s) = ((π(l1), ..., π(lx+n)),π(vc),π(vi)) ∈Swith •∀k∈ {1, . . . , x+n}:π(lk) =        lii f k =j, lji f k =i, lkelse. •∀c∈Cg:π(vc)(c) = vc(c). •∀k∈ {1, . . . , x+n}:∀c∈Cl k:π(vc)(c) =        vc(ci)i f k =j, vc(cj)i f k =i, vc(c)else, where ci and cj refer clock c in automaton Ai ( c∈Cl i ) and Aj ( c∈Cl j ), respectively. •∀iv ∈ IV6id :π(vi)(iv) = vi(iv). •∀iv ∈ IVid :π(vi)(iv) =        i i f vi(iv) = j, j i f vi(iv) = i, vi(iv)else. Note, that we also use π(m) to denote the identifier of the automaton with which m has been swapped, formally π(m) =        i i f m =j, j i f m =i, m else. The effect of the swap operation is the same as in the previous chapter. It swaps the locations of the two automata, the values of their local clocks, as well as values for identifier aware integer variables that refer to one of the two automata. The only difference is the restriction to be applied only for symmetric timed automata. Again, a permutation involving more than two automata being swapped can easily 128 CHAPTER 5. EXTENDED PARAMETERIZED TIMED SYSTEMS states. Clearly, Consecution of kFkexp(n+1) for NTAn+1 does not hold, which is a contradiction. In summary, we have reached a contradiction in both cases. We demonstrate the practicality of the extended approach in the following. 5.3 Experiments Considering the above example of the train crossing, we have conducted experiments with two distinct safety properties. The first property ρlowered has been presented above (Example 5.2.6) and specifies that the gate has to be closed entirely, when a train is crossing. The second one ( ρoccupied ) denotes that the crossing is not occupied for no reason, i.e., the gate is only lowering, if at least one train is approaching or in the crossing. It is specified via the error state specification err = ((l1 , ∗ , ∗) , true , cnt < 1 ) using an identifier unaware variable cnt that counts the trains that are not far away (that are not in location l0). Our workflow successfully verifies these safety properties. The respective runtimes with and without optimizations are shown in Tables 5.1 and 5.2. Runtime (s) Verified models NTAnfor which n? No Optimization OOM 1-8 Generalization 8,5 ∀n∈N Chockler-Feedback 7,4 ∀n∈N Generalization and Chockler-Feedback 3,6 ∀n∈N using non-generalized set of clauses Generalization and Chockler-Feedback 3,6 ∀n∈N using generalized set of clauses Frame1-Feedback 3,0 ∀n∈N Generalization and Frame1-Feedback 2,6 ∀n∈N using non-generalized set of clauses Generalization and Frame1-Feedback 2,5 ∀n∈N using generalized set of clauses Both-Feedback 4,8 ∀n∈N Generalization and Both-Feedback 3,3 ∀n∈N using non-generalized set of clauses Generalization and Both-Feedback 3,5 ∀n∈N using generalized set of clauses Table 5.1: Verification experiments for the safety property ρlowered and the Train- Controller-Gate model As can be seen, both safety properties have been successfully verified within reasonable time. Again, the optimization of using the Frame1-Feedback has shown to be a good option. 5.4. SUMMARY 129 Runtime (s) Verified models NTAnfor which n? No Optimization OOM 1-7 Generalization 13,0 ∀n∈N Chockler-Feedback OOM 1-9 Generalization and Chockler-Feedback OOM 1-9 using non-generalized set of clauses Generalization and Chockler-Feedback 6,2 ∀n∈N using generalized set of clauses Frame1-Feedback 25,7 ∀n∈N Generalization and Frame1-Feedback 4,6 ∀n∈N using non-generalized set of clauses Generalization and Frame1-Feedback OOM 1-7 using generalized set of clauses Both-Feedback 11,4 ∀n∈N Generalization and Both-Feedback 8,7 ∀n∈N using non-generalized set of clauses Generalization and Both-Feedback OOM 1-7 using generalized set of clauses Table 5.2: Verification experiments for the safety property ρoccupied and the Train- Controller-Gate model 5.4 Summary In summary, the presented extensions to the allowed modeling formalism in our parameterized setting are valuable in that they significantly increase the modeling capabilities without a drawback. They allow the modeling of server-client situations, as well as other effects like a communication medium. The necessary adaptations were small and we were able to use the overall workflow, as well as the Termination Theorem without modifications. The experiments were successful and promising and emphasize the practicality of the approach. Using this extended formalism, our incremental workflow enables the verification of safety properties for a broad number of parameterized timed systems that are composed of a finite number of auxiliary processes accompanying a fixed, but arbitrary large number of instantiations of the same process. This extension adds significant value to our technique. Yet, it’s application area remains the a priori verification of properties for an arbitrary, but fixed number of equal processes. This context is in line with the paradigm of Industry 4.0, which facilitates the adaptation of systems during lifetime. The benefits of our proposed technique for this scenario are obvious. It avoids an online verification by executing an a priori verification, which removes the necessity to verify every single reconfigured model, in which the number of processes has been changed. Other reconfigurations, however, can not be handled using this technique. We will examine the effects of general reconfigurations in the following chapter and give a best-guess approach, as the effects of reconfigurations can not be estimated easily in general. 6 Inductive Verification of Reconfigured Models Timed formalisms are of significant importance for the modeling of today’s systems. As explained, most of these systems are safety critical and, thus, model-based design processes are employed to ensure a certain quality. To this end, formal models are created and properties are verified for these models. During such design procedures, however, the models might repeatedly be reconfigured, resulting in a need to redo the verification. These reconfigurations might also occur later on, e.g., if the model represents an adaptive and self-optimizing system as in Industry 4.0. As every such reconfiguration changes the state space of the model, the desired safety properties need to be verified again. Doing this from scratch is very inefficient, in particular, when considering that the original, similar model has been examined before. In the previous two chapters, we have proposed a technique that verifies safety properties for parameterized timed systems. Within such restricted models, our technique prevents the costly verification from scratch when dealing with reconfigurations that change the number of processes. It does so using an incremental workflow specifically designed for parameterized systems. One of the optimizations presented for this technique, namely the Feedback -loop, is suitable to be used in a general setting. It injects an inductive strengthening computed for the original model into the verification run of the reconfigured model. By doing so, some of the clauses in the inductive strengthening are injected into all frames of the IC3 run, or at least into the frame F1 (see Subsection 4.6.1). Our experiments have shown that this reuse of clauses successfully prevents the costly rediscovery of some of them and, by doing so, speeds up the entire verification run. So far, we have employed this acceleration technique only for symmetric reconfigurations in the setting of parameterized timed systems. In the following, we will try to utilize its benefits for reconfigured models in general and examine 131 132 CHAPTER 6. INDUCTIVE VERIFICATION OF RECONFIGURED MODELS the effectiveness in several experiments. We start with a classification of possible reconfigurations. Taking into account the generality of models expressible with our formalism of networks of timed automata (Chapter 2), several types of reconfiguration are possible as detailed in the following. We characterize reconfigurations of a model within the following three categories: • Addition of new parts to the model, • Deletion of parts of the model, • Replacement/Modification of parts of the model. We illustrate these categories below. Addition Analog to the addition of a symmetric timed automaton as in the previous chapter, other parts can be added to a model. When considering a network of timed automata modeling the interaction of several components in the real world, the addition of an extra timed automaton may represent the addition of a new component interacting with the others. Furthermore, smaller additions are possible. An extra location might model a new discrete state of a system, an edge models additional interaction. Note, that the addition of a part to the model does not always result in additional behavior, e.g., a constraint added to an edge restricts the existing behavior. Deletion In contrast, deleted portions of the model might specify the removal of a part of the system, a state or interaction. These would be performed via the removal of an entire timed automaton in the model, or of a location or edge, respectively. Even smaller changes to the constraints or updates of edges can be considered, where it should be noted that the removal of a constraint might allow additional behavior of the model. As illustrated, the options to modify real-world systems and, in consequence, their models are diverse. The third category contains reconfigurations that are very specific as they replace detailed parts of the model. Replacement In addition to the above mentioned reconfigurations, there exist those that alter parts of the model without addition or deletion. These reconfigurations essentially rely on clock or integer constraints being altered, or assignments and resets being changed. They correspond, for instance, to the adaptation of timing parameters in the modeled systems. The above variety of reconfigurations makes the reuse of previous verification results extremely challenging. In this chapter, we propose a general procedure to employ these results anyhow. It is heavily based on the Feedback -techniques presented in the previous chapter, which allow the reuse of several clauses of an 133 inductive strengthening computed for the original model in order to speed up the verification run for the reconfigured model. Our algorithm presented in Chapter 3 successfully combines the IC3 algorithm with the Zone abstraction for the verification of safety properties for networks of timed automata. In case the safety property is invariant, it yields an inductive strengthening of the safety property as additional outcome. Via an efficient validity check, the inductive strengthening can easily be checked to guarantee the safety property’s invariance for the original model. In combination with a reconfigured model, however, a simple check for validity of the inductive strengthening will most often fail though the safety property is indeed invariant. The reason is that the formula is not inductive for the reconfigured model. The failed inductiveness originates from a changed state space. Depending on the performed reconfiguration, the change to the state space may be drastic. In the previous two chapters, this change was anticipated based on the structure of the models, i.e., the symmetry, via an extrapolation procedure. This procedure adapts the inductive strengthening as anticipated, s.t. it is close to a valid inductive strengthening for the reconfigured model. However, due to the large variety of reconfigurations, the change of state space can not be anticipated in general. In order to give an intuition why the reuse of a formula might be of benefit even without an adaptation, consider the following example. Example 6.0.1. Let the Fischer_U_ 2 model be given as depicted in Figure 3.1. The inductive strengthening of the safety property ρ:=¬(cnt > 1 ) computed by our algorithm IC3 with Zones is listed in the first column of Table 6.1 Fischer_U_2 Fischer_U_2(2048) (int1≤1) (int1≤1) ∧((int06=0)∨(int1≤0)) ∧((int06=0)∨(int1≤0)) ∧(¬l1 0∨l1 1∨(int1≤0)) ∧(¬l1 0∨l1 1∨(int1≤0)) ∧(¬l2 0∨l2 1∨(int1≤0)) ∧(¬l2 0∨l2 1∨(int1≤0)) ∧(l1 0∨(int06=1)∨(int1≤0)) ∧(l1 0∨(int06=1)∨(int1≤0)) ∧(l2 0∨(int06=2)∨(int1≤0)) ∧(l2 0∨(int06=2)∨(int1≤0)) ∧((c1 0≤1024.0)∨(int06=1)∨(c2 0>1024.0)) ∧((c1 0≤2048.0)∨(int06=1)∨(c2 0>2048.0)) ∧((c2 0≤1024.0)∨(int06=2)∨(c1 0>1024.0)) ∧((c2 0≤2048.0)∨(int06=2)∨(c1 0>2048.0)) Table 6.1: Inductive strengthenings computed for the models Fischer_U_ 2 and the reconfigured model Fischer_U_2(2048)as depicted in Figure 6.1 When changing the timing parameters of the Fischer algorithm, a reconfigured model might look as depicted in Figure 6.1. It equals the original model, except that the waiting times that the algorithm adheres to are now doubled. The corresponding inductive strengthening for the reconfigured model computed without the reuse of the original inductive strengthening is listed in the second column of Table 6.1. Clearly, the two inductive strengthenings are similar. In fact, they both consists of eight clauses and differ only at literals referring the time constants. In particular, the first six clauses are exactly the same. Thus, the injection of the former inductive strengthening into the run of our algorithm IC3 with Zones (Chapter 3) to verify the 134 CHAPTER 6. INDUCTIVE VERIFICATION OF RECONFIGURED MODELS cnt:=cnt+1 id:=0; cnt:=cnt-1 id=0 c≤2048 c:=0 id=0 c≤2048 id:=1 c:=0 c>2048 id=1 c:=0 l0 l3 l1 l2 cnt:=cnt+1 id:=0; cnt:=cnt-1 id=0 c≤2048 c:=0 id=0 c≤2048 id:=2 c:=0 c>2048 id=2 c:=0 l0 l3 l1 l2 Figure 6.1: Reconfigured Fischer model Fischer_U_ 2 ( 2048 ) with altered time constants, where all constants 1024 are replaced by 2048 reconfigured model, should prevent the costly rediscovery of these six clauses and, thus, speed up the verification run. However, the injection of a previously computed inductive strengthening might not always be beneficial, as observable in the runtimes depicted in Table 6.2. For the model Fischer_U_ 15 ( 2048 ) with 15 processes, it compares a verification from scratch as described in Chapter 3 to the one that utilizes the inductive strengthening previously computed for the original model Fischer_U_15. We show the results for all three distinct Feedback -techniques presented in the previous chapter ( Chockler - Feedback [Cho+11], Frame 1-Feedback, Both -Feedback). All of them are clearly inferior to a verification from scratch. The reason is that the change in the model is rather drastic (all time constants are changed) resulting in a significant change of the state space concerning the time domain. In addition, the ration of clauses that were of value, i.e., actually occur in the new inductive strengthening computed for the reconfigured model, is rather small (compared to the 6 out of 8 clauses reused for Fischer_U_2(2048)). However, the overall idea of reusing old verification results might be of value in the general setting even so. Interestingly, in the symmetric setting of the previous chapters the reuse could be optimized. The employed extrapolation procedure Runtime (s) Memory (MB) Verification reconfigured model 140,6 267,8 (from scratch) Verification reconfigured model 176,8 287,5 with Chockler-Feedback Verification reconfigured model 245,9 245,1 with Frame1-Feedback Verification reconfigured model 359,5 261,5 with Both-Feedback Table 6.2: Comparison of the runtimes for verification from scratch or using the distinct Feedback-techniques with model Fischer_U_15(2048) 6.1. ADAPTATION OF THE FORMULA 135 adapts the original inductive strengthening in order to reflect the reconfiguration, that is the addition of a symmetric timed automaton. In general, this modification is not mandatory. In the symmetric setting, however, the results proved to be of significant value in form of the presented workflow. Hence, we will examine the feasibility of an adaptation procedure for the general case in the following. 6.1 Adaptation of the Formula Optimally, an adaptation of the inductive strengthening formula according to the applied reconfiguration would result in a valid inductive strengthening for a reconfigured model. To illustrate such an optimal approach, consider the following example. Example 6.1.1. Consider again the original Fischer_U_ 2 model and the reconfigured Fischer_U_ 2 ( 2048 ) model as explained in the previous example. They are depicted in Figures 3.1 and 6.1, where the reconfiguration replaces all time constants 1024 in the original model by the constant 2048. An optimal adaptation of the formula would change all time constants according to the reconfiguration, i.e., replace all constants 1024 in the formula by 2048. The resulting formula is a valid inductive strengthening for the reconfigured model. In fact, it equals the inductive strengthening for the reconfigured model listed before in the second column of Table 6.1. We also performed the adaptation with the Fischer_U_ 15 example above, in which the reuse of the inductive strengthening was unsuccessful. When comparing the runtimes of the verifications, it is obvious that the adapted formula improves on the non-adapted one. The results are shown in Table 6.3, which displays the runtimes of IC3 with Zones with injection of the adapted inductive strengthening using the distinct Feedback -techniques. Furthermore, it includes the runtime of a simple validation of the adapted inductive strengthening as a reference time. The comparison with Table 6.2 shows a significant improvement over the reuse of the original (non-adapted) inductive strengthening and over the verification from scratch. This example represents an optimal setting, where a valid inductive strengthening for the reconfigured model could be produced by adapting the inductive strengthening for the original model. It is, however, not representative, as many challenges hinder such perfect adaption in the usual case. This is due to the fact that the impact of a reconfiguration can hardly be estimated, in particular if the reconfiguration is more complex. In the following, we propose adaptations to the formula for the three distinct categories of reconfigurations shown above. Adaptation to Addition-Reconfigurations The impossibility of an adaptation can best be observed when considering reconfigurations that include the addition of parts to the model. In general, an additional timed automaton, as well as additional edges or locations in existing automata introduce additional behavior in interaction with the original parts of the model. This means the state space may change in 136 CHAPTER 6. INDUCTIVE VERIFICATION OF RECONFIGURED MODELS Runtime (s) Memory (MB) Validation of adapted inductive strengthening 1,1 48,4 Verification reconfigured model 36,6 100,0with Chockler-Feedback (adapted inductive strengthening) Verification reconfigured model 25,8 82,8with Frame1-Feedback (adapted inductive strengthening) Verification reconfigured model 36,7 102,2with Both-Feedback (adapted inductive strengthening) Table 6.3: Comparison of the runtimes for validation and verification injecting the adapted formula using the distinct Feedback -techniques with model Fischer_U_15(2048) various ways, which can not be estimated without knowledge about any structural characteristics like symmetry. Thus, a perfect adaptation of the original inductive strengthening is not feasible in general. For reconfigurations that include the addition of parts, we are unable to adapt the formula, as we can not estimate the changed state space. In consequence, the formula remains unchanged with the hope that the state space has not changed, or at least is similar to the original one. Adaptation to Deletion-Reconfigurations The same argumentation holds true when considering reconfigurations including the deletion of parts of the model. As above, the effect on the state space can hardly be estimated. For illustration purpose, consider the deletion of a single constraint. Its removal weakens the restrictions on an edge or location and might allow for additional behavior that might increase the reachable portion of the state space, s.t. a state violating the safety property is now reachable. Adapting the inductive strengthening of the safety property according to these changes in the state space is not feasible. However, when considering the removal of other parts of a model, e.g., an entire timed automaton, the formula can, and in fact must, be adapted to reflect this change. It would otherwise include variables that do not exist in the encoding of the model. Thus, we adapt the formula as follows. There might exist literals in some of the clauses of the formula that refer to deleted parts removed during the reconfiguration. We propose two distinct options how these literals can be handled. Definition 6.1.2 (Adaptation to Deleted Parts) . Let an inductive strengthening F of a safety property be computed for an original model NTA . We adapt the formula kFk concerning parts of the model deleted in a reconfiguration as follows. For each clause c in kFk that includes at least one literal referring a nonexistent part (clock, location or integer variable) in the reconfigured model, we either 6.1. ADAPTATION OF THE FORMULA 137 • Delete the entire clause, or • Delete all disjuncts that refer nonexistent parts in the reconfigured model. This approach is illustrated in the following example. Example 6.1.3. Consider a model and a reconfiguration in which a local clock c0 in timed automaton with identifier 1 is deleted. As a result, the respective clock variable c1 0 must not be used and has to be removed from the inductive strengthening formula. However, simply deleting the clock variable is not an option, as it would result in an invalid formula that includes deformed constraints. Considering the clause l1 0∨(c1 0≥ 1 ) illustrates this issue. Deleting the clock variable c1 0 encoding clock c0 in timed automaton with identifier 1 results in the invalid formula l1 0∨(≥ 1 ) . The above presented procedures of deleting the entire clause or only the affected literals yield distinct results. Either the clause is discarded in its entirety or the disjunct (c1 0≥1)is removed resulting in clause l1 0. Adaptation to Replacement-Reconfigurations Lastly, reconfigurations that alter the model by specific replacements of parts offer the best chance to adapt the inductive strengthening accordingly. This is due to the structure of these reconfigurations, where the model is modified without addition or deletion. Thus, these reconfigurations include the modification of constraints, assignments and sets of clocks to be reset. The latter two modifications (reset clocks and assignments) are of various effect and, thus, remain without adaptation of the inductive strengthening formula, much like the addition or deletion of parts. Changes on constraints, however, can be handled partly as we will see in the following. Basically, the changes in constraints that can be handled are those that replace constants. As explained in Chapter 3, the constraints are incorporated in the predecessor computation within the weakest precondition computation. To this end, they may be combined with other constraints (for example in the All-Pairs-Shortest-Paths algorithm for the backwards computation of the predecessor zone) or be combined with clock resets or assignments (for integer variables). As a result, the constraints may occur modified or unmodified in the inductive strengthening, or don’t occur at all. Hence, the chances for a reasonable adaptation of the formula can be very diverse. Best Case: Whenever the reconfigured constraint can be uniquely related to parts of the formula, an adaptation is easy, e.g., whenever all constraints in the model are unique and occur unmodified in the formula. For illustration, again consider Example 6.1.1. All constraints in the model are changed and the adaptation of the formula can, thus, be easily performed by replacing all constants in the formula. Since all constraints are changed, it does not matter whether the literal (c1 0≥ 1024 ) refers the invariant constraint of location l1 or the guard constraint of the edge between locations l1and l2. Problematic Mapping: The lack of said knowledge, however, results in the question which parts of the formula should be replaced. Since no reliable information is given