<p align="justify">Computer Science is currently facing a grand challenge : finding good design practices for embedded systems. Embedded systems are essentially computers interacting with some physical process. You could find one in a braking systems or in a nuclear power plant for example. They present several design difficulties : first they are reactive systems, interacting indefinitely with their environment. Second,they must satisfy real-time constraints specifying when they should respond, and not only how. Finally, their environment is often deeply continuous, presenting complex dynamics. The formal models of choice for specifying such systems are timed and hybrid automata for which model checking is pretty well studied.</p> <p align="justify">In a first part of this thesis, we study a complete design approach, including verification and code generation, for timed automata. We have to define a new semantics for timed automata, the AASAP semantics, that preserves the decidability properties for model checking and at the same time is implementable. Our notion of implementability is completely novel, and relies on the simulation of a semantics that is obviously implementable on a real platform. We wrote tools for the analysis and code generation and exemplify them on a case study about the well known Philips Audio Control Protocol.</p> <p align="justify">In a second part of this thesis, we study the problem of controller synthesis for an environment specified as a hybrid automaton. We give a new solution for discrete controllers having only an imperfect information about the state of the system. In the process, we defined a new algorithm, based on the monotonicity of the controllable predecessors operator, for efficiently finding a controller and we show some promising applications on a classical problem : the universality test for finite automata.

Model checking is a fully-automatic formal verification method that has been extremely successful in validating and verifying safety-critical systems in the past three decades. In the past fifteen years, there has been a lot of work in extending many model checking algorithms over finite-state systems to finitely representable infinitestate systems. Unlike in the case of finite systems, decidability can easily become a problem in the case of infinite-state model checking. In this thesis, we present generic and specific techniques that can be used to derive decidability with near-optimal computational complexity for various model checking problems over infinite-state systems. Generic techniques and specific techniques primarily differ in the way in which a decidability result is derived. Generic techniques is a “top-down” approach wherein we start with a Turing-powerful formalismfor infinitestate systems (in the sense of being able to generate the computation graphs of Turing machines up to isomorphisms), and then impose semantic restrictions whereby the desired model checking problem becomes decidable. In other words, to show that a subclass of the infinite-state systems that is generated by this formalism is decidable with respect to the model checking problem under consideration, we will simply have to prove that this subclass satisfies the semantic restriction. On the other hand, specific techniques is a “bottom-up” approach in the sense that we restrict to a non-Turing powerful formalism of infinite-state systems at the outset. The main benefit of generic techniques is that they can be used as algorithmic metatheorems, i.e., they can give unified proofs of decidability of various model checking problems over infinite-state systems. Specific techniques are more flexible in the sense they can be used to derive decidability or optimal complexity when generic techniques fail. In the first part of the thesis, we adopt word/tree automatic transition systems as a generic formalism of infinite-state systems. Such formalisms can be used to generate many interesting classes of infinite-state systems that have been considered in the literature, e.g., the computation graphs of counter systems, Turing machines, pushdown systems, prefix-recognizable systems, regular ground-tree rewrite systems, PAprocesses, order-2 collapsible pushdown systems. Although the generality of these formalisms make most interesting model checking problems (even safety) undecidable, they are known to have nice closure and algorithmic properties. We use these nice properties to obtain several algorithmic metatheorems over word/tree automatic systems, e.g., for deriving decidability of various model checking problems including recurrent reachability, and Linear Temporal Logic (LTL) with complex fairness constraints. These algorithmic metatheorems can be used to uniformly prove decidability with optimal (or near-optimal) complexity of various model checking problems over many classes of infinite-state systems that have been considered in the literature. In fact, many of these decidability/complexity results were not previously known in the literature. In the second part of the thesis, we study various model checking problems over subclasses of counter systems that were already known to be decidable. In particular, we consider reversal-bounded counter systems (and their extensions with discrete clocks), one-counter processes, and networks of one-counter processes. We shall derive optimal complexity of various model checking problems including: model checking LTL, EF-logic, and first-order logic with reachability relations (and restrictions thereof). In most cases, we obtain a single/double exponential reduction in the previously known upper bounds on the complexity of the problems.

