Probabilistic model checking is a powerful formal verification method that can ensure the correctness of real-life systems that exhibit stochastic behaviour. The work presented in this thesis aims to solve the scalability challenge of probabilistic model checking, by developing, for the first time, fully-automated compositional verification techniques for probabilistic systems. The contributions are novel approaches for automatically learning probabilistic assumptions for three different compositional verification frameworks. The first framework considers systems that are modelled as Segala probabilistic automata, with assumptions captured by probabilistic safety properties. A fully-automated approach is developed to learn assumptions for various assume-guarantee rules, including an asymmetric rule Asym for two-component systems, an asymmetric rule Asym-N for n-component systems, and a circular rule Circ. This approach uses the L* and NL* algorithms for automata learning. The second framework considers systems where the components are modelled as probabilistic I/O systems (PIOSs), with assumptions represented by Rabin probabilistic automata (RPAs). A new (complete) assume-guarantee rule Asym-Pios is proposed for this framework. In order to develop a fully-automated approach for learning assumptions and performing compositional verification based on the rule Asym-Pios, a (semi-)algorithm to check language inclusion of RPAs and an L*-style learning method for RPAs are also proposed. The third framework considers the compositional verification of discrete-time Markov chains (DTMCs) encoded in Boolean formulae, with assumptions represented as Interval DTMCs (IDTMCs). A new parallel operator for composing an IDTMC and a DTMC is defined, and a new (complete) assume-guarantee rule Asym-Idtmc that uses this operator is proposed. A fully-automated approach is formulated to learn assumptions for rule Asym-Idtmc, using the CDNF learning algorithm and a new symbolic reachability analysis algorithm for IDTMCs. All approaches proposed in this thesis have been implemented as prototype tools and applied to a range of benchmark case studies. Experimental results show that these approaches are helpful for automating the compositional verification of probabilistic systems through learning small assumptions, but may suffer from high computational complexity or even undecidability. The techniques developed in this thesis can assist in developing scalable verification frameworks for probabilistic models.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Thèse numérisée par la Direction des bibliothèques de l'Université de Montréal.

Model checking is an automatic formal verification technique for establishing correctness of systems. It has been widely used in industry for analysing and verifying complex safety-critical systems in application domains such as avionics, medicine and computer security, where manual testing is infeasible and even minor errors could have dire consequences. In our increasingly parallelised world, concurrency has become pivotal and seamlessly woven within programming paradigms, however, extremely challenging when it comes to modelling and establishing correctness of intended behaviour. Tools for model checking concurrent systems face severe limitations due to scalability problems arising from the need to examine all possible interleavings (schedules) of executions of parallel components. Moreover, concurrency poses additional challenges to model checking, giving rise to phenomena such as nondeterminism, deadlock, livelock, etc. In this thesis we focus on adapting and developing novel model-checking techniques for concurrent systems in the setting of the process algebra CSP and its primary model checker FDR. CSP allows for a compact modelling and precise analysis of event-based concurrency, grounded on synchronous message passing as a fundamental mechanism of inter-component communication. In particular, we investigate techniques based on symbolic model checking, static analysis and abstraction, all of them exploiting the compositionality inherent in CSP and targeting to increase the scale of systems that can be tractably analysed. Firstly, we investigate symbolic model-checking techniques based on Boolean satisfiability (SAT), which we adapt for the traces model of CSP. We tailor bounded model checking (BMC), that can be used for bug detection, and temporal k-induction, which aims at establishing inductiveness of properties and is capable of both bug finding and establishing the correctness of systems. Secondly, we propose a static analysis framework for establishing livelock freedom of CSP processes, with lessons for other concurrent formalisms. As opposed to traditional exhaustive state-space exploration, our framework employs a system of rules on the syntax of a process to calculate a sound approximation of its fair/co-fair sets of events. The rules either safely classify a process as livelock-free or report inconclusiveness, thereby trading accuracy for speed. Finally, we develop a series of abstraction/refinement schemes for the traces, stable-failures and failures-divergences models of CSP and embed them into a fully automated and compositional CEGAR framework. For each of those techniques we present an implementation and an experimental evaluation on a set of CSP benchmarks.

