Probabilistic model checking mainly concentrates on techniques for reasoning about the probabilities of certain path properties or expected values of certain random variables. For the quantitative system analysis, however, there is also another type of interesting performance measure, namely quantiles. A typical quantile query takes as input a lower probability bound p ∈ ]0,1] and a reachability property. The task is then to compute the minimal reward bound r such that with probability at least p the target set will be reached before the accumulated reward exceeds r. Quantiles are well-known from mathematical statistics, but to the best of our knowledge they have not been addressed by the model checking community so far. In this paper, we study the complexity of quantile queries for until properties in discrete-time finite-state Markov decision processes with nonnegative rewards on states. We show that qualitative quantile queries can be evaluated in polynomial time and present an exponential algorithm for the evaluation of quantitative quantile queries. For the special case of Markov chains, we show that quantitative quantile queries can be evaluated in pseudo-polynomial time.

The Parameterised Model Checking Problem asks whether an implementation Impl(t) satisfies a specification Spec(t) for all instantiations of parameter t. In general, t can determine numerous entities: the number of processes used in a network, the type of data, the capacities of buffers, etc. The main theme of this thesis is automation of uniform verification of a subclass of PMCP with the parameter of the first kind, using techniques based on counter abstraction. Counter abstraction works by counting how many, rather than which, node processes are in a given state: for nodes with k local states, an abstract state (c(1), ..., c(k)) models a global state where c(i) processes are in the i-th state. We then use a threshold function z to cap the values of each counter. If for some i, counter c(i) reaches its threshold, z(i) , then this is interpreted as there being z(i) or more nodes in the i-th state. The addition of thresholds makes abstract models independent of the instantiation of the parameter. We adapt standard counter abstraction techniques to concurrent reactive systems modelled using the CSP process algebra. We demonstrate how to produce abstract models of systems that do not use node identifiers (i.e. where all nodes are indistinguishable). Every such abstraction is, by construction, refined by all instantiations of the implementation. If the abstract model satisfies the specification, then a positive answer to the particular uniform verification problem can be deduced. We show that by adding node identifiers we make the uniform verification problem undecidable. We demonstrate a sound abstraction method that extends standard counter abstraction techniques to systems that make full use of node identifiers (in specifications and implementations). However, on its own, the method is not enough to give the answer to verification problems for all parameter instantiations. This issue has led us to the development of a type reduction theory, which, for a given verification problem, establishes a function phi that maps all (sufficiently large) instantiations T of the parameter to some fixed type T and allows us to deduce that if Spec(T) is refined by phi(Impl(T)), then Spec(T) is refined by Impl(T). We can then combine this with our extended counter abstraction techniques and conclude that if the abstract model satisfies Spec(T), then the answer to the uniform verification problem is positive. We develop a symbolic operational semantics for CSP processes that satisfy certain normality requirements and we provide a set of translation rules that allow us to concretise symbolic transition graphs. The type reduction theory relies heavily on these results. One of the main advantages of our symbolic operational semantics and the type reduction theory is their generality, which makes them applicable in other settings and allows the theory to be combined with abstraction methods other than those used in this thesis. Finally, we present TomCAT, a tool that automates the construction of counter abstraction models and we demonstrate how our results apply in practice.

