This thesis presents a framework to verify asynchronous real-time systems based on model checking. These systems are modeled by using a common modeling formalism named Labeled Petri-nets(LPNs). In order to verify the real-time systems algorithmically, the zone-based timing analysis method is used for LPNs. It searches the state space with timing information (represented by zones). When there is a high degree of concurrency in the model, firing concurrent enabled transitions in different order may result in different zones, and these zones may be combined without affecting the verification result. Since the zone-based method could not deal with this problem efficiently, the POSET timing analysis method is adopted for LPNs. It separates concurrency from causality and generates an exactly one zone for a single state. But it needs to maintain an extra POSET matrix for each state. In order to save time and memory, an improved zone-based timing analysis method is introduced by integrating above two methods. It searches the state space with zones but eliminates the use of the POSET matrix, which generates the same result as with the POSET method. To illustrate these methods, a circuit example is used throughout the thesis. Since the state space generated is usually very large, a graph data structure named multi-value decision diagrams (MDDs) is implemented to store the zones compactly. In order to share common clock value of dierent zones, two zone encoding methods are described: direct encoding and minimal constraint encoding. They ignore the unnecessary information in zones thus reduce the length of the integer tuples. The effectiveness of these two encoding methods is demonstrated by experimental result of the circuit example.

Software is finding its way into an increasing range of devices (phones, medical equipment, cars...). A challenge is to design verification methods to ensure correctness of software. We focus on model checking, an approach in which an abstract model of the implementation and a specification of requirements are provided. The task is to answer automatically whether the system conforms with its specification.We concentrate on (i) timed systems, and (ii) parameterized systems. Timed systems can be modeled and verified using the classical model of timed automata. Correctness is translated to language inclusion between two timed automata representing the implementation and the specification. We consider variants of timed automata, and show that the problem is at best highly complex, at worst undecidable. A parameterized system contains a variable number of components. The problem is to verify correctness regardless of the number of components. Regular model checking is a prominent method which uses finite-state automata. We present a semi-symbolic minimization algorithm combining the partition refinement algorithm by Paige and Tarjan with decision diagrams. Finally, we consider systems which are both timed and parameterized: Timed Petri Nets (TPNs), and Timed Networks (TNs). We present a method for checking safety properties of TPNs based on forward reachability analysis with acceleration. We show that verifying safety properties of TNs is undecidable when each process has at least two clocks, and explore decidable variations of this problem.

The problem of analyzing concurrent systems has been investigated by many researchers, and several solutions have been proposed. Among the proposed techniques, reachability analysis—systematic enumeration of reachable states in a finite-state model—is attractive because it is conceptually simple and relatively straightforward to automate and can be used in conjunction with model-checking procedures to check for application-specific as well as general properties. The system validation problem considered here is the problem of verifying that the original specification is itself logically consistent. If, for instance, the specification has a design error, an implementation is expected to pass a conformance test if it contains the same error. A validation for the logical consistency of the system, however, must reveal the design error. An automated analysis of all reachable states in a distributed system can be used to trace obscure logical errors that would be very hard to find manually. This type of validation is traditionally performed by the symbolic execution of a finite state machine model of the system studied. The author presents an overview of the existing validation techniques and methods. Specified and analyzed systems are presented as reachable state graph. The implementation of the aggregate specifications validation system is also presented.

The factored state representation and concurrency semantics of Petri nets are closely related to those of classical planning models, yet automated planning and Petri net analysis have developed independently, with minimal and mainly unconvincing attempts at crossfertilisation. This thesis exploits the relationship between the formal reachability problem, and the automated planning problem, via Petri net unfolding, which is an attractive reachability analysis method for highly concurrent systems as it facilitates reasoning about independent sub-problems. The first contribution of this thesis is the theory of directed unfolding: controlling the unfolding process with informative strategies, for the purpose of optimality and increased efficiency. The second contribution is the application of directed unfolding to automated planning. Inspired by well-known planning heuristics, this thesis shows how problem specific information can be employed to guide unfolding, in response to the formal problem of developing efficient, directed reachability analysis methods for concurrent systems. Complimenting this theoretical work, this thesis presents a new forward search method for partial order planning which can be exponentially more efficient than state space search. Our suite of planners based on directed unfolding can perform optimal and suboptimal classical planning subject to arbitrary action costs, optimal temporal planning with respect to arbitrary action durations, and address probabilistic planning via replanning for the most likely path. Empirical results reveal directed unfolding is competitive with current state of the art automated planning systems, and can solve Petri net reachability problems beyond the reach of the original “blind” unfolding technique. / Thesis (Ph.D.) -- University of Adelaide, School of Electrical and Electronic Engineering, 2008