Gegenstand der Arbeit ist die Verifikation von verteilten diskreten Systemen in bezug auf Spezifikationen ihres Verhaltens. Diskrete Systeme bestehen aus einer abzaehlbaren Zustandsmenge und einer Zustandsuebergangsrelation. Bei verteilten Systemen ist eine signifikante Zahl von Zustandsuebergaengen nur durch eine kleine Zahl von Komponenten eines strukturierten Zustandsraumes bedingt und aendert auch nur wenige Komponenten. Bei praktisch relevanten Systemen ist die Zustandszahl unbeherrschbar gross. Dieses Phaenomen wird Zustandsraumexplosion genannt. Verteiltheit gilt als eine der wesentlichen Ursachen fuer Zustandsraumexplosion, weil nebenlaeufig moegliche lokale Zustandsuebergaenge abhaengig von ihren exponentiell vielen Ausfuehrungsreihenfolgen exponentiell viele verschiedene Zwischenzustaende erzeugen koennen. Fuer Verifikationsaufgaben sind Systeme daher implizit gegeben durch eine Beschreibung von Anfangszustaenden und (lokale) Regeln zur Generierung von Folgezustaenden. Solche Systembeschreibungen folgen verschiedenen Paradigmen, z.B. dem variablenorientierten Paradigma (Zustaende sind Werte von Variablen, die durch Zustandsuebergaenge gelesen und geschrieben werden) oder dem ressourcenorientierten Paradigma (Zustaende sind Verteilungen von Ressourcen im System, die durch Zustandsuebergaenge konsumiert oder produziert werden). Die Verfuegbarkeit von Verifikationstechniken oder spezifischen Implementationen haengt vom zugrundeliegenden Paradigma ab. Als Sprache zur Formulierung von Spezifikationen des Verhaltens verwenden wir etablierte temporale Logiken und fuer die Praxis bedeutsame Fragmente solcher Logiken. Temporale Logik beschreibt Eigenschaften von Abfolgen von Zustaenden, basierend auf elementaren, einzelne Zustaende betreffenden Eigenschaften. Auf einer expliziten Systemdarstellung lassen sich temporallogische Eigenschaften effizient, d.h. mit einer linear von der Zustandszahl abhaengigen Laufzeit, verifizieren. Eine solche Verifikation basiert auf einfachen Suchalgorithmen in dem durch das System definierten Zustandsgraph. Ein solcher Verifikationsansatz ist aber wegen der genannten Zustandsraumexplosion nicht durchfuehrbar. Im wesentlichen werden drei Loesungsansaetze in Richtung durchfuehrbarer Verifikationsalgorithmen verfolgt. Die strukturelle Verifikation versucht, Eigenschaften direkt aus spezifischen Mustern in der impliziten Systembeschreibung abzuleiten. Der derzeitige Stand der Technik gestattet solche Ableitungen nur fuer wenige und einfach strukturierte Verhaltensspezifikationen und erfordert auch dann in einigen Faellen recht aufwendige Berechnungen. Bei der symbolischen Zustandsraumanalyse wird der Zustandsraum erschoepfend durchmustert, allerdings unter Benutzung von Datenstrukturen, deren elementare Objekte ganze Mengen von Zustaenden beschreiben, und deren elementare Operationen die Folgezustaende fuer ganze solche Mengen aus der impliziten Systembeschreibung errechnen. Bei der expliziten Zustandsraumverifikation, dem Thema der vorliegenden Habilitationsschrift, wird eine explizite Repraesentation eines Zustandsraumes generiert, der wesentlich kleiner ist als der Zustandsraum des untersuchten Systems, in bezug auf die untersuchte Eigenschaft aber per Konstruktion aequivalent zum originalen System ist. Zur Konstruktion werden Informationen aus der impliziten Systembeschreibung herangezogen. Eine Technologie zur expliziten Zustandsraumverifikation besteht also aus - Einer mathematisch fundierten Theorie, die einer bestimmten Konstruktionsmethode bescheinigt, welche Eigenschaften durch sie bewahrt werden; - effizienten Algorithmen zur Implementation eine solchen Konstruktion; Die Arbeit enthaelt, fuer mehrere bekannte Verfahren, Beitraege zu jeweils mindestens einem der beiden Bestandteile einer expliziten Zustandsraumverifikationstechnik. Die Methode der sturen Mengen verkleinert den explizit zu konstruierenden Zustandsraum dadurch, dass von den in einem Zustand moeglichen Zustandsuebergaengen nur einige tatsaechlich untersucht werden, so dass weit weniger Zwischenzustaende durch verschiedene Abfolge nebenlaeufiger lokaler Zustandsuebergaenge entstehen. Die zu untersuchenden Uebergaenge werden abhaengig von der zu verifizierenden Eigenschaft und Informationen aus der Systemstruktur so ausgewaehlt, dass zu jeder Klasse von fuer die Eigenschaft relevanten Systemablaeufen wenigstens einer im reduzierten Zustandsraum repraesentiert ist. Die erste 1988 veroeffentlichte Methode diente der Bewahrung von terminalen Zustaenden sowie mindestens eines Pfades unendlicher Laenge. In der Folge wurde diese Technik auf viele andere Klassen von Eigenschaften erweitert, wobei vor allem die Faehigkeit, einen unendlichen Pfad zu bewahren, dahingehend verfeinert wurde, dass gezielt Pfade mit bestimmten Eigenschaften bewahrt werden konnten. Dabei spielte das Konzept unsichtbarer Zustandsuebergaenge eine tragende Rolle, wobei ein unsichtbarer Zustandsuebergang die Eigenschaft hat, dass er keine fuer die Eigenschaft relevanten Zustandskomponenten aendert. Daher war die Anwendung der Methode sturer Mengen begrenzt auf lokale Systemeigenschaften, weil andereseits zu wenige unsichtbare Uebergaenge fuer eine substantielle Reduktion zur Verfuegung stuenden. In der vorliegenden Arbeit setzen wir an der ersten Arbeit zur Methode sturer Mengen an und verfeinern die Faehigkeit, terminale Zustaende zu bewahren, dahingehend, dass nun die Praesenz von Zustaenden mit beliebigen in temporaler Logik formulierbaren Eigenschaften bewahrt werden. Die neue Methode basiert nicht auf der Existenz unsichtbarer Uebergaenge und kann in der Tat auch bei der Verifikation globaler Systemeigenschaften zu substantieller Reduktion fuehren. Das neue Konzept zur Konstruktion des reduzierten Zustandsraumes sind sogenannte UP-Mengen. Eine UP-Menge ist eine Menge von Uebergaengen, von denen mindestens einer in einem Systemablauf von einem Zustand, der die untersuchte Eigenschaft nicht erfuellt, zu einem Zustand, der die Eigenschaft erfuellt, vorkommen muss. Wir geben Algorithmen an, die kleine UP-Mengen fuer beliebige Zustaende aus der impliziten Systembeschreibung und einer Repraesentation der untersuchten Eigenschaft in der temporalen Logik CTL berechnet. Wir zeigen, dass jede Konstruktion, die in einem Zustand alle Uebergaenge in einer schwach sturen Obermenge einer zu dem Zustand berechneten UP-Menge untersucht, alle Zustaende erreicht, die die Eigenschaft besitzen. Dabei ist die Konstruktion schwach sturer Mengen die allen Methoden sturer Mengen gemeinsame Grundkonstruktion. Symmetrische Reduktion verkleinert den zu untersuchenden Zustandsraum dadurch, dass zu jeder Klasse von in bezug auf Symmetrie aequivalenten Zustaenden jeweils nur einer weiterverfolgt wird. Dadurch lassen sich alle gegenueber Symmetrie insensitive Eigenschaften bewahren (wobei man oft Insensitivitaet einer Eigenschaft durch die geeignete Wahl der Symmetrienmenge erreichen kann). Symmetrische Reduktion beinhaltet zwei Probleme, erstens das Aufinden der einem System innewohnenden Symmetrie, und zweitens, zu einem gegebenen Zustand, das Auffinden zu ihm aequivalenter Zustaende in der Menge bereits untersuchter Zustaende. Die meisten vorhandenen Implementationen leiten Symmetrien aus speziellen Datenstrukturen ab, in denen wegen der eingeschraenkten Operationen die verschiedenen Elemente des Typs austauschbar sind. Das Auffinden aequivalenter Zustaende wird durch eine Transformation neu berechnter Zustaende in einen aequivalenten kanonischen Repraesentanten realisert. Alternativ zu diesem Ansatz wurde zur Beschreibung von Symmetrien die Verwendung von Graphautomorphismen auf netzartigen impliziten Systembeschreibungsformen vorgeschlagen. Es zeigt sich, dass per Umwandlung von Datenabhaengigkeiten in Graphrepraesentationen, jede Datentypsymmetrie auch einen Graphautomorphismus bildet, andererseits aber durch Graphautomorphismen Symmetrien beschreibbar sind, die sich in Datentypbetrachtungen nicht wiederfinden lassen. Diese zusaetzlichen Symmetrien erlauben eine staerkere Reduktion des Zustandsraumes. Zur Graphautomorphismentechnik fehlten bislang leistungsfaehige Algorithmen zur Umsetzung dieser Technologie. Wir setzen an der auf Graphautomorphismen basierenden Methode an und unterlegen alle Teilprobleme mit leistungsfaehigen Algorithmen. Die Berechnung der Automorphismen beschraenken wir auf ein Erzeugendensystem, das polynomiell viele Elemente, gemessen an der Groesse der impliziten Systembeschreibung, hat. Die Berechnung selbst ist schlimmstenfalls exponentiell, was nicht verwundert, weil das Problem mit einem Entscheidungsproblem eng korreliert, von dem bekannt ist, dass es in der Klasse NP, aber unbekannt, ob es NP-vollstaendig oder in P liegt. Diese Eigenschaft hat dem Problem eingehende Untersuchung zuteil werden lassen, wegen der nach wie vor offenen "P ungleich NP?"-Frage. Trotzdem ist kein polynomieller Algorithmus bekannt. Umso erfreulicher ist es, dass unser Berechnungsalgorithmus sich auf realistischen Beispielen bisher durchweg polynomiell verhielt, und lediglich bei eigens konstruierten Systemen ins Exponentielle ausriss. Fuer die Loesung des Problems, aequivalente bereits bekannte Zustaende aufzuspueren, schlagen wir mehrere Techniken vor und beschreiben ihre Leistungsfaehigkeit abhaengig von der Struktur der innewohnenden Symmetrie. Fuer duenne Symmetriegruppen (wenige symmetrische Transformationen) eignet sich eine Technik, bei der die Symmetrien der Reihe nach aus dem Erzeugendensystem generiert werden, und das symmetrische Bild des neuen Zustandes mit der Menge der bekannten Zustaende verglichen wird. Dabei koennen wir, abhaengig vom Ausgang einer solchen Ueberpruefung, die Generierung von Symmetrien unterdruecken, von denen aus vorhandenen Informationen klar ist, dass sie keinesfalls zum Erfolg fuehren. Dadurch kann eine erhebliche Effizienzsteigerung erzielt werden. Bei einer zweiten Technik iterieren wir die bekannten Zustaende, genauer gesagt, diejenigen Zustaende, die fuer eine die Symmetrie respektierende Hashfunktion denselben Wert liefert wie der neue Zustand, ob es eine Symmetrie gibt, die beide Zustaende ineinander ueberfuehrt. Das verbleibende Problem kann durch eine Adaption des Symmetrieberechnungsverfahrens geloest werden. Eine vorherige Berechnung des Erzeugendensystems kann entfallen. Die dritte vorgeschlagene Technik benutzt das Erzeugendensystem, um den neuen Zustand approximativ in einen kanonischen aequivalenten Zustand zu ueberfuehren. Diese Technik ist von allen beschriebenen Methoden die effizienteste, liefert aber groessere Zustandsraeume als die beiden anderen Techniken. Wir studieren die Vor- und Nachteile aller Techniken anhand mehrerer Beispielsysteme. Die dritte in der Arbeit behandelte Technik ist die Methode der Ueberdeckbarkeitsgraphen. Sie ist spezifisch fuer die ressourcenbasierte Systembeschreibungsform der Petrinetze. Sie diente urspruenglich zur Aufspuerung von Stellen im System, an denen sich unbeschraenkt viele Ressourcen ansammeln koennen. Formal ist ein Ueberdeckbarkeitsgraph eine endliche Abstraktion eines Systems mit bis zu unendlich vielen Zustaenden. Von nur wenigen Eigenschaften war bekannt, dass sie sich aus dem Ueberdeckbarkeitsgraphen ableiten lassen. Wir formulieren Regeln zur Auswertung von Ueberdeckbarkeitsgraphen, mit deren Hilfe es moeglich ist, eine Vielzahl von in temporaler Logik formulierten Eigenschaften aus dem Ueberdeckbarkeitsgraph abzuleiten. Diese Reglen sind inhaerent unvollstaendig, da bekannt ist, dass fuer viele Eigenschaften es Paare von Systemen gibt, die isomorphe Ueberdeckbarkeitsgraphen liefern, sich aber in bezug auf die Eigenschaft verschieden verhalten. Fuer universelle Eigenschaften des CTL-Fragments ACTL erhalten wir Bewahrungsresultate durch das Ausweisen einer Simulationsrelation zwischen dem originalen System und seinem Ueberdeckbarkeitsgraph. Fuer existentielle Eigenschaften basieren unsere Resultate auf einer Abschwaechung der Erfuellbarkeitsrelation ueber Zustaenden des Ueberdeckbarkeitsgraphen. Einem Zustand des Ueberdeckbarkeitsgraphen entsprechen divergierende Folgen von Zustaenden des Originalgraphen. Normalerweise schreibt man einem Zustand des Ueberdeckbarkeitsgraphen dann eine Eigenschaft zu, wenn alle Folgenglieder im Originalsystem die Eigenschaft besitzen. Wir arbeiten dagegen mit einem Begriff, wo Gueltigkeit der Eigenschaft nur fuer fast alle Folgenglieder gefordert wird. Eine letzte Gruppe von Techniken ist bisher in der Zustandsraumverifikation nicht eingestzt worden, aber aus der strukturellen Verifikation fuer Petrinetze bekannt. Zu einem Petrinetz kann eine ganzzahlige Inzidenzmatrix C gebildet werden, mit deren Hilfe ein linear-algebraischer Zusammenhang zwischen voneinander errichbaren Zustaenden hergestellt werden kann. Stellen- und Transitionsinvarianten sind Loesungen der durch C-T bzw. C definierten homogenen Gleichungssysteme. Dabei dienen Stelleninvarianten gewoehnlich einer Abschaetzung der Menge der erreichbaren Zustaende nach oben, mit daraus resultierenden Moeglichkeiten der Ableitung von Eigenschaften, waehrend Transitionsinvarianten Zyklen im Zustandsraum charakterisieren. Wir verwenden Stelleninvarianten zur Kompression von einzelnen Zustaenden. Durch Stelleninvarianten lassen sich einige Komponenten in einen funktionalen Zusammenhang zu den verbleibenden Komponenten stellen. Dadurch ist auch nach dem Streichen der funktional abhaengigen Stellen der Zustand noch eindeutig determiniert. Wir zeigen, dass bei der Konstruktion des Zustandsraumes ein durch die verbleibenden Stellen gebildeter "Fingerabdruck" ausreicht. Transitionsinvarianten verwenden wir dazu, eine Menge von Zustaenden so auszuzeichnen, dass jeder Zyklus im Zustandsraum mindestens einen ausgezeichneten Zustand enthaelt. Darufhin speichern wir noch noch ausgezeichnete Zustaende permanent, sparen also Speicherplatz. Fuer nicht ausgezeichnete Zustaende kann es passieren, dass sie mehrmals aufgesucht werden (auf verschiedene Weise aus Vorgaengerzustaenden entstehen). Weil sie nicht gespeichert sind, werden auch wiederholt ihre Nachfolgezustaende untersucht. Da in jedem Kreis mindestens ein ausgezeichneter, also permanent zu speichernder Zustand enthalten ist, entstehen durch diese wiederholte Berechnung keine Probleme in bezug auf Terminierung des Verfahrens, wohl aber erhebliche Laufzeiteinbussen. Wir schlagen Methoden zur Begrenzung der Laufzeiteinbussen um den Preis weiterer zu speichernder Zustaende vor. Fuer alle untersuchten Methoden studieren wir die Abhaengigkeit der Anwendbarkeit und Effizienz der Methode von dem der gegebenen impliziten Systembeschreibung zugrundeliegenden Paradigma. Wir untersuchen ebenfalls die Kompatibilitaet der Verfahren mit verschiedenen Strategien zur Generierung des Zustandsraumes (Tiefe zuerst, Breite zuerst, verteilt) und Moeglichkeiten der gemeinsamen Anwendung verschiedener Techniken. / Verification is the task of determining whether a (model of a) system holds a given behavioral property. State space verification comprises a class of computer aided verification techniques where the property is verified through exhaustive exploration of the reachable states of the system. Brute force implementations of state space verification are intractable, due to the well known state explosion problem. Explicit state space verification techniques explore the state space one state at a time, and rely usually on data structures where the size of the data structure increases monotonously with an increasing number of explored states. They alleviate state explosion by constructing a reduced state space that, by a mathematically founded construction, behaves like the original system with respect to the specified properties. Thereby, decrease of the number of states in the reduced system is the core issue of a reduction technique thus reducing the amount of memory required. An explicit state space verification technique comprises of - a theory that establishes whether, and how, certain properties can be preserved through a construction of a reduced state space; - a set of procedures to execute the actual construction efficiently. In this thesis, we contribute to several existing explicit state space verification techniques in either of these two respects. We extend the class of stubborn set methods (an instance of partial order reduction) by constructions that preserve previously unsupported classes of properties. Many existing constructions rely on the existence of "invisible" actions, i.e. actions whose effect does not immediately influence the verified property. We propose efficient constructions that can be applied without having such invisible actions, and prove that they preserve reachability properties as well as certain classes of more complex behavioral system properties. This way, so called "global" properties can now be approached with better stubborn set methods. We pick up a graph automorphism based approach to symmetry reduction and propose a set of construction algorithms that make this approach feasible. In difference to established symmetry techniques that rely on special "symmetry creating" data types, a broader range of symmetries can be handled with our approach thus obtaining smaller reduced state spaces. Coverability graph construction leads to a finite representation of an infinite state space of a Petri net by condensing diverging sequences of states to their limit. We prove rules to determine temporal logic properties of the original system from its coverability graph, far beyond the few properties known to be preserved so far. We employ the Petri net concept of linear algebraic invariants for compressing states as well as for leaving states out of explicit storage. Compression uses place invariants for replacing states by smaller fingerprints that still uniquely identify a state (unlike many hash compression techniques). For reducing the number of explicitly stored states, we rely on the capability of Petri net transition invariants to characterize cycles in the state space. For termination of an exhaustive exploration of a finite state space, it is sufficient to cover all cycles with explicitly stored states. Both techniques are easy consequences of well known facts about invariants. As a novel contribution, we observe that both techniques can be applied without computing an explicit representation of (a generating set for) the respective invariants. This speeds up the constructions considerably and saves a significant amount of memory. For all presented techniques, we illustrate their capabilities to reduce the complexity of state space reduction using a few academic benchmark examples. We address compatibility issues, i.e. the possibility to apply techniques in combination, or in connection with different strategies for exploring the reduced state space. We propose a scheme to distribute state space exploration on a cluster of workstations and discuss consequences for using this scheme for state space reduction. We collect observations concerning the impact of the choice of system description formalisms, and property specification languages, on the availability of explicit state space verification techniques.