Este trabalho reflete os esforcos realizados no estudo das principais técnicas automaticas de verificacao de sistemas que podem ser modelados em Maquinas de Estados Finitas, em particular as que normalmente se enquadram dentro da denominacao de model checking (verificacao de modelos). De modo a permitir ao leitor uma compreensao das vantagens e desvantagens de cada tecnica, os fundamentos teoricos de cada uma delas sao apresentados e ilustrados atraves de exemplos. Alem de uma apresentacao da teoria associada a cada tecnica, esta dissertação ainda apresenta dois estudos de caso de interesse bastante pratico: a verificacao de propriedades de um sistema de manufatura originalmente modelado atraves de uma rede de Petri e a verificacao de propriedades do intertravamento de uma seção metroviaria. Os dois estudos de caso utilizam tecnicas denominadas simbolicas. No primeiro estudo de caso, propoe-se que as invariantes obtidas da equação de estado sejam acrescentadas ao modelo a ser verificado, o que permite a obtenção de ganhos de desempenho na verificacao. O segundo estudo de caso e resolvido a partir da utilizacao de um procedimento proposto nesta dissertacao. Este procedimento permite a verificacao de algumas propriedades de seguranca sem que a verificacao se inviabilize devido a explosao no numero de estados. A utilizacao deste procedimento permite a verificacao de propriedades de uma secao de intertravamento com cerca de 2000 variaveis digitais em questao de poucos segundos.A principal conclusao a que este trabalho chega e consequencia dos resultados positivos observados nos estudos de caso: o model checking simbólico parece possuir um amplo campo de aplicacoes ainda por ser mais bem explorado / This work is the result of the efforts oriented to the study of the main automatic verification techniques for systems that can be modeled as Finite State Machines, in particular of those techniques which are generally called as model checking. In order to make the reader able to understand the pros and cons of each technique, the theory associated to each one is presented, as well as some examples. This work also presents two case studies of practical interest, both of each were solved with techniques which are called symbolic. The first one is the verification of some properties of a manufacturing system originally modeled by a Petri net. In order to improve the verification performance, it is proposed that the model to be verified be enlarged with the inclusion of the invariants calculated with the help of the state equation. The second case study is the verification of some safety properties of an interlocking system of a subway section. The verification is carried out with the help of a procedure which is proposed in this work. The aim of such a procedure is to bypass the state explosion problem, in order to make the verification feasible. It was possible to verify an interlocking system with about 2000 digital variables in a matter of few seconds. The main conclusion of the work comes from the positive results reached by both case studies: it seems to be a large number of applications yet to be explored in which symbolic model checking may be considered.

La conception d'algorithmes pour les systèmes concurrents et répartis est subtile et difficile. Ces systèmes sont enclins à des blocages et à des conditions de course et sont par conséquent difficiles à reproduire La vérification formelle est une technique essentielle pour modéliser le système et ses propriétés et s'assurer de sa correction au moyen du model checking. Des langages formels tels TLA+ permettent de décrire des algorithmes compliqués de manière assez concise, mais les concepteurs d'algorithmes trouvent souvent difficile de modéliser un algorithme par un ensemble de formules. Dans ce mémoire nous présentons le langage PlusCal-2 qui vise à allier la simplicité de pseudo-code à la capacité d'être vérifié formellement. PlusCal-2 améliore le langage algorithmique PlusCal conçu par Lamport en levant certaines restrictions de ce langage et en y ajoutant de nouvelles constructions. Notre langage est destiné à la description d'algorithmes à un niveau élevé d'abstraction. Sa syntaxe ressemble à du pseudo-code mais il est tout à fait expressif et doté d'une sémantique formelle. Pour calculer la dépendance conditionnelle pour les algorithmes en PlusCal-2 nous exploitons des informations sur la localité des actions et nous générons des prédicats d'indépendance. Nous proposons également une adaptation d'un algorithme de réduction par ordre partiel dynamique pour une variante du model checker TLC. Enfin, nous proposons une variante d'un algorithme de réduction par ordre partiel statique s'appuyant sur une relation de dépendance constante, et son implantation au sein de TLC. Nous présentons nos résultats expérimentaux et une preuve de correction / Designing sound algorithms for concurrent and distributed systems is subtle and challenging. These systems are prone to deadlocks and race conditions, and are therefore hard to reproduce. Formal verification is a key technique to model the system and its properties and then perform verification by means of model checking. Formal languages like TLA+ have the ability to describe complicated algorithms quite concisely, but algorithm designers often find it difficult to model an algorithm in the form of formulas. In this thesis, we present PlusCal-2 that aims at being similar to pseudo-code while being formally verifiable. PlusCal-2 improves upon Lamport?s PlusCal algorithm language by lifting some of its restrictions and adding new constructs. Our language is intended for describing algorithms at a high level of abstraction. Finite instances of algorithms described in PlusCal-2 can be verified through the TLC model checker. The second contribution presented in this thesis is a study of partial-order reduction methods using conditional and constant dependency relation. To compute conditional dependency for PlusCal-2 algorithms, we exploit their locality information and present them in the form of independence predicates. We also propose an adaptation of a dynamic partial-order reduction algorithm for a variant of the tlc model checker. As an alternative to partial order reduction based on conditional dependency, we also describe a variant of a static partial-order reduction algorithm for the tlc model checker that relies on constant dependency relation. We also present our results for the experiments along with the proof of correctness