Cette thèse propose une nouvelle approche pour la synthèse de valeurs temporelles dans les systèmes temporisés. Notre approche est basée sur la méthode inverse suivante : à partir d’une instance de référence des paramètres, nous synthétisons une contrainte sur les paramètres, garantissant le même comportement que pour l’instance de référence, abstraction faite du temps. Il en résulte un critère de robustesse pour le système. En itérant cette méthode sur des points dans un domaine paramétrique borné, nous sommes alors à même de partitionner l’espace des paramètres en bonnes et mauvaises zones par rapport à une propriété à vérifier. Ceci nous donne une cartographie comportementale du système. Cette méthode s’étend aisément aux systèmes probabilistes. Nous présentons également des variantes de la méthode inverse pour les graphes orientés valués et les processus de décision markoviens. Parmi les prototypes implémentés, IMITATOR II implémente la méthode inverse et la cartographie pour les automates temporisés. Ce prototype nous a permis de synthétiser de bonnes valeurs pour les paramètres temporels de plusieurs études de cas, dont un modèle abstrait d’une mémoire commercialisée par le fabricant de puces STMicroelectronics, ainsi que plusieurs protocoles de communication. / This thesis proposes a novel approach for the synthesis of delays for timed systems, in particular in the framework oftimed automata, a model for verifying real-time systems. Our approach relies on the following inverse method: given a reference valuation of the parameters, we synthesize a constraint on the parameters, guaranteeing the same timeabstract linear behavior as for the reference valuation. This gives a criterion of robustness to the system. By iterating this inverse method on various points of a bounded parameter domain, we are then able to partition the parametric space into good and bad zones, with respect to a given property one wants to verify. This gives a behavioral cartography of the system. This method extended to probabilistic systems allows to preserve minimum and maximum probabilities of reachability properties. We also present variants of the inverse method for directed weighted graphs and Markov Decision Processes. Several prototypes have been implemented; in particular, IMITATOR II implements the inverse method and the cartography for timed automata. It allowed us to synthesize parameter values for several case studies such as an abstract model of a memory circuit sold by the chipset manufacturer ST-Microelectronics, and various communication protocols.

Software-intensive systems are increasingly expected to operate under changing and uncertain conditions, including not only varying user needs and workloads, but also fluctuating resource capacity. Self-adaptation is an approach that aims to address this problem, giving systems the ability to change their behavior and structure to adapt to changes in themselves and their operating environment without human intervention. Self-adaptive systems tend to be reactive and myopic, adapting in response to changes without anticipating what the subsequent adaptation needs will be. Adapting reactively can result in inefficiencies due to the system performing a suboptimal sequence of adaptations. Furthermore, some adaptation tactics—atomic adaptation actions that leave the system in a consistent state—have latency and take some time to produce their effect. In that case, reactive adaptation causes the system to lag behind environment changes. What is worse, a long running adaptation action may prevent the system from performing other adaptations until it completes, further limiting its ability to effectively deal with the environment changes. To address these limitations and improve the effectiveness of self-adaptation, we present proactive latency-aware adaptation, an approach that considers the timing of adaptation (i) leveraging predictions of the near future state of the environment to adapt proactively; (ii) considering the latency of adaptation tactics when deciding how to adapt; and (iii) executing tactics concurrently. We have developed three different solution approaches embodying these principles. One is based on probabilistic model checking, making it inherently able to deal with the stochastic behavior of the environment, and guaranteeing optimal adaptation choices over a finite decision horizon. The second approach uses stochastic dynamic programming to make adaptation decisions, and thanks to performing part of the computations required to make those decisions off-line, it achieves a speedup of an order of magnitude over the first solution approach without compromising optimality. A third solution approach makes adaptation decisions based on repertoires of adaptation strategies— predefined compositions of adaptation tactics. This approach is more scalable than the other two because the solution space is smaller, allowing an adaptive system to reap some of the benefits of proactive latency-aware adaptation even if the number of ways in which it could adapt is too large for the other approaches to consider all these possibilities. We evaluate the approach using two different classes of systems with different adaptation goals, and different repertoires of adaptation strategies. One of them is a web system, with the adaptation goal of utility maximization. The other is a cyberphysical system operating in a hostile environment. In that system, self-adaptation must not only maximize the reward gained, but also keep the probability of surviving a mission above a threshold. In both cases, our results show that proactive latency-aware adaptation improves the effectiveness of self-adaptation with respect to reactive time-agnostic adaptation.

Higher-order recursion schemes are a powerful model of functional computation that grew out of traditional recursive program schemes and generalisations of grammars. It is common to view recursion schemes as generators of possibly-infinite trees, which Ong showed to have a decidable monadic second order theory and opened the door to applications in verification. Kobayashi later presented an intersection type characterisation of the model checking problem, on which most subsequent applied work is based. In recent work, recursion schemes have been considered to play a role similar to Boolean programs in verification of first-order imperative programs: a natural target for abstraction of programs with very large or infinite data domains. In this thesis we focus on the development of model checking algorithms for variants of recursion schemes. We start our contributions with a model checking algorithm inspired by the fully abstract game semantics of recursion schemes, but specified as a goal-directed approach to intersection type inference, that offers a unification of the views of Ong and Kobayashi. We build on this largely theoretical contribution with two orthogonal extensions and practical implementations. First, we develop a new extension of recursion schemes: higher-order recursion schemes with cases, which add non-determinism and a case construct operating over a finite data domain. These additions provide us with a more natural and succinct target for abstraction from functional programs: encoding data using functions inevitably results in an increase in the order and arity of the scheme, which have a direct impact on the worst-case complexity of the problem. We characterise the model checking problem using a novel intersection and union type system and give a practical algorithm for type inference in this system. We have carried out an empirical evaluation of the implementation --- the tool T_RAVMC --- using a variety of problem instances from the literature and a new suite of problem instances derived via an abstraction-refinement procedure from functional programs. Second, we extend our approach from safety properties to all properties expressible in monadic second order logic using alternating parity tree automata as our specification language. We again provide an implementation and an empirical evaluation, which shows that despite the challenges accompanying liveness properties our tool scales beyond the current state of the art.