Feature-oriented software architecture is a way of organizing code around the features that the program provides instead of the program's objects and components. In the development of a feature-oriented software system, the developers, supplied with a set of features, select and organize features to construct the desired system. This approach, by better aligning the implementation of a system with the external view of users, is believed to have many potential benefits such as feature reuse and easy maintenance. However, there are challenges in the formal verification of feature-oriented systems: first, the product may grow very large and complicated. As a result, it's intractable to apply the traditional formal verification techniques such as model checking on such systems directly; second, since the number of feature-oriented products the developers can build is exponential in the number of features available, there may be redundant verification work if doing verification on each product. For example, developers may have shared specifications on different products built from the same set of features and hence doing verification on these features many times is really unnecessary. All these drive the need for modular verifications for feature-oriented architectures. Assume-guarantee reasoning as a modular verification technique is believed to be an effective solution. In this thesis, I compare two verification methods of this category on feature-oriented systems and analyze the results. Based on their pros and cons, I propose a new modular model checking method to accomplish verification for sequential feature compositions with cyclic connections between the features. This method first builds an abstract finite state machine, which summarizes the information related to checking the property/specification from the concrete feature design, and then applies a revised CTL model checker to decide whether the system design can preserve the property or not. Proofs of the soundness of my method are also given in this thesis.