This thesis concerns decision procedures for fragments of linear arithmetic and their application to model-checking one-counter automata. The first part of this thesis covers the complexity of decision problems for different types of linear arithmetic, namely the existential subset of the first-order linear theory over the p-adic numbers and the existential subset of Presburger arithmetic with divisibility, with all integer constants and coefficients represented in binary. The most important result of this part is a new upper complexity bound of <b>NEXPTIME</b> for existential Presburger arithmetic with divisibility. The best bound that was known previously was <b>2NEXPTIME</b>, which followed directly from the original proof of decidability of this theory by Lipshitz in 1976. Lipshitz also gave a proof of <b>NP</b>-hardness of the problem in 1981. Our result is the first improvement of the bound since this original description of a decision procedure. Another new result, which is both an important building block in establishing our new upper complexity bound for existential Presburger arithmetic with divisibility and an interesting result in its own right, is that the decision problem for the existential linear theory of the p-adic numbers is in the Counting Hierarchy <b>CH</b>, and thus within <b>PSPACE</b>. The precise complexity of this problem was stated as open by Weispfenning in 1988, who showed that it is in <b>EXPTIME</b> and <b>NP</b>-hard. The second part of this thesis covers two problems concerning one-counter automata. The first problem is an LTL synthesis problem on one-counter automata with integer-valued and parameterised updates and with equality tests. The decidability of this problem was stated as open by G&ouml;ller et al. in 2010. We give a reduction of this problem to the decision problem of a subset of Presburger arithmetic with divisibility with one quantifier alternation and a restriction on existentially quantified variables. A proof of decidability of this theory is currently under review. The final result of this thesis concerns a type of one-counter automata that differs from the previous one in that it allows parameters only on tests, not actions, and it includes both equality and disequality tests on counter values. The decidability of the basic reachability problem on such one-counter automata was stated as an open problem by Demri and Sangnier in 2010. We show that this problem is decidable by a reduction to the decision problem for Presburger arithmetic.

La sécurité des Systèmes d’Information (SI) constitue un défi majeur car elle conditionne amplement la future exploitation d’un SI. C’est pourquoi l’étude des vulnérabilités d’un SI dès les phases conceptuelles est cruciale. Il s’agit d’étudier la validation de politiques de sécurité, souvent exprimées par des règles de contrôle d’accès, et d’effectuer des vérifications automatisées sur des modèles afin de garantir une certaine confiance dans le SI avant son opérationnalisation. Notre intérêt porte plus particulièrement sur la détection des vulnérabilités pouvant être exploitées par des utilisateurs internes afin de commettre des attaques, appelées attaques internes, en profitant de leur accès légitime au système. Pour ce faire, nous exploitons des spécifications formelles B générées, par la plateforme B4MSecure, à partir de modèles fonctionnels UML et d’une description Secure UML des règles de contrôle d’accès basées sur les rôles. Ces vulnérabilités étant dues à l’évolution dynamique de l’état fonctionnel du système, nous proposons d’étudier l’atteignabilité des états, dits indésirables, donnant lieu à des attaques potentielles, à partir d’un état normal du système. Les techniques proposées constituent une alternative aux techniques de model-checking. En effet, elles mettent en œuvre une recherche symbolique vers l’arrière fondée sur des approches complémentaires : la preuve et la résolution de contraintes. Ce processus de recherche est entièrement automatisé grâce à notre outil GenISIS qui a montré, sur la base d’études de cas disponibles dans la littérature, sa capacité à retrouver des attaques déjà publiées mais aussi des attaques nouvelles. / The early detection of potential threats during the modelling phase of a Secure Information System (IS) is required because it favours the design of a robust access control policy and the prevention of malicious behaviours during the system execution. This involves studying the validation of access control rules and performing vulnerabilities automated checks before the IS operationalization. We are particularly interested in detecting vulnerabilities that can be exploited by internal trusted users to commit attacks, called insider attacks, by taking advantage of their legitimate access to the system. To do so, we use formal B specifications which are generated by the B4MSecure platform from UML functional models and a SecureUML modelling of role-based access control rules. Since these vulnerabilities are due to the dynamic evolution of the functional state, we propose to study the reachability of someundesirable states starting from a normal state of the system. The proposed techniques are an alternative to model-checking techniques. Indeed, they implement symbolic backward search algorithm based on complementary approaches: proof and constraint solving. This rich technical background allowed the development of the GenISIS tool which automates our approach and which was successfully experimented on several case studies available in the literature. These experiments showed its capability to extract already published attacks but also new attacks.

