Software defects can frequently be traced to poorly-specified requirements. Many software teams manage their requirements using tools such as checklists and databases, which lack a formal semantic mapping to system behavior. Such a mapping can be especially helpful for safety-critical systems. Another limitation of many requirements analysis methods is that much of the analysis must still be done manually. We propose techniques that automate portions of the requirements analysis process, as well as clarify the syntax and semantics of requirements models using a variety of methods, including machine learning tools and our own tool, VeriCCM. The machine learning tools used help us identify potential model elements and verify their correctness. VeriCCM, a formalized extension of the causal component model (CCM), uses formal methods to ensure that requirements are well-formed, as well as providing the beginnings of a full formal semantics. We also explore the use of statecharts to identify potential abnormal behaviors from a given set of requirements. At each stage, we perform empirical studies to evaluate the effectiveness of our proposed approaches.

No description available.

L'injection de faute est une méthode bien connue pour évaluer la robustesse et détecter les vulnérabilités des systèmes. La détection des vulnérabilités créées par injection de fautes a été approchée par différentes méthodes. Dans la littérature deux approches existent: les approches logicielles et les approches matérielles. Les approches logicielles peuvent fournir une large et rapide couverture, mais ne garantissent pas la présence de vulnérabilité dans le système. Les approches matérielles sont incontestables dans leurs résultats, mais nécessitent l’utilisation de matériaux assez coûteux et un savoir-faire approfondi, qui ne permet tout de même pas dans la majorité des cas de confirmer le modèle de faute représentant l'effet créé. Dans un premier lieu, cette thèse se concentre sur l'approche logicielle et propose une approche automatisée qui emploie les techniques de la vérification formelle pour détecter des vulnérabilités créées par injection de faute au niveau binaire. L'efficacité de cette approche est montrée en l'appliquant à des algorithmes de cryptographie implémentés dans les systèmes embarqués. Dans un second lieu, cette thèse établit un rapprochement entre les deux approches logicielles et matérielles sur la détection de vulnérabilité d'injection de faute en comparant les résultats des expériences des deux approches. Ce rapprochement des deux approches démontre que: toutes les vulnérabilités détectées par l'approche logicielle ne peuvent pas être reproduites dans le matériel; les conjectures antérieures sur le modèle de faute par des attaques d'impulsion électromagnétique ne sont pas précises ; et qu’il y a un lien entre les résultats de l’approche logicielle et l'approche matérielle. De plus, la combinaison des deux approches peut rapporter une approche plus précise et plus efficace pour détecter les vulnérabilités qui peuvent être créées par injection de faute. / Fault injection is a well known method to test the robustness and security vulnerabilities of systems. Detecting fault injection vulnerabilities has been approached with a variety of different but limited methods. Software-based and hardware-based approaches have both been used to detect fault injection vulnerabilities. Software-based approaches can provide broad and rapid coverage, but may not correlate with genuine hardware vulnerabilities. Hardware-based approaches are indisputable in their results, but rely upon expensive expert knowledge, manual testing, and can not confirm what fault model represent the created effect. First, this thesis focuses on the software-based approach and proposes a general process that uses model checking to detect fault injection vulnerabilities in binaries. The efficacy and scalability of this process is demonstrated by detecting vulnerabilities in different cryptographic real-world implementations. Then, this thesis bridges software-based and hardware-based fault injection vulnerability detection by contrasting results of the two approaches. This demonstrates that: not all software-based vulnerabilities can be reproduced in hardware; prior conjectures on the fault model for electromagnetic pulse attacks may not be accurate; and that there is a relationship between software-based and hardware-based approaches. Further, combining both software-based and hardware-based approaches can yield a vastly more accurate and efficient approach to detect genuine fault injection vulnerabilities.

The popular model checker PRISM has been successfully used for the modeling and analysis of complex probabilistic systems. As one way to tackle the challenging state explosion problem, PRISM supports symbolic storage and manipulation using multi-terminal binary decision diagrams for representing the models and in the computations. However, it lacks automated heuristics for variable reordering, even though it is well known that the order of BDD variables plays a crucial role for compact representations and efficient computations. In this article, we present a collection of extensions to PRISM. First, we provide support for automatic variable reordering within the symbolic engines of PRISM and allow users to manually control the variable ordering at a fine-grained level. Second, we provide extensions in the realm of reward-bounded properties, namely symbolic computations of quantiles in Markov decision processes and, for both the explicit and symbolic engines, the approximative computation of quantiles for continuous-time Markov chains as well as support for multi-reward-bounded properties. Finally, we provide an implementation for obtaining minimal weak deterministic Büchi automata for the obligation fragment of linear temporal logic (LTL), with applications for expected accumulated reward computations with a finite horizon given by a co-safe LTL formula.