Le travail présenté dans ce mémoire concerne une méthode de conception sûre de systèmes(COTS). Un COTS est un composant matériel ou logiciel générique qui est naturellement conçu pour être réutilisable et cela se traduit par une forme de flexibilité dans la mise en oeuvre de sa fonctionnalité : en clair, une même fonction peut être réalisée par un ensemble (potentiellement infini) de scénarios différents, tous réalisables par le COTS. La complexité grandissante des fonctions implémentées fait que ces situations sont très difficiles à anticiper d’une part, et encore plus difficiles à éviter par un codage correct. Réaliser manuellement une fonction composite correcte sur un système de taille industrielle, s’avère être très coûteuse. Elle nécessite une connaissance approfondie du comportement des COTS assemblés. Or cette connaissance est souvent manquante, vu qu’il s’agit de composants acquis, ou développés par un tiers, et dont la documentation porte sur la description de leur fonction et non sur sa mise en IJuvre. Par ailleurs, il arrive souvent que la correction manuelle d’une faute engendre une ou plusieurs autres fautes, provoquant un cercle vicieux difficile à maîtriser. En plus, le fait de modifier le code d’un composant diminue l’avantage lié à sa réutilisation. C’est dans ce contexte que nous proposons l’utilisation de la technique de synthèse du contrôleur discret (SCD) pour générer automatiquement du code de contrôle commande correct par construction. Cette technique produit des composants, nommés contrôleurs, qui agissent en contraignant le comportement d’un (ou d’un assemblage de) COTS afin de garantir si possible la satisfaction d’une exigence fonctionnelle. La méthode que nous proposons possède plusieurs étapes de conception. La première étape concerne la formalisation des COTS et des propriété de sûreté et de vivacité (P) en modèles automate à états et/ou en logique temporelle. L’étape suivante concerne la vérification formelle du modèle d’un(des) COTS pour l’ensemble des propriétés (P). Cette étape découvrir les états de violation des propriétés (P) appelés états d’erreur. La troisième étape concerne la correction automatique des erreurs détectées en utilisant la technique SCD. Dans cette étape génère on génère un composant correcteur qui sera assemblé au(x) COTS original(aux) pour que leur comportement général respecte les propriétés souhaitées. L’étape suivante concerne la vérification du système contrôlé pour un ensemble de propriétés de vivacité pour assurer la passivité du contrôleur et la vivacité du système. En fin, une étape de simulation est proposée pour observer le comportement du système pour quelque scénarios intéressent par rapport à son implémentation finale. / This PhD dissertation contributes to the safe design of COTS-based control-command embedded systems. Due to design constraints bounding delays, costs and engineering resources, component re-usability has become a key issue in embedded design. Our proposal is a design method which ensures correction of COTS-based designs. This method uses in synergy a number of design techniques and tools. It starts from modeling of the COTS components which are stored in a generic COTS library, and ends with a design of the global control-command system, verified to be free of errors and ready to be implemented over a hardware chip such as an ASIC or an FPGA "Field Programmable Gate Array". The designer starts by modeling the temporal and logical local preconditions and postconditions of each COTS component, then the global pre/post conditions of the assembly which are not necessary a simple combination of local properties. He models also a list of properties that must be satisfied by the assembly. Any violation of these properties is defined as a design error. Then, by using the model checking approach the model of the assembly is verified against the predefined local and global properties. Some design errors can be corrected automatically through the Discrete Controller Synthesis method (DCS), others however must be manually corrected. After the correction step, the controlled control-command system is verified. Finally a global simulation step is proposed in order to perform a system-level verification beyond the capabilities of available formal tools. We apply the method on two different systems, one concerns transferring data from senders to receivers through FIFO unit, the other is controlcommand system of a train passengers’ access.

