Embedded systems are used in many technical products of today. The tendency also points to the fact that they are in many ways becoming more and more complex as technology advances. Systems like advanced avionics, air bags, ABS brakes or any real-time embedded system requires reliability, correctness and timeliness. This puts hard pressure on designers, analyzers and developers. The need for high performance and non failing systems has therefore led to a growing interest in modeling and verification of component-based embedded systems in order to reduce costs and simplify design and development. The solution proposed by the Embedded Systems Lab at Linköping University is the modeling language PRES+, Petri Net based Representation for Embedded Systems. PRES+ models are then translated into timed automata, TA, which is used by the UPPAAL verification tool. To be able to verify timing properties the translated TA model must be instrumented with certain timers, called clocks. These clocks must be reset in a manner reflected by the property to be verified. This thesis will provide a solution to the problem and also give the reader necessary information in order to understand the theoretical background needed. The thesis will also show the reader the importance of modeling and time verification in the development of embedded systems. A simple example is used to describe and visualize the benefit regarding real-time embedded systems as well as the importance of the ability to verify these systems. The conclusion drawn stresses the fact that high development costs, possible gain of human lives and the problems in developing complex systems only emphasize the need for easy to handle and intuitive verification methods.

Abstract Due to increasing amount of concurrency, systems have become difficult to design and analyse. In this effort, formal verification, which means proving the correctness of a system, has turned out to be useful. Unfortunately, the application domain of the formal verification methods is often indefinite, tools are typically unavailable, and most of the techniques do not suit especially well for the verification of software systems. These are the questions addressed in the thesis. A typical approach to modelling systems and specifications is to consider them parameterised by the restrictions of the execution environment, which results in an (infinite) family of finite-state verification tasks. The thesis introduces a novel approach to the verification of such infinite specification-system families represented as labelled transition systems (LTSs). The key idea is to exploit the algebraic properties of the correctness relation. They allow the correctness of large system instances to be derived from that of smaller ones and, in the best case, an infinite family of finite-state verification tasks to be reduced to a finite one, which can then be solved using existing tools. The main contribution of the thesis is an algorithm that automates the reduction method. A specification and a system are given as parameterised LTSs and the allowed parameter values are encoded using first order logic. Parameters are sets and relations over these sets, which are typically used to denote, respectively, identities of replicated components and relationships between them. Because the number of parameters is not limited and they can be nested as well, one can express multiply parameterised systems with a parameterised substructure, which is an essential property from the viewpoint of modelling software systems. The algorithm terminates on all inputs, so its application domain is explicit in this sense. Other proposed parameterised verification methods do not have both these features. Moreover, some of the earlier results on the verification of parameterised systems are obtained as a special case of the results presented here. Finally, several natural and significant extensions to the formalism are considered, and it is shown that the problem becomes undecidable in each of the cases. Therefore, the algorithm cannot be significantly extended in any direction without simultaneously restricting some other aspect.