For modeling and reasoning about complex systems, symbolic methods provide a prominent way to tackle the state explosion problem. It is well known that for symbolic approaches based on binary decision diagrams (BDD), the ordering of BDD variables plays a crucial role for compact representations and efficient computations. We have extended the popular probabilistic model checker PRISM with support for automatic variable reordering in its multi-terminal-BDD-based engines and report on benchmark results. Our extensions additionally allow the user to manually control the variable ordering at a finer-grained level. Furthermore, we present our implementation of the symbolic computation of quantiles and support for multi-reward-bounded properties, automata specifications and accepting end component computations for Streett conditions.

Reactive systems are computer systems that maintain continuous interaction with the environment in which they operate. Such systems are nowadays part of our daily life: think about common yet critical applications like engine control units in automotive, aircraft autopilots, medical aided- devices, or micro-controllers in mass production. Clearly, any flaw in such critical systems can have catastrophic consequences. However, they exhibit several characteristics, like resource limitation constraints, real-time responsiveness, concurrency that make them difficult to implement correctly. To ensure the design of reactive systems that are dependable, safe, and efficient, researchers and industrials have advocated the use of so-called formal methods, that rely on mathematical models to express precisely and analyze the behaviors of these systems.Automata theory provides a fundamental notion such as languages of program executions for which membership, emptiness, inclusion, and equivalence problems allow us to specify and verify properties of reactive systems. However, these Boolean notions yield the correctness of the system against a given property that sometimes, falls short of being satisfactory answers when the performances are prone to errors. As a consequence, a common engineering approach is not just to verify that a system satisfies a property, but whether it does so within a degree of quality and robustness.This thesis investigates the expressibility, recognition, and robustness of quantitative properties for program executions.• Firstly, we provide a survey on languages definable by regular automata with Presburger definable constraints on letter occurrences for which we provide descriptive complexity. Inspired by this model, we introduce an expression formalism that mixes formula and automata to define quantitative languages \ie function from words to integers. These expressions use Presburger arithmetic to combine values given by regular automata weighted by integers. We show that quantitative versions of the classical decision problems such as emptiness, universality, inclusion, and equivalence are computable. Then we investigate the extension of our expressions with a ''Kleene star'' style operator. This allows us to iterate an expression over smaller fragments of the input word, and to combine the results by taking their iterated sum. The decision problems quickly turn out to be not computable, but we introduce a new subclass based on a structural restriction for which algorithmic procedures exist.• Secondly, we consider a notion of robustness that places a distance on words, thus defining neighborhoods of program executions. A language is said to be robust if the membership satisfiability cannot differ for two ''close'' words, and that leads to robust versions of all the classical decision problems. Our contribution is to study robustness verification problems in the context of weighted transducers with different measures (sum, mean-payoff, and discounted sum). Here, the value associated by the transducer to rewrite a word into another denotes the cost of the noise that this rewriting induce. For each measure, we provide algorithms that determine whether a language is robust up to a given threshold of error and we solve the synthesis of the robust kernel for the sum measure. Furthermore, we provide case studies including modeling human control failures and approximate recognition of type-1 diabetes using robust detection of blood sugar level swings.• Finally, we observe that algorithms for structural patterns recognition of automata often share similar techniques. So, we introduce a generic logic to express structural properties of automata with outputs in some monoid, in particular, the set of predicates talking about the output values is parametric. Then, we consider three particular automata models (regular automata, transducers, and automata weighted by integers) and instantiate the generic logic for each of them. We give tight complexity results for the three logics with respect to the pattern recognition problem. We study the expressiveness of our logics by expressing classical structural patterns characterizing for instance unambiguity and polynomial ambiguity in the case of regular automata, determinizability, and finite-valuedness in the case of transducers and automata weighted by integers. As a consequence of our complexity results, we directly obtain that these classical properties can be decided in logarithmic space. / Doctorat en Sciences / info:eu-repo/semantics/nonPublished