Alors que l'informatique est devenue omniprésente dans notre société actuelle, assurer la qualité d'un logiciel revêt une importance grandissante. Pour accroître cette qualité, l'une des conditions à respecter est la correction du système. Dans cette thèse, nous nous intéressons plus particulièrement aux systèmes distribués mettant en œuvre un ou plusieurs programmes exécutés sur plusieurs machines qui communiquent entre elles à travers le réseau. Dans ce contexte, assurer leur correction est rendu plus difficile par leur hétérogénéité mais également par leurs spécificités communes. Les algorithmes correspondants sont parfois complexes et la prédiction de leur comportement difficilement réalisable sans une étude avancée. Les travaux réalisés au cours de cette thèse mettent en œuvre la vérification dynamique formelle de propriétés temporelles sur des applications distribuées. Cette approche consiste à vérifier l'implémentation réelle d'une application à travers son exécution. L'enjeu majeur est de réussir à appliquer les techniques associées au Model checking dans le cadre d'une vérification sur des implémentations réelles d'applications distribuées et non plus sur des modèles abstraits. Pour cela, nous proposons dans un premier temps une analyse sémantique dynamique par introspection mémoire d'un état système permettant de détecter des états sémantiquement identiques. Puis, nous mettons en œuvre la vérification dynamique formelle de certaines propriétés temporelles : les propriétés de vivacité, formulées à l'aide de la logique LTL_X, et le déterminisme des communications dans les applications MPI. Une évaluation de chacune de ces contributions est réalisée à travers plusieurs expériences / While computers have become ubiquitous in our current society, ensuring the software quality takes on an increasing importance. One of the requirements to enhance this quality is the system correctness. In this thesis, we are particularly interested in distributed systems implementing one or more programs executed on several machines which communicate with each other through a network. Ensuring the system correctness is more difficult in this context, due to their heterogeneity but also their common characteristics. Corresponding algorithms are sometimes complex and the prediction of their behavior may be difficult to realize without an advanced study. The work done during this thesis implement the dynamic formal verification of some temporal properties on legacy distributed applications. This approach consists of checking the real implementation of an application by its systematic execution. The challenge in this approach is how to apply the methods derived from Model checking in the context of the verification of legacy distributed applications (without access to source code) and no longer on abstract models. For that, we propose in a first step a dynamic semantic analysis of a system state permitting the detection of identical states. Then, we implement the dynamic formal verification of some temporal properties: liveness properties, specified with the LTL_X logic, and the communications determinism in MPI applications. These contributions are experimentaly validated and evaluated with different series of experiments