Dans cette thèse nous nous intéressons au problème d’analyse des spécifications des protocoles d’interactions des services Web orientés données. La spécification de ce type de protocoles inclut les données en plus de la signature des opérations et des contraintes d’ordonnancement des messages. L’analyse des services orientés données est complexe car l’exécution d’un service engendre une infinité d’états. Notre travail se concentre autour du problème d’existence d’une relation de simulation quand les spécifications des protocoles des services Web sont représentés en utilisant un système à transition orienté données. D’abord nous avons étudié le modèle Colombo [BCG+05]. Dans ce modèle, un service (i) échange des messages en utilisant des variables ; (ii) modifie une base de donnée partagée ; (iii) son comportement est modélisé avec un système à transition. Nous montrons que tester l’existence de la relation de simulation entre deux services Colombo non bornée est indécidable. Puis, nous considérons le cas où les services sont bornés. Nous montrons pour ce cas que le test de simulation est (i) exptime-complet pour les services Colombo qui n’accèdent pas à la base de donnée (noté ColomboDB=∅), et (ii) 2exptime-complet quand le service peut accéder à une base de donnée bornée (Colombobound). Dans la seconde partie de cette thèse, nous avons défini un modèle générique pour étudier l’impact de différents paramètres sur le test de simulation dans le contexte des services Web orientés données. Le modèle générique est un système à transition gardé qui peut lire et écrire à partir d’une base de donnée et échanger des messages avec son environnement (d’autres services ou un client). Dans le modèle générique toutes les actions sont des requêtes sur des bases de données (modification de la base de données, messages échangés et aussi les gardes). Dans ce contexte, nous avons obtenu les résultats suivant : (i) pour les services gardés sans mise à jour, le test de simulation est caractérisé par rapport à la décidabilité du test de satisfiabilité du langage utilisé pour exprimer les gardes augmenté avec une forme restrictive de négation, (ii) pour les services sans mise à jour mais qui peuvent envoyer comme message le résultat d’une requête, nous avons trouvé des conditions suffisantes d’indécidabilité et de décidabilité par rapport au langage utilisé pour exprimer l’échange de messages, et (iii) nous avons étudié le cas des services qui ne peuvent que insérer des tuples dans la base de donnée. Pour ce cas, nous avons étudié la simulation ainsi que la weak simulation et nous avons montré que : (a) la weak simulation est indécidable quand les requêtes d’insertion sont des requêtes conjonctives, (b) le test de simulation est indécidable si la satisfiabilité du langage de requête utilisé pour exprimer les insertions augmenté avec une certaine forme de négation est indécidable. Enfin, nous avons étudié l’interaction entre le langage utilisé pour exprimer les gardes et celui utilisé pour les insertions, nous exhibons une classe de service où la satisfiabilité des deux langages est décidable alors que le test de simulation entre les services qui leur sont associés ne l’est pas. / In this thesis we address the problem of analyzing specifications of data-centric Web service interaction protocols (also called data-centric business protocols). Specifications of such protocols include data in addition to operation signatures and messages ordering constraints. Analysis of data-centric services is a complex task because of the inherently infinite states of the underlying service execution instances. Our work focuses on characterizing the problem of checking a refinement relation between service interaction protocol specifications. More specifically, we consider the problem of checking the simulation preorder when service business protocols are represented using data-centric state machines. First we study the Colombo model [BCG+05]. In this framework, a service (i) exchanges messages using variables; (ii) acts on a shared database; (iii) has a transition based behavior. We show that the simulation test for unbounded Colombo is undecidable. Then, we consider the case of bounded Colombo where we show that simulation is (i) exptime-complete for Colombo services without any access to the database (noted ColomboDB=∅), and (ii) 2exptime-complete when only bounded databases are considered (the obtained model is noted Colombobound). In the second part of this thesis, we define a generic model to study the impact of various parameters on the simulation test in the context of datacentric services. The generic model is a guarded transition system acting (i.e., read and write) on databases (i.e., local and shared) and exchanging messages with its environment (i.e., other services or users). The model was designed with a database theory perspective, where all actions are viewed as queries (i.e modification of databases, messages exchanges and guards). In this context, we obtain the following results (i) for update free guarded services (i.e., generic services with guards and only able to send empty messages) the decidability of simulation is fully characterized w.r.t decidability of satisfiability of the query language used to express the guards augmented with a restrictive form of negation, (ii) for update free send services (i.e., generic services without guards and able to send as messages the result of queries over local and shared database), we exhibit sufficient conditions for both decidability and undecidability of simulation test w.r.t the language used to compute messages payloads, and (iii) we study the case of insert services (i.e., generic services without guards and with the ability of insert the result of queries into the local and the shared database). In this case, we study the simulation as well as the weak simulation relations where we show that: (i) the weak simulation is undecidable when the insertions are expressed as conjunctive queries, (ii) the simulation is undecidable if satisfiability of the query language used to express the insertion augmented with a restricted form of negation is undecidable. Finally, we study the interaction between the queries used as guards and the ones used as insert where we exhibit a class of services where satisfiability of both languages is decidable while simulation is undecidable.