Este trabalho reflete os esforcos realizados no estudo das principais técnicas automaticas de verificacao de sistemas que podem ser modelados em Maquinas de Estados Finitas, em particular as que normalmente se enquadram dentro da denominacao de model checking (verificacao de modelos). De modo a permitir ao leitor uma compreensao das vantagens e desvantagens de cada tecnica, os fundamentos teoricos de cada uma delas sao apresentados e ilustrados atraves de exemplos. Alem de uma apresentacao da teoria associada a cada tecnica, esta dissertação ainda apresenta dois estudos de caso de interesse bastante pratico: a verificacao de propriedades de um sistema de manufatura originalmente modelado atraves de uma rede de Petri e a verificacao de propriedades do intertravamento de uma seção metroviaria. Os dois estudos de caso utilizam tecnicas denominadas simbolicas. No primeiro estudo de caso, propoe-se que as invariantes obtidas da equação de estado sejam acrescentadas ao modelo a ser verificado, o que permite a obtenção de ganhos de desempenho na verificacao. O segundo estudo de caso e resolvido a partir da utilizacao de um procedimento proposto nesta dissertacao. Este procedimento permite a verificacao de algumas propriedades de seguranca sem que a verificacao se inviabilize devido a explosao no numero de estados. A utilizacao deste procedimento permite a verificacao de propriedades de uma secao de intertravamento com cerca de 2000 variaveis digitais em questao de poucos segundos.A principal conclusao a que este trabalho chega e consequencia dos resultados positivos observados nos estudos de caso: o model checking simbólico parece possuir um amplo campo de aplicacoes ainda por ser mais bem explorado / This work is the result of the efforts oriented to the study of the main automatic verification techniques for systems that can be modeled as Finite State Machines, in particular of those techniques which are generally called as model checking. In order to make the reader able to understand the pros and cons of each technique, the theory associated to each one is presented, as well as some examples. This work also presents two case studies of practical interest, both of each were solved with techniques which are called symbolic. The first one is the verification of some properties of a manufacturing system originally modeled by a Petri net. In order to improve the verification performance, it is proposed that the model to be verified be enlarged with the inclusion of the invariants calculated with the help of the state equation. The second case study is the verification of some safety properties of an interlocking system of a subway section. The verification is carried out with the help of a procedure which is proposed in this work. The aim of such a procedure is to bypass the state explosion problem, in order to make the verification feasible. It was possible to verify an interlocking system with about 2000 digital variables in a matter of few seconds. The main conclusion of the work comes from the positive results reached by both case studies: it seems to be a large number of applications yet to be explored in which symbolic model checking may be considered.