Notre propos est la conception assistée par ordinateur des scénarios comprenant des contenus multimédia qui interagissent avec les actions extérieures, notamment celles de l’interprète (e.g., spectacles vivants, installations muséales interactives et jeux vidéo). Le contenu multimédia est structuré dans un ordre spatial et temporel selon les exigences de l’auteur. Par conséquent, la complexité potentiellement élevée de ces scénarios nécessite des langages de spécification adéquats pour leur complète description et vérification.Partitions Interactives est un formalisme qui a été proposé comme un modèle pour la composition et l’exécution des scénarios multimédias interactifs. En outre, un séquenceur inter-médias, appelé ISCORE,a été élaboré à partir de la sémantique Petri net proposée par ce formalisme. Au cours des dernières années, I-SCORE a été utilisé avec succès pour la composition et l’exécution des spectacles et des expositions interactives. Néanmoins, ces applications et les applications émergentes telles queles jeux vidéo et les installations muséales interactives, de plus en plus exigent deux caractéristiques que la version stable actuelle de I-SCORE ainsi que son modèle sous-jacent ne supportent pas : (1)des structures de contrôle flexibles comme des conditionnelles et des boucles ; et (2) des mécanismes pour la vérification automatique de scénarios.Dans cette thèse, nous présentons deux modèles formels pour la composition et la vérification automatique de scénarios interactifs multimédia avec des choix interactifs, i.e., des scénarios où l’interprète ou le système peut prendre des décisions au sujet de leur état d’exécution avec un certain degré de liberté définie par le compositeur.Dans notre première approche, nous définissons un nouveau langage de programmation appelé REACTIVEIS dont les programmes sont définis comme des arbres représentant l’aspect hiérarchique des scénarios interactifs et dont les noeuds contiennent les conditions nécessaires pour démarrer et arrêter les objets temporels (TOS). En outre, nous définissons une sémantique opérationnelle basé sur des arbres marqués, contenant dans leurs noeuds, les informations sur le début et la fin de chaque TO. Nous définissons également une interprétation déclarative de REACTIVEIS comme formules de la logique linéaire intuitionniste avec sous exponentiels (SELL). Nous montrons que cette interprétation est adéquate : les dérivations dans la logique correspondent à des traces du programme et vice-versa.Dans notre deuxième approche, nous présentons un système basé sur des Automates Temporisés.Dans le système proposé, nous modélisons des scénarios interactifs comme un réseau d’automates temporisés et les étendons avec des points interactifs gardés par des conditions, permettant ainsi la spécification de comportements avec branchements. Par ailleurs, nous profitons des outils matures et efficaces pour simuler et vérifier automatiquement des scénarios modélisés comme des automates temporisés. Dans notre système, les scénarios peuvent être synthétisés dans un matériel reconfigurable afin de fournir une faible latence et l’exécution en temps réel.Dans cette thèse, nous explorons également une nouvelle façon de définir et mettre en oeuvre des scénarios interactifs, visant à un modèle plus dynamique en utilisant le langage réactif REACTIVEML.Enfin, nous présentons une extension des scénarios interactifs utilisant des réseaux de Petri colorés(CPN) qui vise à traiter des données complexes, en particulier, les données statiques et dynamiques de flux audio. / Interactive multimedia deals with the computer-based design of scenarios consisting of multimediacontent that interacts with external actions and those of the performer (e.g., multimedialive-performance arts, interactive museum installations, and video games). The multimedia content is structured in a spatial and temporal order according to the author’s requirements. Therefore, thepotentially high complexity of these scenarios requires adequate specification languages for theircomplete description and verification.Interactive scores is a formalism which has been proposed as a model for composing and performing interactive multimedia scenarios. In addition, an inter-media sequencer, called I-SCORE, hasbeen developed following the Petri Net semantics proposed by this formalism. During the last years,I-SCORE has been used successfully for the composition and performance of live performances and interactive exhibitions. Nevertheless, these applications and emergent applications such as videogames and interactive museum installations, increasingly demand two features that the current stable version of I-SCORE as well as its underlying model do not support: (1) flexible control structures such as conditionals and loops; and (2) mechanisms for the automatic verification of scenarios.In this dissertation we present two formal models for composition and automatic verification of multimedia interactive scenarios with interactive choices, i.e., scenarios where the performer or thesystem can take decisions about their execution state with a certain degree of freedom defined bythe composer.In our first approach, we define a novel programming language called REACTIVEIS. This language extends the full capacity of temporal organization of interactive scenarios by allowing the composerto use a defined logical system for the specification of the starting and stopping conditions of temporal objects (TOs). REACTIVEIS programs are formally defined as tree-like structures representing the hierarchical aspect of interactive scenarios and whose nodes contain the conditions needed to startand stop the TOs. Moreover, we define an operational semantics based on labeled trees, containing in their nodes, the information about the start and stop times of each TO.We show that this operational semantics offers an intuitive yet precise description of the behavior of interactive scenarios.We also endowed REACTIVEIS with a declarative interpretation as formulas in Intuitionistic LinearLogic with Subexponentials (SELL). We shall show that such interpretation is adequate: derivations in the logic correspond to traces of the program and vice-versa. Hence, we can use all the meta-theory of Intuitionistic Linear Logic (ILL) to reason about interactive scenarios and develop tools for theverification and analysis of interactive scenarios.In our second approach, we present a Timed Automata (TA) based framework. In the proposed framework, we model interactive scenarios as a network of timed automata and extend them with interactive points (IPs) guarded by conditions, thus allowing for the specification of branching behaviors.Moreover, we take advantage of the mature and efficient tools for TA to simulate and automatically verify scenarios. In our framework, scenarios can be synthesized into a reconfigurable hardware in order to provide a low-latency and real-time execution by taking advantage of the physical parallelism,low-latency, and high-reliability of these devices. Furthermore, we implemented a tool to systematically construct bottom-up TA models from the composition environment of I-SCORE. Doing that, we provide a friendly and specialized environment for composing and automatic verification of interactive scenarios. Finally, we present an extension of interactive scenarios using Colored Petri Nets (CPNs) thataims to handle complex data, in particular, dynamic and static data audio streams. [...]