Over the last decades, autonomous robots have been considered in a variety of applications such  as persistent monitoring, package delivery and cooperative transportation. These applications often require the satisfaction of a set of complex tasks that need to be possibly performed in a timely manner. For example, in search and rescue missions, UAVs are expected to cover a set of regions within predetermined time intervals in order to increase the probability of identifying the victims of an accident. Spatio-temporal tasks of this form can be easily expressed in Signal Temporal Logic (STL), a predicate language that allow us to formally introduce time-constrained tasks such as visit area A between 0 and 5 min or robot 1 should move in a formation with robot 2 until robot 1 reaches region B between 5 and 20 sec. Existing approaches in control under spatio-temporal tasks encode the STL constraints using mixed-integer expressions. In the majority of these works, receding horizon schemes are designed and long planning horizons are considered that depend on the temporal constraints of the STL tasks. As a result, the complexity of these problems may increase with the number of the tasks or the length of the time interval within which a STL task needs to be satisfied. Other approaches, consider a limited STL fragment and propose computationally efficient feedback controllers that ensure the satisfaction of the STL task with a minimum, desired robustness. Nevertheless, these approaches do not consider actuation limitations that are always present in real-world systems and thus, yield controllers of arbitrarily large magnitude.  In this thesis, we consider the control problem under spatio-temporal constraints for systems that are subject to actuation limitations. In the first part, receding horizon control schemes (RHS) are proposed that ensure the satisfaction or minimal violation of a given set of STL tasks. Contrary to existing approaches, the planning horizon of the RHS scheme can be chosen independent of the STL task and hence, arbitrarily small, given the initial feasibility of the problem. Combining the advantages of the RHS and feedback strategies, we encode the STL tasks using control barrier functions that are designed either online or offline and design controllers that aim at maximizing the robustness of the STL task. The recursive feasibility property of the framework is established and a lower bound on the violation of the STL formula is derived. In the next part, we consider a multi-agent system that is subject to a STL task whose satisfaction may involve a large number of agents in the team. Then, the goal is to decompose the global task into local ones the satisfaction of each one of which  depends only on a given sub-team of agents. The proposed decomposition method enables the design of decentralized controllers under local STL tasks avoiding unnecessary communication among agents.  In the last part of the thesis, the coordination problem of multiple platoons is considered and related tasks such as splitting, merging and distance maintenance are expressed as Signal Temporal Logic tasks. Then, feedback control techniques are employed ensuring the satisfaction the STL formula, or alternatively minimal violation in presence of actuation limitations. / De senaste ̊artiondena har autonoma robotar sett en rad nya användningsområden, såsom ̈overvakning, paketleverans och kooperativ transport. Dessa innebär ofta att en samling komplexa uppgifter måste lösas på kort tid. Inom Search and Rescue (SAR), till exempel, krävs att drönare hinner genomsöka vissa geografiska regioner inom givna tidsintervall. Detta för att ̈oka chansen att identifierade drabbade vid en olycka. Den här typen av uppgift i tid och rum (spatio-temporal) kan enkelt uttryckas med hjälp av Signal Temporal Logic (STL). STL ̈är ett språk som tillåter oss att på ett formellt sätt formulera tidsbegränsade uppgifter, såsom besök område A mellan o och 5 minuter, eller robot 1 ska röra sig i formationtillsammans med robot 2 till dess att robot 1 når område B mellan 5 och 20 sekunder. Nuvarande lösningar till styrproblem av spatio-temporal-typen kodar STL-begränsningar med hjälp av mixed-integer-uttryck. Majoriteten av lösningarna involverar receding-horizon-metoder med långa tidshorisonter som beror av tidsbegränsningarna i STL-uppgifterna. Detta leder till att problemens komplexitet ̈ökar med antalet deluppgifter inom och tiden för STL-uppgifterna. Andra lösningar bygger på restriktiva STL-fragment och beräkningsmässigt effektiva ̊aterkopplingsregulatorer som garanterar STL-begränsningarna med minimal önskad robusthet. Dessvärre tar dessa sällan hänsyn till fysiska begräsningar hos regulatorn och ger ofta godtyckligt stora styrsignaler. I den här licentiatuppsatsen behandlar vi styrproblem med begräsningar i rum och tid, samt den ovan nämnda typen av fysiska regulatorbegränsningar. I den första delen presenterar vi receding-horizon-metoder (RHS) som uppfyller kraven i STL-uppgifter, eller minimalt bryter mot dessa. Till skillnad från tidigare lösningar så kan tidshorisonten i våra RHS-metoder väljas oberoende av STL-uppgifterna och därmed göras godtyckligt kort, så länge ursprungsproblemet ̈ar lösbart. Genom att formulera STL-uppgifterna som control barrier funktioner kan vi kombinera fördelarna hos RHS och ̊återkoppling. Vi härleder en rekursiv lösbarhetsegenskap och en undre gräns på ̈overträdelsen av STL-kraven. I den andra delen behandlar vi multi-agent-system med uppgifter i tid och rum som berör många agenter. Målet är att bryta ner den globala uppgiften i fler men enklare lokala uppgifter som var och en bara involverar en given delmängd av agenterna. Vår nedbrytning till ̊åter oss att konstruera decentraliserade regulatorer som löser lokala STL-uppgifter, och kan i och med det markant minska kommunikationskostnaderna i j̈ämförelse med centraliserad styrning. I den sista delen av uppsatsen behandlar vi samordning av flera grupper. Vi uttrycker uppgifter såsom delning, sammanslagning och avståndshållning med hjälp av STL, och utnyttjar sedan ̊aterkoppling för att uppfylla eller minimalt bryta mot kraven. / <p>QC 20220311</p>