[pt] Em métodos formais, uma das abordagens que vem obtendo sucesso nos últimos anos é a de verificação formal. Dentro desta, vem se destacando uma técnica chamada de verificação de modelos (model checking), na qual se verifica automaticamente a validade de propriedades em sistemas acerca do funcionamento de um sistema. Atualmente, a verificação de modelos é muito empregada em informática na verficação formal de software e hardware, mas tem sido utilizada em outra áreas, como em matemática e em economia. Esta dissertação visa aplicar verificação de modelos a problemas de economia. O tema da pesquisa seria delimitado à Teoria dos Jogos. Algumas inadequações foram observadas, fazendo-se necessário algumas novas definições: uma definição de qualitativa que se utiliza de uma linguagem lógica denominada de Game Analysis Logic (GAL); uma linguagem para descrever jogo denominada de RollGame (Romero - All Game); uma tradução de RollGame na linguagem de especificação de modelos; uma tradução da definição de jogo em estrutura de Kripke. Observou-se ainda que com a utilização de model checking em jogos consegue- se analisar estratégias de jogadores. Uma ferramenta para automatizar a tradução de RollGame em model checking foi desenvolvida, chamada de StratAn-RollGame (Strategy Analyzed using RollGame). Assim, a presente dissertação demonstrou que de fato é possível utilizar verificação de modelos em outras areas. / [en] In formal methods, one of the approaches that have been successful lately is Model Checking, which consists in a technique to achieve automatic verification about a system behavior. Nowadays, the model checking is very frequently employed in computer science to formal verification of software and hardware, but it is not used in other knowledge fields, such as mathematics and economics. The purpose of this research is to apply model checking in economics problems, using Game Theory. Some inadequacies have been observed. Therefore, it is necessary to create new definitions: a generic and qualitative definition of game that uses one logic language called Game Analysis Logic (GAL); a new language to describe game called RollGame (Romero + All Game); a translation from RollGame to a language of model specification; a translation from game definition to Kripke structure. It is also been observed that the use of model checking makes it possible to analyze players strategies. One tool, called StratAn-RollGame (Strategy Analyzed using RollGame), makes the translation from RollGame to model Checking automatic. Thus, the present research has demonstrated that is possible indeed to use model checking in other knowledge fields.