The aim of this thesis is to explore the potential of resolution-based methods for linear temporal reasoning. On the abstract level, this means to develop new algorithms for automated reasoning about properties of systems which evolve in time. More concretely, we will: 1) show how to adapt the superposition framework to proving theorems in propositional Linear Temporal Logic (LTL), 2) use a connection between superposition and the CDCL calculus of modern SAT solvers to come up with an efficient LTL prover, 3) specialize the previous to reachability properties and discover a close connection to Property Directed Reachability (PDR), an algorithm recently developed for model checking of hardware circuits, 4) further improve PDR by providing a new technique for enhancing clause propagation phase of the algorithm, and 5) adapt PDR to automated planning by replacing the SAT solver inside with a planning-specific procedure. We implemented the proposed ideas and provide experimental results which demonstrate their practical potential on representative benchmark sets. Our system LS4 is shown to be the strongest LTL prover currently publicly available. The mentioned enhancement of PDR substantially improves the performance of our implementation of the algorithm for hardware model checking in the multi-property...

L’objectif de cette thèse est la modélisation et l’étude de systèmes biologiques par l’intermédiaire de méthodes formelles. Les systèmes biologiques démontrent des comportements continus mais sont aussi susceptibles de montrer des changements abrupts dans leur dynamiques. Les équations différentielles ordinaires, ainsi que les systèmes dynamiques hybrides, sont deux formalismes mathématiques utilisés pour modéliser clairement de tels comportements. Un point critique de la modélisation de systèmes biologiques est la recherche des valeurs des paramètres du modèle afin de reproduire de manière précise un ensemble de données expérimentales. Si aucun jeu de paramètres valides n’est trouvé, il est nécessaire de réviser le modèle. Une possibilité est alors de remplacer un paramètre, ou un ensemble de paramètres, définissant un processus biologique par une fonctiondépendante du temps.Dans le cadre de cette thèse, nous exposons tout d’abord une méthode pour la révision de modèles hybrides. Pour cela, nous proposons une approche gloutonne appliquée à une méthode de contrôle optimal utilisant les mesures d’occupations etla relaxation convexe. Ensuite, nous étudions comment analyser les propriétés dynamiques d’un modèle à temps discret en utilisant la simulation ensembliste. Dans cet objectif, nous proposons deux méthodes basées sur deux outils mathématiques.La première méthode, qui se repose sur les polynômes de Bernstein, est une extension aux systèmes dynamiques hybrides, de l’outil de calcul ensembliste Sapo [1]. La seconde méthode utilise les représentations de Krivine-Stengle [2] pour permettre l’analyse d’atteignaiblité de systèmes dynamiques polynomiaux. Enfin, nous proposons aussi une méthodologie pour générer des systèmes dynamiques hybrides modélisant des protocoles biologiques expérimentaux. Les méthodes précédemment proposées sont appliquées sur divers études biologiques. Nous étudions tout d’abord un modèle de la production d’hémoglobinedurant la différentiation des érythrocytes dans la moelle [3]. Pour permettre la construction de ce modèle, nous avons dans un premier temps généré un ensemble de jeux de paramètres valides à l’aide d’une méthode de type Monte-Carlo. Dans un second temps, nous avons appliqué la méthode de révision de modèle afin de reproduire plus précisément les données expérimentales [4]. Nous proposons aussi un modèle préliminaire des effets à faibles doses du Cadmium sur la réponse du métabolisme à différentes étapes de la vie d’un rat. Enfin, nous appliquons les techniques d’analyse ensembliste pour la validation d’hypothèses sur un modèle d’homéostasie du fer [6] dans le cas où des paramètres varient dans de larges intervalles.Dans cette thèse, nous montrons aussi que le protocole associé à l’étude de la production d’hémoglobine, ainsi que le protocole étudiant l’intégration du Cadmium durant la vie d’un rat, peuvent être formalisés comme des systèmes dynamiques hybrides, et servent ainsi de preuves de concepts pour notre méthode de modélisation de protocoles expérimentaux / The purpose of this thesis is the modelling and analysis of biological systems with mechanistic models (in opposition with black-box models).In particular we use two mathematical formalisms for mechanism modelling: hybrid dynamical systems and polynomial Ordinary Differential Equations (ODEs).Biological systems modelling give rise to numerous problem and in this work we address three of them.First, the parameters in the differential equations are often uncertain or unknown.Consequently, we aim at generating a subset of valid parameter sets such that the models satisfy constraints deducted from some experimental data.This problem is addressed in the literature under the denomination of parameter synthesis, parameter estimation, parameter fitting, or parameter identification following the context.Then, if no valid parameter is found, one solution is to revise the model. This can be done by substituting a law in place of a constant parameter.In the literature, models with uncertain parts are known as grey models, and their studies can be found under the term of model identification.Finally, it may be necessary to ensure the correctness of the built models using validation, or verification, methods for a continuous over-approximation of the determined valid parameters.In this thesis we study the parameter synthesis problem, in the Haemoglobin production model case study, using an adaptation of the classical method based on Monte-Carlo sampling, and numerical simulations.To perform model revision of hybrid dynamical systems we propose an iterative scheme of an optimal control method based on occupation measures, and convex relaxations.Finally, we assess the quality of a model using set-based simulations, and reachability analysis.For this purpose, we propose two methods: the first one, which relies on Bernstein expansion, is an extension for hybrid dynamical systems of the reachability tool sapo , while the other uses Krivine-Stengle representations to perform the reachability analysis of polynomial ODEs.We also provide a methodology to generate hybrid dynamical systems modelling biological experimental protocols.All of these proposed methods were applied in different case studies.We first propose a model of haemoglobin production during the differentiation of an erythrocyte in the bone marrow.To develop this model we first applied the Monte-Carlo based parameters synthesis, followed by the model revision to correctly fit to the experimental data.We also propose a hybrid model of Cadmium flux in rats in the context of an experimental protocol, as well as a preliminary study of the effect of low dose Cadmium on a Glucose response.Finally, we apply the reachability analysis techniques for the validation on large parameters set of the iron homoeostasis model developed by Nicolas Mobilia during his Phd.We note the haemoglobin production model, as well as the glucose reponse model can be formalised, in their experimental context, as hybrid dynamical systems. Thus, they serve as proof of concept for the methodology of biological experimental protocols modelling.