De manière générale, en informatique, les vulnérabilités logicielles sont définies comme des cas particuliers de fonctionnements non attendus du système menant à la dégradation des propriétés de sécurité ou à la violation de la politique de sécurité. Ces vulnérabilités peuvent être exploitées par des utilisateurs malveillants comme brèches de sécurité. Comme la documentation sur les vulnérabilités n'est pas toujours disponible pour les développeurs et que les outils qu'ils utilisent ne leur permettent pas de les détecter et les éviter, l'industrie du logiciel continue à être paralysée par des failles de sécurité. Nos travaux de recherche s'inscrivent dans le cadre du projet Européen SHIELDS et portent sur les techniques de modélisation et de détection formelles de vulnérabilités. Dans ce domaine, les approches existantes sont peu nombreuses et ne se basent pas toujours sur une modélisation formelle précise des vulnérabilités qu'elles traitent. De plus, les outils de détection sous-jacents produisent un nombre conséquent de faux positifs/négatifs. Notons également qu'il est assez difficile pour un développeur de savoir quelles vulnérabilités sont détectées par chaque outil vu que ces derniers sont très peu documentés. En résumé, les contributions réalisées dans le cadre de cette thèse sont les suivantes: Définition d'un formalisme tabulaire de description de vulnérabilités appelé template. Définition d'un langage formel, appelé Condition de Détection de Vulnérabilité (VDC). Une approche de génération de VDCs à partir des templates. Définition d'une approche de détection de vulnérabilités combinant le model checking et l'injection de fautes. Évaluation des deux approches / In general, computer software vulnerabilities are defined as special cases where an unexpected behavior of the system leads to the degradation of security properties or the violation of security policies. These vulnerabilities can be exploited by malicious users or systems impacting the security and/or operation of the attacked system. Since the literature on vulnerabilities is not always available to developers and the used tools do not allow detecting and avoiding them; the software industry continues to be affected by security breaches. Therefore, the detection of vulnerabilities in software has become a major concern and research area. Our research was done under the scope of the SHIELDS European project and focuses specifically on modeling techniques and formal detection of vulnerabilities. In this area, existing approaches are limited and do not always rely on a precise formal modeling of the vulnerabilities they target. Additionally detection tools produce a significant number of false positives/negatives. Note also that it is quite difficult for a developer to know what vulnerabilities are detected by each tool because they are not well documented. Under this context the contributions made in this thesis are: Definition of a formalism called template. Definition of a formal language, called Vulnerability Detection Condition (VDC), which can accurately model the occurrence of a vulnerability. Also a method to generate VDCs from templates has been defined. Defining a second approach for detecting vulnerabilities which combines model checking and fault injection techniques. Experiments on both approaches