Les logiciels sont devenus une partie importante de notre vie quotidienne, car ils sont maintenant utilisés dans de nombreux périphériques hétérogènes, tels que nos téléphones, nos voitures, nos appareils ménagers, etc. Ces périphériques sont parsemés d’un certain nombre de logiciels intégrés, chacun gérant une tâche spécifique. Ces logiciels intégrés sont conçus pour fonctionner à l’intérieur de systèmes plus vastes avec un matériel varié et hétérogène et des ressources limitées. L'utilisation de logiciels embarqués est motivée par la flexibilité et la simplicité que ces logiciels peuvent garantir, ainsi que par la réduction des coûts. Les Cyber-Physical System (CPS) sont des logiciels utilisés pour contrôler des systèmes physiques. Les CPS sont souvent intégrés et s'exécutent en temps réel, ce qui signifie qu'ils doivent réagir aux événements externes. Un CPS complexe peut contenir de nombreux systèmes en temps réel. Le fait que ces systèmes puissent être utilisés dans des domaines critiques tels que la médecine ou les transports exige un haut niveau de sécurité pour ces systèmes. Les systèmes temps réel (RTS), par définition, sont des systèmes informatiques de traitement qui doivent répondre à des entrées générées de manière externe. Ils sont appelés temps réel car leur réponse doit respecter des contraintes de temps strictes. Par conséquent, l'exactitude de ces systèmes ne dépend pas seulement de l'exactitude des résultats de leur traitement, mais également du moment auquel ces résultats sont donnés. Le principal problème lié à l'utilisation de systèmes temps réel est la difficulté de vérifier leurs contraintes de synchronisation. Un moyen de vérifier les contraintes de temps peut consister à utiliser la théorie de la planification, stratégie utilisée pour partager les ressources système entre ses différents composants. Outre les contraintes de temps, il convient de prendre en compte d'autres contraintes, telles que la consommation d'énergie ou la sécurité. Plusieurs méthodes de vérification ont été utilisées au cours des dernières années, mais avec la complexité croissante des logiciels embarqués, ces méthodes atteignent leurs limites. C'est pourquoi les chercheurs se concentrent maintenant sur la recherche de nouvelles méthodes et de nouveaux formalismes capables de vérifier l'exactitude des systèmes les plus complexes. Aujourd'hui, une classe de méthodes de vérification bien utilisées est les techniques basées sur des modèles. Ces techniques décrivent le comportement du système considéré à l'aide de formalismes mathématiques, puis, à l'aide de méthodes appropriées, permettent d'évaluer l'efficacité du système par rapport à un ensemble de propriétés. Dans ce manuscrit, nous nous concentrons sur l'utilisation de techniques basées sur des modèles pour développer de nouvelles techniques de planification afin d'analyser et de valider la satisfiabilité d'un certain nombre de propriétés sur des systèmes temps réel. L'idée principale est d'exploiter la théorie de l'ordonnancement pour proposer ces nouvelles techniques. Pour ce faire, nous proposons un certain nombre de nouveaux modèles afin de vérifier la satisfiabilité d'un certain nombre de propriétés telles que l'ordonnancement, la consommation d'énergie ou la fuite d'informations. / Software’s become an important part of our daily life as they are now used in many heterogeneous devices, such as our phones, our cars, our home appliances … etc. These devices are dotted with a number of embedded software’s, each handling a specific task. These embedded software’s are designed to run inside larger systems with various and heterogeneous hardware and limited resources. The use of embedded software is motivated by the flexibility and the simplicity that these software can guarantee, and to minimize the cost. Cyber-Physical System (CPS) are software used to control physical systems. CPS are often embedded and run in real-time, which means that they must react to external events. A complex CPS can contains many real-time systems. The fact that these systems can be used in critical domains like medicine or transport requires a high level of safety for these systems. Real-Time Systems (RTS) by definition are processing information systems that have to respond to externally generated inputs, and they are called real-time because their response must respect a strict timing constraints. Therefore, the correctness of these systems does not depend only on the correctness of their treatment results, but it also depends on the timings at which these results are given. The main problem with using real-time systems is the difficulty to verify their timing constraints. A way to verify timing constraints can be to use Scheduling theory which is a strategy used in order to share the system resources between its different components. In addition to the timing constraints, other constraints should be taken in consideration, like energy consumption or security. Several verification methods have been used in the last years, but with the increasing complexity of the embedded software these methods reach their limitation. That is why researchers are now focusing their works on finding new methods and formalisms capable of verifying the correctness of the most complex systems. Today, a well-used class of verification methods are model-based techniques. These techniques describe the behavior of the system under consideration using mathematical formalisms, then using appropriate methods they give the possibility to evaluate the correctness of the system with respect to a set of properties. In this manuscript we focus on using model-based techniques to develop new scheduling techniques in order to analyze and validate the satisfiability of a number of properties on real-time systems. The main idea is to exploit scheduling theory to propose these new techniques. To do that, we propose a number of new models in order to verify the satisfiability of a number of properties as schedulability, energy consumption or information leakage.