No description available.

Type checking is widely used in mainstream programming languages to detect programming errors at compile time. Model checking is gaining popularity as an automated technique for systematically analyzing behaviors of systems. My research focuses on combining these two software verification techniques synergically into one platform for the creation of correct models for software designs. This thesis describes two modeling languages ATS/PML and ATS/Veri that inherit the advanced type system from an existing programming language ATS, in which both dependent types of Dependent ML style and linear types are supported. A detailed discussion is given for the usage of advanced types to detect modeling errors at the stage of model construction. Going further, various modeling primitives with well-designed types are introduced into my modeling languages to facilitate a synergic combination of type checking with model checking. The semantics of ATS/PML is designed to be directly rooted in a well-known modeling language PROMELA. Rules for translation from ATS/PML to PROMELA are designed and a compiler is developed accordingly so that the SPIN model checker can be readily employed to perform checking on models constructed in ATS/PML. ATS/Veri is designed to be a modeling language, which allows a programmer to construct models for real-world multi-threaded software applications in the same way as writing a functional program with support for synchronization, communication, and scheduling among threads. Semantics of ATS/Veri is formally defined for the development of corresponding model checkers and a compiler is built to translate ATS/Veri into CSP# and exploit the state-of-the-art verification platform PAT for model checking ATS/Veri models. The correctness of such a transformational approach is illustrated based on the semantics of ATS/Veri and CSP#. In summary, the primary contribution of this thesis lies in the creation of a family of modeling languages with highly expressive types for modeling concurrent software systems as well as the related platform supporting verification via model checking. As such, we can combine type checking and model checking synergically to ensure software correctness with high confidence.

Les implémentations cryptographiques sont vulnérables aux attaques physiques, et ont donc besoin d'en être protégées. Bien sûr, des protections défectueuses sont inutiles. L'utilisation des méthodes formelles permet de développer des systèmes tout en garantissant leur conformité à des spécifications données. Le premier objectif de ma thèse, et son aspect novateur, est de montrer que les méthodes formelles peuvent être utilisées pour prouver non seulement les principes des contre-mesures dans le cadre d'un modèle, mais aussi leurs implémentations, étant donné que c'est là que les vulnérabilités physiques sont exploitées. Mon second objectif est la preuve et l'automatisation des techniques de protection elles-même, car l'écriture manuelle de code est sujette à de nombreuses erreurs, particulièrement lorsqu'il s'agit de code de sécurité. / Implementations of cryptosystems are vulnerable to physical attacks, and thus need to be protected against them. Of course, malfunctioning protections are useless. Formal methods help to develop systems while assessing their conformity to a rigorous specification. The first goal of my thesis, and its innovative aspect, is to show that formal methods can be used to prove not only the principle of the countermeasures according to a model, but also their implementations, as it is where the physical vulnerabilities are exploited. My second goal is the proof and the automation of the protection techniques themselves, because handwritten security code is error-prone.