Dans la conception basée sur des modèles on construit un modèle mathématique du système que l'on utilise pour concevoir le système de sorte qu'il présente les propriétés souhaitées. Pour les systèmes de sûreté critique, il peut être d'une importance capitale de vérifier ces propriétés de sûreté sur le modèle, par exemple, pour tenir compte des variations des paramètres. Le calcul d'un nombre fini de comportements du système par le biais de simulation ne suffit pas à garantir des propriétés de sécurité. Avec une analyse d'atteignabilité on peut calculer une couverture de tous les comportements possibles du système, possiblement infinis. Cette analyse peut prendre en compte de non-déterminisme dans le modèle et peut garantir des propriétés de sécurité. Les systèmes d'intérêt présentent souvent à la fois un comportement continu et discret et de tels systèmes sont appelés systèmes hybrides. Le calcul d'atteignabilité est considéré comme difficile pour les systèmes continus et hybrides. Ce n'est que récemment que des méthodes pour le calcul d'accessibilité ont été développées qui peuvent être mis à l'échèlle. Ils sont basés sur des représentations implicites d'ensembles continus à l'aide du concepte mathématique de la fonction de support. Dans cette thèse, nous développons un outil extensible appelé SpaceEx pour le calcul d'atteignabilité des systèmes hybrides. Deux algorithmes d'atteignabilité ont été mis en œuvre dans SpaceEx, l'un basé sur l'outil PHAVer pour les automates linéaires hybrides et l'autre basé sur les fonctions de support pour les dynamiques affines par morceaux. L'algorithme de fonction support a été mis au point et sa mise à l'échelle a été amélioré en basculant entre différentes représentations d'ensembles continus. Nous proposons un algorithme de calcul d'image des transition discrètes amélioré qui réduit l'erreur de sur-approximation et nous illustrons sa précision et son efficacité avec plusieurs études de cas. / In model based design, one constructs a mathematical model of the system and uses it to design the system so that it exhibits the desired properties. For safety critical systems, it can be of utmost importance to verify these safety properties on the model, e.g., to account for parameter variations. Computing a finite number of system behaviors via simulation is not sufficient to guarantee safety properties. With a reachability analysis one can compute a cover of all possible system behaviors, potentially infinite, accounting for any non-determinism in the model, and with which one can guarantee safety properties. Systems of interest often exhibit both continuous and discrete behavior and such systems are called hybrid systems. Reachability computation is considered hard for continuous and hybrid systems. Only recently, scalable methods for reachability computation have been developed based on implicit set representations using the mathematical construct of support functions. In this thesis, we develop an extendable tool called SpaceEx for reachability of hybrid systems. Two reachability algorithms have been implemented in SpaceEx, one based on the PHAVer tool for linear hybrid automata and the other based on support functions for piecewise affine dynamics. The support function based algorithm has been tuned and its scalability has been improved by switching set representations. We propose an improved image computation algorithm for discrete transition that further reduces the over-approximation error and illustrate its accuracy and efficiency with several case studies.