Cette thèse appartient au domaine des méthodes formelles. Nous nous concentrons sur leur application à une méthodologie spécifique pour le développement de logiciels: l'ingénierie à base de composants. Le Grid Component Model (GCM) suit cette méthodologie en fournissant tous les moyens pour définir, composer, et dynamiquement reconfigurer les applications distribuées à base de composants. Dans cette thèse, nous abordons la spécification formelle, la vérification et le déploiement d'applications GCM reconfigurables et distribuées. Notre première contribution est un cas d'étude industriel sur la spécification comportementale et la vérification d'une application distribuée et reconfigurable: L'HyperManager. Notre deuxième contribution est une plate-forme, élaborée avec l'assistant de preuve Coq, pour le raisonnement sur les architectures logicielles: Mefresa. Cela comprend la mécanisation de la spécification du GCM, et les moyens pour raisonner sur les architectures reconfigurables GCM. En outre, nous adressons les aspects comportementaux en formalisant une sémantique basée sur les traces d'exécution de systèmes de transitions synchronisées. Enfin, notre troisième contribution est un nouveau langage de description d'architecture (ADL): Painless. En outre, nous discutons son intégration avec ProActive, un intergiciel Java pour la programmation concurrente et distribuée, et l'implantation de référence du GCM. / This thesis belongs to the domain of formal methods. We focus their application on a specific methodology for the development of software: component-based engineering.The Grid Component Model (GCM) endorses this approach by providing all the means to define, compose and dynamically reconfigure component-based distributed applications. In this thesis we address the formal specification, verification and deployment of distributed and reconfigurable GCM applications. Our first contribution is an industrial case study on the behavioural specification and verification of a reconfigurable distributed application: The HyperManager. Our second contribution is a framework, developed with the Coq proof assistant, for reasoning on software architectures: Mefresa. This encompasses the mechanization of the GCM specification, and the means to reason about reconfigurable GCM architectures. Further, we address behavioural concerns by formalizing a semantics based on execution traces of synchronized transition systems. Overall, it provides the first steps towards a complete specification and verification platform addressing both architectural and behavioural properties. Finally, our third contribution is a new Architecture Description Language (ADL), denominated Painless. Further, we discuss its proof-of-concept integration with ProActive, a Java middleware for concurrent and distributed programming, and the de facto reference implementation of the GCM.

Le développement des réseaux de communication digitaux tel Internet a rendu omniprésents les protocoles de communication. Les différents appareils électroniques que nous utilisons au quotidien doivent interagir les uns avec les autres afin de réaliser les taches nombreuses et variées qui sont devenues courantes, comme d'utiliser d'un téléphone portable, envoyer ou recevoir des messages électroniques, faire des achats en ligne et ainsi de suite. Pour ces applications, la sécurité est une notion cruciale. Par exemple, dans le cas des achats en ligne, il faut que la transaction ait lieu sans divulguer les informations personnelles de l'acheteur à un tiers. Les protocoles de communications contiennent les règles qui régissent ces interactions. Afin de s'assurer qu'ils garantissent un certain niveau de sécurité, on souhaite pouvoir les analyser. Une analyse manuelle, ou leur faire subir des tests, n'est pas suffisant, les attaques pouvant se révéler subtiles. Certains protocols ont été utilisés pendant des années avant qu'une attaque soit découverte contre eux. Étant donnée leur ubiquité croissante dans de nombreuses applications importantes, comme le commerce électronique, un des défis importants auquel la recherche doit faire face consiste à développer des méthodes et des outils de vérification pour augmenter notre confiance dans les protocoles sécurisés, et dans les applications qui dépendent de ces protocoles. Par exemple, plus de 28 milliards d'euros sont dépensés en France au cours de transactions sur Internet, et cette quantité ne cesse d'augmenter. De plus, de nouveaux types de protocoles apparaissent continuellement afin de relever de nouveaux défis technologiques et de société, e.g. le vote électronique, le passeport numérique pour n'en citer que quelques-uns. / With the development of digital networks, such as Internet, communication protocols are omnipresent. Digital devices have to interact with each other in order to perform the numerous and complex tasks we have come to expect as commonplace, such as using a mobile phone, sending or receiving electronic mail, making purchases online and so on. In such applications, security is important. For instance, in the case of an online purchase, the right amount of money has to be paid without leaking the buyer personal information to outside parties. Communication protocols are the rules that govern these interactions. In order to make sure that they guarantee a certainlevel of security, it is desirable to analyze them. Doing so manually or by testing them is not enough, as attacks can be quite subtle. Some protocols have been used for years before an attack was discovered. Because of their increasing ubiquity in many important applications, e.g. electronic commerce, a very important research challenge consists in developing methods and verification tools to increase our trust on security protocols, and so on the applications that rely on them. For example, more than 28 billion Euros were spent in France using Internet transactions, and the number is growing. Moreover, new types of protocols are continuously appearing in order to face new technological and societal challenges, e.g. electronic voting, electronic passport to name a few.