This dissertation documents two contributions to automating the formal verification of hardware – particularly memory-intensive circuits – by Symbolic Trajectory Evaluation (STE), a model checking technique based on symbolic simulation over abstract sets of states. The contributions focus on improvements to the use of BDD-based STE, which uses binary decision diagrams internally. We introduce a solution to one of the major hurdles in using STE: finding suitable abstractions. Our work has produced the first known algorithm that addresses this problem by automatically discovering good, non-trivial abstractions. These abstractions are computed from the specification, and essentially encode partial input combinations sufficient for determining the specification’s output value. They can then be used to verify whether the hardware model meets its specification using a technique based on and significantly extending previous work by Melham and Jones [2]. Moreover, we prove that our algorithm delivers correct results by construction. We demonstrate that the abstractions received by our algorithm can greatly reduce verification costs with three example hardware designs, typical of the kind of problems faced by the semiconductor design industry. We further propose a refinement method for abstraction schemes when over- abstraction occurs, i.e., when the abstraction hides too much information of the original design to determine whether it meets its specification. The refinement algorithm we present is based on previous work by Chockler et al. [3], which selects refinement candidates by approximating which abstracted input is likely the biggest cause of the abstraction being unsuitable. We extend this work substantially, concentrating on three aspects. First, we suggest how the approach can also work for much more general abstraction schemes. This enables refining any abstraction allowed in STE, rather than just a subset. Second, Chockler et al. describe how to refine an abstraction once a refinement candidate has been identified. We present three additional variants of refining the abstraction. Third, the refinement at its core depends on evaluating circuit logic gates. The previous work offered solutions for NOT- and AND-gates. We propose a general approach to evaluating arbitrary logic gates, which improves the selection process of refinement candidates. We show the effectiveness of our work by automatically refining an abstraction for a content-addressable memory that exhibits over-abstraction, and by evaluating some common logic gates. These two contributions can be used independently to help automate the hard- ware verification by STE, but they also complement each other. To show this, we combine both algorithms to create a fully automatic abstraction discovery and refinement loop. The only inputs required are the hardware design and the specification, which the design should meet. While only small circuits could be verified completely automatically, it clearly shows that our two contributions allow the construction of a verification framework that does not require any user interaction.

Many software systems exhibit probabilistic behaviour, either added explicitly, to improve performance or to break symmetry, or implicitly, through interaction with unreliable networks or faulty hardware. When employed in safety-critical applications, it is important to rigorously analyse the behaviour of these systems. This can be done with a formal verification technique called model checking, which establishes properties of systems by algorithmically considering all execution scenarios. In the presence of probabilistic behaviour, we consider quantitative properties such as "the worst-case probability that the airbag fails to deploy within 10ms", instead of qualitative properties such as "the airbag eventually deploys". Although many model checking techniques exist to verify qualitative properties of software, quantitative model checking techniques typically focus on manually derived models of systems and cannot directly verify software. In this thesis, we present two quantitative model checking techniques for probabilistic software. The first is a quantitative adaptation of a successful model checking technique called counter-example guided abstraction refinement which uses stochastic two-player games as abstractions of probabilistic software. We show how to achieve abstraction and refinement in a probabilistic setting and investigate theoretical extensions of stochastic two-player game abstractions. Our second technique instruments probabilistic software in such a way that existing, non-probabilistic software verification methods can be used to compute bounds on quantitative properties of the original, uninstrumented software. Our techniques are the first to target real, compilable software in a probabilistic setting. We present an experimental evaluation of both approaches on a large range of case studies and evaluate several extensions and heuristics. We demonstrate that, with our methods, we can successfully compute quantitative properties of real network clients comprising approximately 1,000 lines of complex ANSI-C code — the verification of such software is far beyond the capabilities of existing quantitative model checking techniques.