Le développement de circuits électroniques et de systèmes logiciels critiques pour le ferroviaire ou l’avionique, par exemple, demande à être systématiquement associé à un processus de vérification formelle permettant de garantir l’exhaustivité des tests. L’approche formelle la plus répandue dans l’industrie est le Model Checking. Le succès de son adoption provient de deux caractéristiques : (i) son aspect automatique, (ii) sa capacité à produire un témoin (un scénario rejouable) lorsqu’un comportement indésirable est détecté, ce qui fournit une grande aide aux concepteurs pour corriger le problème. Néanmoins, la complexité grandissante des systèmes à vérifier est un réel défi pour le passage à l’échelle des techniques existantes. Pour y remédier, différents algorithmes de model checking (e.g., parcours symbolique des états du système, interpolation), diverses méthodes complémentaires (e.g., abstraction,génération automatique d’invariants), et de multiples procédures de décision(e.g., diagramme de décision, solveur SMT) sont envisageables.Dans cette thèse, nous nous intéressons plus particulièrement à l’induction temporelle.Il s’agit d’un algorithme de model checking très utilisé dans l’industrie pour vérifier les systèmes critiques. C’est également l’algorithme principal de l’outil développé au sein de l’entreprise Safe River, entreprise dans laquelle cette thèse a été effectuée. Plus précisément, l’induction temporelle combine deux techniques :(i) BMC (Bounded Model Checking), une méthode très efficace pour la détection debugs dans un système (ii) k-induction, une méthode ajoutant un critère de terminaison à BMC lorsque le système n’admet pas de bug. Ces deux techniques génèrent des formules logiques propositionnelles pour lesquelles il faut en déterminer la satisfaisabilité.Pour se faire, nous utilisons un solveur SAT, c’est-à-dire une procédure de décision qui détermine si une telle formule admet une solution.L’originalité des travaux proposés dans cette thèse repose en grande partie sur la volonté de renforcer la collaboration entre le solveur SAT et le model checker.Nos efforts visent à accroître l’interconnexion de ces deux modules en exploitant la structure haut niveau du problème. Nous avons alors défini des méthodes profitant de la structure symétrique des formules. Cette structure apparaît lors du dépliage successif de la relation de transition, et nous permet de dupliquer les clauses ou encore de déplier les transitions dans différentes directions (i.e., avant ou arrière). Nous avons aussi pu instaurer une communication entre le solveur SAT et le model checker permettant de : (i) simplifier la représentation au niveau du model checker grâce à des informations déduites par le solveur, et (ii) aider le solveur lors de la résolution grâce aux simplifications effectuées sur la représentation haut niveau. Une autre contribution importante de cette thèse est l’expérimentation des algorithmes proposées. Cela se concrétise par l’implémentation d’un model checker prenant en entrée des modèles AIG (And-Inverter Graph) dans lequel nous avons pu évaluer l’efficacité de nos différentes méthodes. / The design of electronic circuits and safety-critical software systems in railway or avionic domains for instance, is usually associated with a formal verification process. More precisely, test methods for which it is hard to show completeness are combined with approaches that are complete by definition. Model Checking is one of those approaches and is probably the most prevalent in industry. Reasons of its success are mainly due to two characteristics, namely: (i) its fully automatic aspect, and (ii) its ability to produce a short execution trace of undesired behaviors, which is very helpful for designers to fix the issues. However, the increasing complexity of systems to be verified is a real challenge for the scalability of existing techniques. To tackle this challenge, different model checking algorithms (e.g., symbolic model checking, interpolation), various complementary methods (e.g., abstraction, automatic generation of invariants) and multiple decision procedures (e.g., decision diagram, SMT solver) can be considered. In this thesis, we particularly focus on temporal induction. It is a model checking algorithm widely used in the industry to check safety-critical systems. This is also the core algorithm of the tool developed within SafeRiver, company in which this thesis was carried out. More precisely, temporal induction consists of a combination of BMC (Bounded Model Checking) and k-induction. BMC is a very efficient bugfinding method. While k-induction adds a termination criterion to BMC when the system does not admit bugs. These two techniques generate formulas for which it is necessary to determine their satisfiability. To this end, we use a SAT solver as a decision procedure to determine whether a propositional formula has a solution. The main contribution of this thesis aims to strengthen the collaboration between the SAT solver and the model checker. The improvements proposed mainly focus on increasing the interconnections of these two modules by exploiting the high-level structure of the problem.We have therefore defined several methods taking advantage of the symmetrical structure of the formulas. This structure emerges during the successive unfolding of the transition relation, and allows us to duplicate clauses or even unroll the transitions in different directions (i.e., forward or backward). We also established a communication between the solver and the model checker, which has for purpose to: (i) simplify the model checker representation using the information inferred by the solver, and (ii) assist the solver during resolution with simplifications performed on the high-level representation. Another important contribution of this thesis is the empirical evaluation of the proposed algorithms on well-established benchmarks. This is achieved concretely via the implementation of a model checker taking AIG (And-Inverter Graph) as input, from which we were able to evaluate the effectiveness of our algorithms.