Cette thèse développe des outils permettant de prouver qu’un système dynamique est sûr. En supposant qu’une partie de l’espace d’état est dangereuse, un système dynamique est dit sûr lorsque son état n’atteint jamais cette partie dangereuse au cours du temps, quel que soit l’état initial appartenant à un ensemble d’états initiaux admissibles et quel que soit le niveau de perturbation restant dans un domaine admissible. Les outils proposés cherchent à établir des preuves de sûreté pour des systèmes décrits par des modèles dynamiques non-linéaires et des modèles dynamiques hybrides. Prouver qu’un système dynamique est sûr en calculant explicitement l’ensemble des trajectoires possibles du système lorsque le modèle dynamique est non-linéaire et perturbé reste une tâche très difficile. C’est pourquoi cette thèse aborde ce problème à l’aide de fonctions barrières paramétrées. Une barrière, lorsqu’elle existe, permet de partitionner l’espace d’état et d’isoler l’ensemble des trajectoires possibles de l’état du système de la partie dangereuse de l’espace d’état. La fonction paramétrique décrivant la barrière doit satisfaire un certain nombre de contraintes impliquant la dynamique du modèle, l’ensemble des états initiaux possibles, et l’ensemble dangereux. Ces contraintes ne sont pas convexes en général, ce qui complique la recherche de fonctions barrières satisfaisantes. Précédemment, seules des fonctions barrières polynomiales ont été considérées pour des modèles dynamiques polynomiaux. Cette thèse considère des systèmes dynamiques relativement généraux avec des barrières paramétriques quelconques. Les solutions présentées exploitent des outils de satisfaction de contraintes sur des domaines continus et des outils issus de l’analyse par intervalles. Dans un premier temps, cette thèse considère des systèmes dynamiques non-linéaires à temps continu. Le problème de conception d’une barrière paramétrique est formulé comme un problème de satisfaction des contraintes sur des domaines réels avec des variables quantifiées de manière existentielle et universelle. L’algorithme CSC-FPS a été adapté afin de résoudre le problème de synthèse de barrière. Cet algorithme combine une exploration de l’espace des paramètres de la barrière et une phase de vérification des propriétés de la barrière. A l’aide de contracteurs, il est possible de significativement accélérer la recherche de solutions. Dans un second temps, ces résultats sont étendus au cas de systèmes décrits par des modèles dynamiques hybrides. La propriété de sûreté doit être prouvée lors de l’évolution à temps continu du système dynamique, mais aussi pendant les transitions du système. Ceci nécessite l’introduction de contraintes supplémentaires qui lient les fonctions barrières associées à chaque mode à temps continu entre elles. Réaliser la synthèse de toutes les fonctions barrières pour les différents modes simultanément n’est envisageable que pour des systèmes de très petite dimension avec peu de modes. Une approche séquentielle a été proposée. Les contraintes liées aux transitions sont introduites progressivement entre les modes pour lesquels une barrière a déjà été obtenue. Lorsque certaines contraintes de transition ne sont pas satisfaites, une méthode de backtracking doit être mise en œuvre afin de synthétiser des barrières offrant une meilleure prise en compte des contraintes de transition non satisfaites. Ces approches ont été évaluées et comparées avec des techniques de l’état de l’art sur des systèmes décrits par des modèles à temps continu et des modèles hybrides. / This thesis addresses the problem of proving the safety of systems described by non-linear dynamical models and hybrid dynamical models. A system is said to be safe if all trajectories of its state do not reach an unsafe region. Proving the safety of systems by explicitly computing all its trajectories when its dynamic is non-linear or when its behavior is described by an hybrid model with non-linear dynamics remains a challenging task. This thesis considers the barrier function approach to prove the safety of a system. A barrier function, when it exists, partitions the state space and isolates the trajectories of the system starting from any possible initial values of the state and the unsafe part of the state space. The set of constraints, which have to be satisfied by a barrier function are usually non-convex, rendering the search of satisfying barrier functions hard. Previously, only polynomial barrier functions were taken in consideration and for systems with polynomial dynamics. This thesis considers relatively general dynamical systems with generic non-linear barrier functions. The solutions presented are based on template barrier functions, constraint satisfaction problems, and interval analysis. The first part of the thesis focuses on non-linear dynamical systems. The barrier function design problem is formulated as a constraint satisfaction problem that can be solved using tools from interval analysis. This formulation allows one to prove the safety of a non-linear dynamical system by finding the parameters of a template barrier function such that all constraints are satisfied using the FPS-CSC algorithm, which has been adapted and supplemented with contractors to improve its efficiency. The second part of the thesis is dedicated to the design of barrier functions for systems described by hybrid dynamical models. Safety properties have to be proven during the continuous-time evolution of the system, but also during transitions. This leads to additional constraints that have to be satisfied by candidate barrier functions. Solving all the constraints simultaneously to find all the barrier functions is usually computationally intractable. In the proposed approach, the algorithm explores all the locations sequentially. Transition constraints are introduced progressively between the already explored locations. Backtracking to previous location is considered when transition constraints are not satisfied. The efficiency of the proposed approaches has been compared with state-of-the-art solutions.