Models of true concurrency have gained a lot of interest over the last decades as models of concurrent or distributed systems which avoid the well-known problem of state space explosion of the interleaving models. In this thesis, we study such models from two perspectives. Firstly, we study the relation between Petri nets and stable event structures. Petri nets can be considered as one of the most general and perhaps wide-spread models of true concurrency. Event structures on the other hand, are simpler models of true concurrency with explicit causality and conflict relations. Stable event structures expand the class of event structures by allowing events to be enabled in more than one way. While the relation between Petri nets and event structures is well understood, the relation between Petri nets and stable event structures has not been studied explicitly. We define a new and more compact unfoldings of safe Petri nets which is directly translatable to stable event structures. In addition, the notion of complete finite prefix is defined for compact unfoldings, making the existing model checking algorithms applicable to them. We present algorithms for constructing the compact unfoldings and their complete finite prefix. Secondly, we study probabilistic models of true concurrency. We extend the definition of probabilistic event structures as defined by Abbes and Benveniste to a newly defined class of stable event structures, namely, jump-free stable event structures arising from Petri nets (characterised and referred to as net-driven). This requires defining the fundamental concept of branching cells in probabilistic event structures, for jump-free net-driven stable event structures, and by proving the existence of an isomorphism among the branching cells of these systems, we show that the latter benefit from the related results of the former models. We then move on to defining a probabilistic logic over probabilistic event structures (PESL). To our best knowledge, this is the first probabilistic logic of true concurrency. We show examples of expressivity achieved by PESL, which in particular include properties related to synchronisation in the system. This is followed by the model checking algorithm for PESL for finite event structures. Finally, we present a logic over stable event structures (SEL) along with an account of its expressivity and its model checking algorithm for finite stable event structures.

Threaded Behavioral Protocols (TBP) is a specification language for modelling the behavior of software components. This thesis aims at an analysis of TBP specifications within environments which involve an unbounded replication of threads. Such a TBP specification - together with a model of the possible environments - induces infinite state space which contains a vast amount of symmetries caused by thread replication. A model checking technique addressing such a state space and reducing the symmetries by using symbolic counter abstraction is proposed. In order to utilize the symbolic counter abstraction, the properties of the TBP specifications (called provisions) are converted into thread state reachability properties. The proposed analysis is safe in the sense that it discovers all errors in the model. On the other hand, it may yield spurious errors, i.e., errors that do not correspond to any real error in the model. The spurious errors are well identified and further possibilities to reduce them are outlined. Beyond the scope of the specific specifications, this work may also present a small step towards supporting dynamic thread creation in TBP.

Systems biology aims to describe and understand biology at a global scale where biological systems function as a result of complex mechanisms that happen at several scales. Modelling and simulation are computational tools that are invaluable for description, understanding and prediction these mechanisms in a quantitative and integrative way. Thus multi-scale methods that couple the design, simulation and analysis of models spanning several spatial and temporal scales is becoming a new emerging focus of systems biology. This thesis uses an exemplar – Planar cell polarity (PCP) signalling – to illustrate a generic approach to model biological systems at different spatial scales, using the new concept of Hierarchically Coloured Petri Nets (HCPN). PCP signalling refers to the coordinated polarisation of cells within the plane of various epithelial tissues to generate sub-cellular asymmetry along an axis orthogonal to their apical-basal axes. This polarisation is required for many developmental events in both vertebrates and non-vertebrates. Defects in PCP in vertebrates are responsible for developmental abnormalities in multiple tissues including the neural tube, the kidney and the inner ear. In Drosophila wing, PCP is seen in the parallel orientation of hairs that protrude from each of the approximately 30,000 epithelial cells to robustly point toward the wing tip. This work applies HCPN to model a tissue comprising multiple cells hexagonally packed in a honeycomb formation in order to describe the phenomenon of Planar Cell Polarity (PCP) in Drosophila wing. HCPN facilitate the construction of mathematically tractable, compact and parameterised large-scale models. Different levels of abstraction that can be used in order to simplify such a complex system are first illustrated. The PCP system is first represented at an abstract level without modelling details of the cell. Each cell is then sub-divided into seven virtual compartments with adjacent cells being coupled via the formation of intercellular complexes. A more detailed model is later developed, describing the intra- and inter-cellular signalling mechanisms involved in PCP signalling. The initial model is for a wild-type organism, and then a family of related models, permitting different hypotheses to be explored regarding the mechanisms underlying PCP, are constructed. Among them, the largest model consists of 800 cells which when unfolded yields 164,000 places (each of which is described by an ordinary differential equation). This thesis illustrates the power and validity of the approach by showing how the models can be easily adapted to describe well-documented genetic mutations in the Drosophila wing using the proposed approach including clustering and model checking over time series of primary and secondary data, which can be employed to analyse and check such multi-scale models similar to the case of PCP. The HCPN models support the interpretation of biological observations reported in literature and are able to make sensible predictions. As HCPN model multi-scale systems in a compact, parameterised and scalable way, this modelling approach can be applied to other large-scale or multi-scale systems.