Planejamento em inteligência artificial é a tarefa de determinar ações que satisfaçam um dado objetivo. Nos problemas de planejamento sob incerteza, as ações podem ter efeitos probabilísticos. Esses problemas são modelados como Processos de Decisão Markovianos (Markov Decision Processes - MDPs), modelos que permitem o cálculo de soluções ótimas considerando o valor esperado de cada ação em cada estado. Contudo, resolver problemas grandes de planejamento probabilístico, i.e., com um grande número de estados e ações, é um enorme desafio. MDPs grandes podem ser reduzidos através da computação de bissimulações estocásticas, i.e., relações de equivalência sobre o conjunto de estados do MDP original. A partir das bissimulações estocásticas, que podem ser exatas ou aproximadas, é possível obter um modelo abstrato reduzido que pode ser mais fácil de resolver do que o MDP original. No entanto, para problemas de alguns domínios, a computação da bissimulação estocástica sobre todo o espaço de estados é inviável. Os algoritmos propostos neste trabalho estendem os algoritmos usados para a computação de bissimulações estocásticas para MDPs de forma que elas sejam computadas sobre o conjunto de estados alcançáveis a partir de um dado estado inicial, que pode ser muito menor do que o conjunto de estados completo. Os resultados experimentais mostram que é possível resolver problemas grandes de planejamento probabilístico com desempenho superior às técnicas conhecidas de bissimulação estocástica. / Planning in artificial intelligence is the task of finding actions to reach a given goal. In planning under uncertainty, the actions can have probabilistic effects. This problems are modeled using Markov Decision Processes (MDPs), models that enable the computation of optimal solutions considering the expected value of each action when applied in each state. However, to solve big probabilistic planning problems, i.e., those with a large number of states and actions, is still a challenge. Large MDPs can be reduced by computing stochastic bisimulations, i.e., equivalence relations over the original MDP states. From the stochastic bisimulations, that can be exact or approximated, it is possible to get an abstract reduced model that can be easier to solve than the original MDP. But, for some problems, the stochastic bisimulation computation over the whole state space is unfeasible. The algorithms proposed in this work extend the algorithms that are used to compute stochastic bisimulations for MDPs in a way that they can be computed over the reachable set of states with a given initial state, which can be much smaller than the complete set of states. The empirical results show that it is possible to solve large probabilistic planning problems with better performance than the known techniques of stochastic bisimulation.