Hardware design verification is the most challenging part in overall hardware design process. It is because design size and complexity are growing very fast while the requirement for performance is ever higher. Conventional simulation-based verification method cannot keep up with the rapid increase in the design size, since it is impossible to exhaustively test all input vectors of a complex design. An important part of hardware verification is combinational arithmetic circuit verification. It draws a lot of attention because flattening the design into bit-level, known as the bit-blasting problem, hinders the efficiency of many current formal techniques. The goal of this thesis is to introduce a robust and efficient formal verification method for combinational integer arithmetic circuit based on an in-depth analysis of recent advances in computer algebra. The method proposed here solves the verification problem at bit level, while avoiding bit-blasting problem. It also avoids the expensive Groebner basis computation, typically employed by symbolic computer algebra methods. The proposed method verifies the gate-level implementation of the design by representing the design components (logic gates and arithmetic modules) by polynomials in Z2n . It then transforms the polynomial representing the output bits (called “output signature”) into a unique polynomial in input signals (called “input signature”) using gate-level information of the design. The computed input signature is then compared with the reference input signature (golden model) to determine whether the circuit behaves as anticipated. If the reference input signature is not given, our method can be used to compute (or extract) the arithmetic function of the design by computing its input signature. Additional tools, based on canonical word-level design representations (such as TED or BMD) can be used to determine the function of the computed input signature represents. We demonstrate the applicability of the proposed method to arithmetic circuit verification on a large number of designs.

Finite tree automata is formalism used in many different areas of computer science, among others in the area of formal verification. Nowdays there are few tools used for handling of finite tree automata, however libraries of MONA tool are the best choice. The finite tree automata are a frequent tool for formal verification of computer systems which work with dynamic data structures. The input format of finite tree automata for libraries of MONA tool is very difficult for humans because it is necessary to enter the move function of the finite tree automaton in a form of several multiterminal binary decision diagrams. The aim of this thesis is to design and implement tool to convert the finite set of move rules into internal format of the MONA tool.

Pre-Charge Half Buffers (PCHB) and NULL convention Logic (NCL) are two major commercially successful Quasi-Delay Insensitive (QDI) asynchronous paradigms, which are known for their low-power performance and inherent robustness. In industry, QDI circuits are synthesized from their synchronous counterparts using custom synthesis tools. Validation of the synthesized QDI implementation is a critical design prerequisite before fabrication. At present, validation schemes are mostly extensive simulation based that are good enough to detect shallow bugs, but may fail to detect corner-case bugs. Hence, development of formal verification methods for QDI circuits have been long desired. The very few formal verification methods that exist in the related field have major limiting factors. This dissertation presents different formal verification methodologies applicable to PCHB and NCL circuits, and aims at addressing the limitations of previous verification approaches. The developed methodologies can guarantee both safety (full functional correctness) and liveness (absence of deadlock), and are demonstrated using several increasingly larger sequential and combinational PCHB and NCL circuits, along with various ISCAS benchmarks. / National Science Foundation (Grant No. CCF-1717420)

Real-time systems such as medical devices, surgical robots, and microprocessors are safety- critical applications that have hard timing constraint. The correctness of real-time systems is important as the failure may result in severe consequences such as loss of money, time and human life. These real-time systems have software to control their behavior. Typically, these software have source code which is converted to object code and then executed in safety-critical embedded devices. Therefore, it is important to ensure that both source code and object code are error-free. When dealing with safety-critical systems, formal verification techniques have laid the foundation for ensuring software correctness. Refinement based technique in formal verification can be used for the verification of real- time interrupt-driven object code. This dissertation presents an automated tool that verifies the functional and timing correctness of real-time interrupt-driven object code programs. The tool has been developed in three stages. In the first stage, a novel timed refinement procedure that checks for timing properties has been developed and applied on six case studies. The required model and an abstraction technique were generated manually. The results indicate that the proposed abstraction technique reduces the size of the implementation model by at least four orders of magnitude. In the second stage, the proposed abstraction technique has been automated. This technique has been applied to thirty different case studies. The results indicate that the automated abstraction technique can easily reduce the model size, which would in turn significantly reduce the verification time. In the final stage, two new automated algorithms are proposed which would check the functional properties through safety and liveness. These algorithms were applied to the same thirty case studies. The results indicate that the functional verification can be performed in less than a second for the reduced model. The benefits of automating the verification process for real-time interrupt-driven object code include: 1) the overall size of the implementation model has reduced significantly; 2) the verification is within a reasonable time; 3) can be applied multiple times in the system development process. / Several parts of this dissertation was funded by a grant from the United States Government and the generous support of the American people through the United States Department of State and the United States Agency for International Development (USAID) under the Pakistan – U.S. Science & Technology Cooperation Program. The contents do not necessarily reflect the views of the United States Government.