La criticité des programmes dépasse constamment de nouvelles frontières car ils sont de plus en plus utilisés dans la prise de décision (voitures autonomes, robots chirurgiens, etc.). Le besoin de développer des programmes sûrs et de vérifier les programmes existants émerge donc naturellement.Pour prouver formellement la correction d'un programme, il faut faire face aux défis de la mise à l'échelle et de la décidabilité. Programmes composés de millions de lignes de code, complexité de l'algorithme, concurrence, et même de simples expressions polynomiales font partis des problèmes que la vérification formelle doit savoir gérer. Pour y arriver, les méthodes formelles travaillent sur des abstractions des états des programmes étudiés afin d'analyser des approximations de leur comportement. L'analyse des boucles est un axe entier de la vérification formelle car elles sont encore aujourd'hui peu comprises. Bien que certaines d'entre elles peuvent facilement être traitées, il existe des exemples apparemment très simples mais dont le comportement n'a encore aujourd'hui pas été résolu (par exemple, on ne sait toujours pas pourquoi la suite de Syracuse, simple boucle linéaire, converge toujours vers 1).L'approche la plus commune pour gérer les boucles est l'utilisation d'invariants de boucle, c'est à dire de relations sur les variables manipulées par une boucle qui sont vraies à chaque fois que la boucle recommence. En général, les invariants utilisent les mêmes expressions que celles utilisées dans la boucle : si elle manipule explicitement la mémoire par exemple, on s'attend à utiliser des invariants portant sur la mémoire. Cependant, il existe des boucles contenant uniquement des affectations linéaires qui n'admettent pas d'invariants linéaires, mais polynomiaux.Les boucles linéaires sont elles plus expressives que ce qu'il paraîtrait ?Cette thèse présente de nouvelles propriétés sur les boucles linéaires et polynomiales. Il est déjà connu que les boucles linéaires sont polynomialement expressives, au sens ou si plusieurs variables évoluent linéairement dans une boucle, alors n'importe quel monôme de ces variables évolue linéairement. La première contribution de cette thèse est la caractérisation d'une sous classe de boucles polynomiales exactement aussi expressives que des boucles linéaires, au sens où il existe une boucle linéaire avec le même comportement. Ensuite, deux nouvelles méthodes de génération d'invariants sont présentées.La première méthode est basée sur l'interprétation abstraite et s'intéresse aux filtres linéaires convergents. Ces filtres jouent un rôle important dans de nombreux systèmes embarqués (dans l'avionique par exemple) et requièrent l'utilisation de flottants, un type de valeurs qui peut mener à des erreurs d'imprécision s'ils sont mal utilisés. Aussi, la présence d'affectations aléatoires dans ces filtres rend leur analyse encore plus complexe.La seconde méthode traite d'une approche différente basée sur la génération d'invariants pour n'importe quel type de boucles linéaires. Elle part d'un nouveau théorème présenté dans cette thèse qui caractérise les invariants comme étant les vecteurs propres de la transformation linéaire traitée. Cette méthode est généralisée pour prendre en compte les conditions, les boucles imbriquées et le non déterminisme dans les affectations.La génération d'invariants n'est pas un but en soi, mais un moyen. Cette thèse s'intéresse au genre de problèmes que peut résoudre les invariants générés par la seconde méthode. Le premier problème traité est problème de l'orbite (Kannan-Lipton Orbit problem), dont il est possible de générer des certificats de non accessibilité en utilisant les vecteurs propres de la transformation considerée. En outre, les vecteurs propres sont mis à l'épreuve en pratique par leur utilisation dans le model-checker CaFE basé sur la verification de propriétés temporelles sur des programmes C. / The criticality of programs constantly reaches new boundaries as they are relied on to take decisions in place of the user (autonomous cars, robot surgeon, etc.). This raised the need to develop safe programs and to verify the already existing ones.Anyone willing to formally prove the soundness of a program faces the two challenges of scalability and undecidability. Million of lines of code, complexity of the algorithm, concurrency, and even simple polynomial expressions are part of the issues formal verification have to deal with. In order to succeed, formal methods rely on state abstraction to analyze approximations of the behavior of the analyzed program.The analysis of loops is a full axis of formal verification, as this construction is still today not well understood. Though some of them can be easily handled when they perform simple operations, there still exist some seemingly basic loops whose behavior has not been solved yet (the Syracuse sequence for example is suspected to be undecidable).The most common approach for the treatment of loops is the use of loop invariants, i.e. relations on variables that are true at the beginning of the loop and after every step. In general, invariants are expected to use the same set of expressions used in the loop: if a loop manipulates the memory on a structure for example, invariants will naturally use expressions involving memory operations. However, there exist loops containing only linear instructions that admit only polynomial invariants (for example, the sum on integers $sumlimits_{i=0}^n i$ can be computed by a linear loop and is a degree 2 polynomial in n), hence using expressions that are syntacticallyabsent of the loop. Is the previous remark wrong then ?This thesis presents new insights on loops containing linear and polynomial instructions. It is already known that linear loops are polynomially expressive, in the sense that if a variable evolves linearly, then any monomial of this variable evolves linearly. The first contribution of this thesis is the extraction of a class of polynomial loops that is exactly as expressive as linear loops, in the sense that there exist a linear loop with the exact same behavior. Then, two new methods for generating invariants are presented.The first method is based on abstract interpretation and is focused on a specific kind of linear loops called linear filters. Linear filters play a role in many embedded systems (plane sensors for example) and require the use of floating point operations, that may be imprecise and lead to errors if they are badly handled. Also, the presence of non deterministic assignments makes their analysis even more complex.The second method treats of a more generic subject by finding a complete set of linear invariants of linear loops that is easily computable. This technique is based on the linear algebra concept of eigenspace. It is extended to deal with conditions, nested loops and non determinism in assignments.Generating invariants is an interesting topic, but it is not an end in itself, it must serve a purpose. This thesis investigates the expressivity of invariantsgenerated by the second method by generating counter examples for the Kannan-Lipton Orbit problem.It also presents the tool PILAT implementing this technique and compares its efficiency technique with other state-of-the-art invariant synthesizers. The effective usefulness of the invariants generated by PILAT is demonstrated by using the tool in concert with CaFE, a model-checker for C programs based on temporal logics.

Les systèmes concurrents sont un bon choix pour ajuster les données et analyser les mécanismes sous-jacents pour leur sémantique simple mais expressive. Cependant, l’apprentissage et l’analyse de tels systèmes concurrents sont difficiles pour ce qui concerne les calculs. Lorsqu’il s’agit de grands ensembles de données, les techniques les plus récentes semblent insuffisantes, que ce soit en termes d’efficacité ou de précision. Ici, nous proposons un cadre de modélisation raffiné ABAN (Asynchronous Binary Automata Network) et développons des outils pour analyser l’atteignabilité : PermReach (Reachability via Permutation search) et ASPReach (Reachability via Answer Set Programming). Nous proposons ensuite deux méthodes de construction et d’apprentissage des modèles: CRAC (Completion via Reachability And Correlations) et M2RIT (Model Revision via Reachability and Interpretation Transitions) en utilisant des données continues et discrètes pour s’ajuster au modèle et des propriétés d’accessibilité afin de contraindre les modèles en sortie. / Concurrent systems become a good choice to fit the data and analyze the underlying mechanics for their simple but expressive semantics. However, learning and analyzing such concurrent systems are computationally difficult. When dealing with big data sets, the state-of-the-art techniques appear to be insufficient, either in term of efficiency or in term of precision. In this thesis, we propose a refined modeling framework ABAN (Asynchronous Binary Automata Network) and develop reachability analysis techniques based on ABAN: PermReach (Reachability via Permutation search) and ASPReach (Reachability via Answer Set Programming). Then we propose two model learning/constructing methods: CRAC (Completion via Reachability And Correlations) and M2RIT (Model Revision via Reachability and Interpretation Transitions) using continuous and discrete data to fit the model and using reachability properties to constrain the output models.

Cette thèse s'inscrit dans le cadre de la conception de véhicules autonomes, et plus spécifiquement de la vérification de contrôleurs de tels véhicules. Nos contributions à la résolution de ce problème sont les suivantes : (1) fournir une syntaxe et une sémantique pour un modèle de systèmes hybrides, (2) étendre les fonctionnalités du model checker statistique Cosmos à ce modèle et (3) valider empiriquement la pertinence de notre approche sur des cas d'étude typiques du véhicule autonome.Nous avons choisi de combiner le modèle des réseaux de Petri stochastiques de haut niveau (qui était le formalisme d'entrée de Cosmos) avec le formalisme d'entrée de Simulink afin d'atteindre un pouvoir d'expression suffisant. En effet Simulink est très largement utilisé dans le domaine automobile et de nombreux contrôleurs sont spécifiés avec cet outil. Or Simulink n'a pas de sémantique formellement définie. Ceci nous a conduit à concevoir une telle sémantique en deux temps : tout d'abord en introduisant une sémantique dite exacte mais qui n'est pas opérationnelle puis en la complétant par une sémantique approchée intégrant le facteur d'approximation recherché.Afin de combiner le modèle à événements discrets des réseaux de Petri et le modèle continu spécifié en Simulink, nous avons proposé au niveau syntaxique une interfacereposant sur de nouveaux types de transitions et au niveau sémantique une extension de la boucle de simulation. L'évaluation de ce nouveau formalisme a été entièrement implémentée dans Cosmos.Grace à ce nouveau formalisme, nous avons développé et étudié les deux cas d'étude suivants : d'une part une circulation dense sur une section d'autoroute et d'autre part l'insertion du véhicule dans une voie rapide. L'analyse des modélisations correspondantes a démontré la pertinence de notre approche. / This thesis takes place in the context of autonomous vehicle design, and concerns more specifically the verification of controllers of such vehicles. Our contributions are the following: (1) give a syntax and a semantics for a hybrid system model, (2) extend the capacities of the model-checker Cosmos to that kind of models, and (3) empirically confirm the relevance of our approach on typical case studies handling autonomous vehicles.We chose to combine high-level stochastic Petri nets (which is the input formalism of Cosmos) with the input formalism of Simulink, to obtain an adequate expressive power. Indeed, Simulink is largely used in the automotive industry and numerous controllers have been specified using this tool. However, there is no formal semantics for Simulink, which lead us to define such a semantics in two steps:first, we propose an exact (but not operational) semantics, then we complete it by an approximate semantics that includes the targeted approximation level.In order to combine the discrete event model of Petri nets and the continous model specified in Simulink, we define a syntactic interface that relies on new transition types; its semantics consists of an extension of the simulation loop. The evaluation of this new formalism has been entirely implemented into Cosmos.Using this new formalism, we have designed and studied the two following case studies: on one hand, a heavy traffic on a motorway segment, and on the other hand the insertion of a vehicle into a motorway. Our approach has been validated by the analysis of the corresponding models.

Model checking is a technique used to verify whether a model meets a given specification by exhaustively and automatically checking each reachable state in the model. It is a well-developed technique, but it suffers from some issues, perhaps most importantly the state space explosion problem. Models may contain so many states that must be checked means that the model checking procedure may be intractable. In this thesis we investigate whether procedure summaries can be used to improve the performance of model checking. Procedure summaries are concise representations of parts of a program, such as a function or method. We present a design and an implementation of dynamically generated summaries as an extension of Java PathFinder, a virtual machine executing Java bytecode that is able to model check programs written in Java by backtracking execution, to explore different schedulings etc. We find that our summaries incur an overhead that outweighs the benefits in most cases, but the approach shows promise in certain cases, in particular when stateless model checking is used. We also provide some statistics related to cases when our summaries are applicable that could provide guidance for future work within this field. / Model checking, eller modellkontroll, är en välkänd teknik inom programverifikation som används för att verifiera att en modell, ofta av ett program, uppfyller en given specifikation genom att undersöka alla nåbara tillstånd i modellen. Det är en välutvecklad teknik som lider av några brister, en av de viktigaste är det så kallade state space explosion-problemet. Modellerna kan bestå av så många olika tillstånd att \textit{model checking} inte går att använda. I den här rapporten undersöker vi om vi kan tillämpa så kallade procedur-sammanfattningar för att förbättra prestandan av model checking. Procedur-sammanfattningar är representationer av delar av program, till exempel metoder eller funktioner. Vi presenterar en design och implementation av dynamiskt genererade sammanfattningar i form av ett tillägg till Java PathFinder, en virtuell maskin som exekverar Java bytecode som kan utföra model checking genom att backa körningar för att till exempel utforska olika schemaläggningar. Våra procedur-sammanfattningar har i många fall en negativ effekt på körtid, men visar på lovande resultat i vissa fall, i synnerhet när så kallad stateless model checking används. Vi presenterar också resultat kopplat till fall när våra sammanfattningar är applicerbara som kan leda vägen för fortsatt arbete inom området.

Formal verification techniques are growing increasingly vital for the development of safety-critical software and hardware in practice. Techniques such as requirements-based design and model checking for system verification have been successfully used to verify systems for air traffic control, airplane separation assurance, autopilots, CPU logic designs, life-support, medical equipment, and other functions that ensure human safety. Formal behavioral specifications written early in the system-design process and communicated across all design phases increase the efficiency, consistency, and quality of the system under development. We argue that to prevent introducing design or verification errors, it is crucial to test specifications for satisfiability. We advocate for the adaptation of a new sanity check via satisfiability checking for property assurance. Our focus here is on specifications expressed in Linear Temporal Logic (LTL). We demonstrate that LTL satisfiability checking reduces to model checking and satisfiability checking for the specification, its complement, and a conjunction of all properties should be performed as a first step to LTL model checking. We report on an experimental investigation of LTL satisfiability checking. We introduce a large set of rigorous benchmarks to enable objective evaluation of LTL-to-automaton algorithms in terms of scalability, performance, correctness, and size of the automata produced. For explicit model checking, we use the Spin model checker; we tested all LTL-to-explicit automaton translation tools that were publicly available when we conducted our study. For symbolic model checking, we use CadenceSMV, NuSMV, and SAL-SMC for both LTL-to-symbolic automaton translation and to perform the satisfiability check. Our experiments result in two major findings. First, scalability, correctness, and other debilitating performance issues afflict most LTL translation tools. Second, for LTL satisfiability checking, the symbolic approach is clearly superior to the explicit approach. Ironically, the explicit approach to LTL-to-automata had been heavily studied while only one algorithm existed for LTL-to-symbolic automata. Since 1994, there had been essentially no new progress in encoding symbolic automata for BDD-based analysis. Therefore, we introduce a set of 30 symbolic automata encodings. The set consists of novel combinations of existing constructs, such as different LTL formula normal forms, with a novel transition-labeled symbolic automaton form, a new way to encode transitions, and new BDD variable orders based on algorithms for tree decomposition of graphs. An extensive set of experiments demonstrates that these encodings translate to significant, sometimes exponential, improvement over the current standard encoding for symbolic LTL satisfiability checking. Building upon these ideas, we return to the explicit automata domain and focus on the most common type of specifications used in industrial practice: safety properties. We show that we can exploit the inherent determinism of safety properties to create a set of 26 explicit automata encodings comprised of novel aspects including: state numbers versus state labels versus a state look-up table, finite versus infinite acceptance conditions, forward-looking versus backward-looking transition encodings, assignment-based versus BDD-based alphabet representation, state and transition minimization, edge abbreviation, trap-state elimination, and determinization either on-the-fly or up-front using the subset construction. We conduct an extensive experimental evaluation and identify an encoding that offers the best performance in explicit LTL model checking time and is constantly faster than the previous best explicit automaton encoding algorithm.

Regular model checking is a method for verifying infinite-state systems based on coding their configurations as words over a finite alphabet, sets of configurations as finite automata, and transitions as finite transducers. We implement regular model checking using inference of regular languages. The method builds upon the observations that for infinite-state systems whose behavior can be modeled using length-preserving transducers, there is a finite computation for obtaining all reachable configurations.   Our new approach to regular model checking via inference of regular languages is based on the Angluin's L* algorithm that is used for finding out an invariant which can answer our question whether the system satisfies some property.   We also provide an intro to the theory of finite automata, model checking, SAT solving and Anguin's L* and Bierman algorithm of learning finite automata.

No description available.

Doctor of Philosophy / Department of Computing and Information Sciences / Matthew Dwyer / John M. Hatcliff / To analyze an open system, one needs to close it with a definition of its environment, i.e., its execution context. Environment modeling is a significant challenge: environment models should be general enough to permit analysis of large portions of a system's possible behaviors, yet sufficiently precise to enable cost-effective reasoning. This thesis presents the Bandera Environment Generator (BEG), a toolset that automates generation of environment models to provide a restricted form of modular model checking of Java programs, where the module's source code is the subject of analysis along with an abstract model of the environment's behavior. Since the most general environments do not allow for tractable model checking, BEG has support for restricting the environment behavior based on domain-specific knowledge and assumptions about the environment behavior, which can be acquired from a variety of sources. When the environment code is not available, developers can encode their assumptions as an explicit formal specification. When the environment code is available, BEG employs static analyses to extract environment assumptions. Both specifications and static analyses can be tuned to reflect domain-specific knowledge, i.e., to describe domain-specific aspects of the environment behavior. Initially, BEG was implemented to handle general Java applications; later, it was extended to handle two specific domains: Graphical User Interfaces (GUI) implemented using the Swing/AWT libraries and web applications implemented using the J2EE framework. BEG was evaluated on several non-trivial case studies, including industrial applications from NASA, SUN, and Fujitsu. This thesis presents the domain-specific environment generation for GUI and web applications and describes BEG, its extensible architecture, usage, and how it can be extended to handle new domains.

Higher-order recursion schemes are systems of equations that are used to define finite and infinite labelled trees. Since, as Ong has shown, the trees defined have a decidable monadic second order theory, recursion schemes have drawn the attention of research in program verification, where they sit naturally as a higher-order, functional analogue of Boolean programs. Driven by applications, fragments have been studied, algorithms developed and extensions proposed; the emerging theme is called higher-order model checking. Kobayashi has pioneered an approach to higher-order model checking using intersection types, from which many recent advances have followed. The key is a characterisation of model checking as a problem of intersection type assignment. This dissertation contributes to both the theory and practice of the intersection type approach. A new, fixed-parameter polynomial-time decision procedure is described for the alternating trivial automaton fragment of higher-order model checking. The algorithm uses a novel, type-directed form of abstraction refinement, in which behaviours of the scheme are distinguished according to the intersection types that they inhabit. Furthermore, by using types to reason about acceptance and rejection simultaneously, the algorithm is able to converge on a solution from two sides. An implementation, Preface, and an extensive body of evidence demonstrate empirically that the algorithm scales well to schemes of several thousand rules. A comparison with other tools on benchmarks derived from current practice and the related literature puts it well beyond the state-of-the-art. A generalisation of the intersection type approach is presented in which higher-order model checking is seen as an instance of exact abstract interpretation. Intersection type assignment is used to characterise a general class of safety checking problems, defined independently of any particular representation (such as automata) for a class of recursion schemes built over arbitrary constants. Decidability of any problem in the class is an immediate corollary. Moreover, the work looks beyond whole-program verification, the traditional territory of model checking, by giving a natural treatment of higher-type properties, which are sets of functions.

As a technique to ensure absence of undesired interference in transactional computations, Concurrency Control (CC) guarantees logical data consistency via providing transaction isolation, thus contributing to their dependability. However, single-version CC, which requires that a transaction system always works on the current version of a data item, may introduce unpredictable delays for real-time transactions because of unbounded blocking time which may cause deadline misses. Compared to single-version CC (current value of a data item is available but the historical values are overwritten and not accessible) mechanism, multi-version Concurrency Control (MVCC, historical values of a data item are maintained in a version list and accessible) mechanisms have several advantages. The benefit of multiple versions for concurrency control is helping the scheduler avoid rejecting operations, which could improve the concurrency for real-time transaction systems. Because transactions are less likely to be blocked using MVCC, timeliness could be improved. Transaction isolation levels, out of which the serializable one is the highest, control the degree of interference-freedom of concurrent transactions. Instead of serializable isolation, some MVCC mechanisms are known to achieve a relaxed level of isolation. In order to select an appropriate MVCC mechanism that guarantees both timeliness and an acceptable level of isolation for a given transaction set, trade-off analysis between isolation and timeliness is necessary. However, even though approaches have been proposed to analyze timeliness and isolation together, they only focus on lock-based single-version concurrency control algorithms, not on MVCC. In this thesis, we focus on modeling multi-version based real-time transaction system as a network of timed automata, and verify the consistency of the tradeoff transaction timeliness and isolation in UPPAAL. We propose a modular modeling approach to model real-time multi-version transaction systems by reusing and extending set of basic blocks. The proposed approach not only reduces the modeling efforts, but also enables easy adjustment for adapting current MVCC mechanism to another. Assuming a given transaction set, we model three MVCC algorithms including multi-version Timestamp Ordering, a variant of multi-version Two-Phase locking and a Two-Version Priority Ceiling Protocol, and verify both timeliness and isolation level. The verification results show that Two-Version Priority Ceiling Protocol outperforms the other two MVCC algorithms with the given transaction set.