Les techniques formelles de la famille « vérification de modèles » (« model checking ») se heurtent au problème de l’explosion combinatoire. Ceci limite les perspectives d’exploitation dans des projets industriels. Ce problème est provoqué par la combinatoire dans la construction de l’espace des états possibles durant l’exécution des systèmes modélisés. Le nombre d’états pour des modèles de systèmes industriels réalistes dépasse régulièrement les capacités des ressources disponibles en calcul et stockage. Cette thèse défend l’idée qu’il est possible de réduire cette combinatoire en spécialisant les outils pour des familles de propriétés. Elle propose puis valide expérimentalement un ensemble de méthodes pour le développement de ce type d’outils en suivant une approche guidée par les propriétés appliquée au contexte temps réel. Il s’agit donc de construire des outils d’analyse performants pour des propriétés temps réel qui soient exploitables pour des modèles industriels de taille réaliste. Les langages considérés sont, d’une part UML étendu par le profil MARTE pour la modélisation par les utilisateurs, et d’autre part les réseaux de Petri temporisés comme support pour la vérification. Les propositions sont validées sur un cas d’étude industriel réaliste issu du monde avionique : l’étude de la latence et la fraicheur des données dans un système de gestion des alarmes exploitant les technologies d’Avionique Modulaire Intégrée. Ces propositions ont été mise en oeuvre comme une boite à outils qui intègre les cinq contributions suivantes: la définition de la sémantique d’exécution spécifiques aux propriétés temps réel pour les modèles d’architecture et de comportement spécifiés en UML/MARTE; la spécification des exigences temps réel en s’appuyant sur un ensemble de patrons de vérification atomiques dédiés aux propriété temps réel; une méthode itérative d’analyse à base d’observateurs pour des réseaux de Petri temporisés; des techniques de réduction de l’espace d’états spécifiques aux propriétés temps réel pour des Réseaux de Petri temporisés; une approche pour l’analyse des erreurs détectées par « vérification des modèles » en s’appuyant sur des idées inspirées de la « fouille de données » (« data mining »). / Automatic formal verification such as model checking faces the combinatorial explosion issue. This limits its application in indus- trial projects. This issue is caused by the explosion of the number of states during system’s execution , as it may easily exceed the amount of available computing or storage resources. This thesis designs and experiments a set of methods for the development of scalable verification based on the property-driven approach. We propose efficient approaches based on model checking to verify real-time requirements expressed in large scale UML-MARTE real-time system designs. We rely on the UML and its profile MARTE as the end-user modeling language, and on the Time Petri Net (TPN) as the verification language. The main contribution of this thesis is the design and implementation of a property-driven verification prototype toolset dedicated to real-time properties verification for UML-MARTE real-time software designs. We validate this toolset using an avionic use case and its user requirements. The whole prototype toolset includes five contributions: definition of real-time property specific execution semantics for UML-MARTE architecture and behavior models; specification of real- time requirements relying on a set of verification dedicated atomic real- time property patterns; real-time property specific observer-based model checking approach in TPN; real-time property specific state space reduction approach for TPN; and fault localization approach in model checking.

Les systèmes temps réel (STR) sont au coeur de machines souvent jugés critiques pour lasécurité : ils en contrôlent l’exécution afin que celles-ci se comportent de manière sûre dans le contexte d’un environnement dont l’évolution peut être imprévisible. Un STR n’a d’autre alternative que de s’adapter à son environnement : sa correction dépend des temps de réponses aux stimuli de ce dernier.Il est couramment admis que le formalisme des réseaux de Petri temporels (RdPT) est adapté àla description des STR. Cependant, la modélisation de systèmes simples, ne possédant que quelquestˆaches périodiques ordonnancées de façon basique se révèle être un exercice souvent complexe.En premier lieu, la modélisation efficace d’une gamme étendue de politiques d’ordonnancementsse heurte à l’incapacité des RdPT à imposer un ordre d’apparition à des évènements concurrentssurvenant au même instant. D’autre part, les STR ont une nette tendance à être constitués de caractéristiques récurrentes, autorisant une modélisation par composants. Or les RdPT ne sont guèreadaptés à une utilisation compositionnelle un tant soit peu générale. Afin de résoudre ces deuxproblèmes, nous proposons dans cette thèse Cifre – en partenariat entre Airbus et le Laas-Cnrs– d’étendre les RdPT à l’aide de deux nouvelles relations, les relations d’inhibition et de permission,permettant de spécifier de manière plus fine les contraintes de temps.Afin de cerner un périmètre clair d’adéquation de cette nouvelle extension à la modélisation dessystèmes temps réel, nous avons défini Pola, un langage spécifique poursuivant deux objectifs :déterminer un sous-ensemble des systèmes temps réel modélisables par les réseaux de Petri temporelsà inhibitions/permissions et fournir un langage simple à la communauté temps réel dont lavérification, idéalement automatique, est assurée par construction. Sa sémantique est donnée par traduction en réseaux de Petri temporels à inhibitions/permissions. L’explorateur d’espace d’états de laboite à outils Tina a été étendu afin de permettre la vérification des descriptions Pola / Real time systems (RTS) are at the core of safety critical devices : they control thedevices’ behavior in such a way that they remain safe with regard to an unpredictable environment. ARTS has no other choices than to adapt to its environment : its correctness depends upon its responsetime to the stimuli stemming from the environment.It is widely accepted that the Time Petri nets (TPN) formalism is adapted to the description ofRTS. However, the modeling of simple systems with only a few periodic tasks scheduled according toa basic policy remains a challenge in the worst case and can be very tedious in the most favorable one.First, we put forward some limitations of TPN regarding the modeling of a wide variety of schedulingpolicies, coming from the fact that this formalism is not always capable to impose a givenorder on events whenever they happen at the same time. Moreover, RTS are usually constituted of thesame recurring features, implying a compositional modeling, but TPN are not well adapted to sucha compositional use. To solve those problems we propose in this Cifre thesis – in partnership withAirbus and the Laas-Cnrs – to extend the formalism with two new dual relations, the forbid andallow relations so that time constraints can be finely tuned.Then, to assess this new extension for modeling of real time systems, we define Pola, a specificlanguage aimed at two goals : to determine a subset of RTS which can be modeled with forbid/allowtime Petri nets and to provide a simple language to the real time community which, ideally, can bechecked automatically. Its semantics is given by translation into forbid/allow Time Petri nets. Thestate space exploration tool of the Tina toolbox have been extended so that it can model check Poladescriptions.