Un des défis majeurs pour le développement des Systèmes Multi-Agents (SMA) auto-organisateurs est de garantir la convergence du système vers la fonction globale attendue par un observateur externe et de garantir que les agents sont capables de s'adapter face aux perturbations. Dans la littérature, plusieurs travaux se sont basés sur la simulation et le model-checking pour analyser les SMA auto-organisateurs. La simulation permet aux concepteurs d'expérimenter plusieurs paramètres et de créer certaines heuristiques pour faciliter la conception du système. Le model-checking fournit un support pour découvrir les blocages et les violations de propriétés. Cependant, pour faire face à la complexité de la conception des SMA auto-organisateurs, le concepteur a également besoin de techniques qui prennent en charge non seulement la vérification, mais aussi le processus de développement lui-même. En outre, ces techniques doivent permettre un développement méthodique et faciliter le raisonnement sur divers aspects du comportement du système à différents niveaux d'abstraction. Dans cette thèse, trois contributions essentielles ont été apportées dans le cadre du développement et la vérification formelle des SMA auto-organisateurs: une formalisation à l'aide du langage B-événementiel des concepts clés de ces systèmes en trois niveaux d'abstraction (micro, méso et macro), une expérimentation d'une stratégie de raffinement descendante pour le développement des SMA auto-organisateurs et la proposition d'un processus de raffinement ascendant basé sur des patrons de raffinement. / A major challenge for the development of self-organizing MAS is to guarantee the convergence of the system to the overall function expected by an external observer and to ensure that agents are able to adapt to changes. In the literature, several works were based on simulation and model-checking to study self-organizing MAS. The simulation allows designers to experiment various settings and create some heuristics to facilitate the system design. Model checking provides support to discover deadlocks and properties violations. However, to cope with the complexity of self-organizing MAS, the designer also needs techniques that support not only verification, but also the development process itself. Moreover, such techniques should support disciplined development and facilitate reasoning about various aspects of the system behavior at different levels of abstraction. In this thesis, three essential contributions were made in the field of formal development and verification of self-organizing MAS: a formalization with the Event-B language of self-organizing MAS key concepts into three levels of abstraction, an experimentation of a top-down refinement strategy for the development of self-organizing MAS and the definition of a bottom-up refinement process based on refinement patterns.

Recently, verification and analysis of data words have gained a lot of interest. Metric temporal logic (MTL) and timed propositional temporal logic (TPTL) are two extensions of Linear time temporal logic (LTL). In MTL, the temporal operator are indexed by a constraint interval. TPTL is a more powerful logic that is equipped with a freeze formalism. It uses register variables, which can be set to the current data value and later these register variables can be compared with the current data value. For monotonic data words, Alur and Henzinger proved that MTL and TPTL are equally expressive and the satisfiability problem is decidable. We study the expressive power, satisfiability problems and path checking problems for MLT and TPTL over all data words. We introduce Ehrenfeucht-Fraisse games for MTL and TPTL. Using the EF-game for MTL, we show that TPTL is strictly more expressive than MTL. Furthermore, we show that the MTL definability problem that whether a TPTL-formula is definable in MTL is not decidable. When restricting the number of register variables, we are able to show that TPTL with two register variables is strictly more expressive than TPTL with one register variable. For the satisfiability problem, we show that for MTL, the unary fragment of MTL and the pure fragment of MTL, SAT is not decidable. We prove the undecidability by reductions from the recurrent state problem and halting problem of two-counter machines. For the positive fragments of MTL and TPTL, we show that a positive formula is satisfiable if and only it is satisfied by a finite data word. Finitary SAT and infinitary SAT coincide for positive MTL and positive TPTL. Both of them are r.e.-complete. For existential TPTL and existential MTL, we show that SAT is NP-complete. We also investigate the complexity of path checking problems for TPTL and MTL over data words. These data words can be either finite or infinite periodic. For periodic words without data values, the complexity of LTL model checking belongs to the class AC^1(LogDCFL). For finite monotonic data words, the same complexity bound has been shown for MTL by Bundala and Ouaknine. We show that path checking for TPTL is PSPACE-complete, and for MTL is P-complete. If the number of register variables allowed is restricted, we obtain path checking for TPTL with only one register variable is P-complete over both infinite and finite data words; for TPTL with two register variables is PSPACE-complete over infinite data words. If the encoding of constraint numbers of the input TPTL-formula is in unary notation, we show that path checking for TPTL with a constant number of variables is P-complete over infinite unary encoded data words. Since the infinite data word produced by a deterministic one-counter machine is periodic, we can transfer all complexity results for the infinite periodic case to model checking over deterministic one-counter machines.

Many software systems eventually undergo changes to their basic architectural structure. Such changes may be prompted by new feature requests, new quality attribute requirements, changing technology, or other reasons. Whatever the causes, architecture evolution is commonplace in real-world software projects. Today’s software architects, however, have few techniques to help them plan such evolution. In particular, they have little assistance in planning alternatives, making trade-offs among these different alternatives, or applying best practices for particular domains. To address this, we have developed an approach for assisting architects in planning and reasoning about software architecture evolution. Our approach is based on modeling and analyzing potential evolution paths that represent different ways of evolving the system. We represent an evolution path as a sequence of transitional architectural states leading from the initial architecture to the target architecture, along with evolution operators that characterize the transitions among these states. We support analysis of evolution paths through the definition and application of constraints that express rules governing the evolution of the systemand evaluation functions that assess path quality. Finally, a set of these modeling elements may be grouped together into an evolution style that encapsulates a body of knowledge relevant to a particular domain of architecture evolution. We evaluate this approach in three ways. First, we evaluate its applicability to real-world architecture evolution projects. This is accomplished through case studies of two very different software organizations. Second, we undertake a formal evaluation of the computational complexity of verifying evolution constraints. Finally, we evaluate the implementability of the approach based on our experiences developing prototype tools for software architecture evolution.

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...

Cette thèse propose un nouveau type de systèmes de ré-écriture, appelé les systèmes de réécriture fonctionnels. Nous montrons que notre modèle a la puissance d'expression des systèmes de ré-écriture et qu'il est bien adapté à l'étude de propriétés de sûreté et de propriétés de logique temporelle de modèles.Nous avons mis en évidence une sous classe de systèmes fonctionnels, les élémentaires et les élémentaires à droite, préservant la puissance d'expression des systèmes fonctionnels et des techniques d'accélération des calculs aboutissant à un outil de vérification symbolique efficace.Dans la partie expérimentale, nous avons comparé notre outil, d'une part avec des outils de ré-écriture tels que Timbuk, Maude et TOM, d'autre part avec des outils de vérification tels que SPIN, NuSMV, SMART, HSDD. Nos benchmarks démontrent l'efficacité des systèmes fonctionnels élémentaires pour la vérification de modèles. / This PhD thesis proposes the theoretical foundations of a new formal tool for symbolic verification of finite models. Some approaches reduce the problem of system verification to the reachability problem in term rewriting systems (TRSs).In our approach, states are encoded by terms in a BDD-like manner and the transition relation is represented by a new rewriting relation so called Functional Term Rewriting Systems (FTRSs).First, we show that FTRSs are as expressive as TRSs. Then, we focus on a subclass of FTRSs, so called Elementary Functional Term Rewriting Systems (EFTRSs), and we show that EFTRSs preserve the FTRSs expressiveness. The main advantage of EFTRSs is that they are well adapted for acceleration techniques usually used in saturation algorithms on BDD-like data structures.Our experiments show that for well-known protocols (e.g. Tree Arbiter, Percolate, Round RobinMutex protocols,... ) our tool is not only better than other rewriting tools such as Timbuk, Maude or TOM, but also competitive with other model-checkers such as SPIN, NuSMV or SMART. Moreover, it can also be applied to model-checking invariant properties which are a particular subclass of linear temporal logic formula (LTL).

Problems in formal verification are often stated in terms of finite automata and extensions thereof. In this thesis we investigate several such algorithmic problems. In the first part of the thesis we develop a theory of completeness thresholds in Bounded Model Checking. A completeness threshold for a given model M and a specification φ is a bound k such that, if no counterexample to φ of length k or less can be found in M, then M in fact satisfies φ. We settle a problem of Kroening et al. [KOS⁺11] in the affirmative, by showing that the linearity problem for both regular and ω-regular specifications (provided as finite automata and Buchi automata respectively) is PSPACE-complete. Moreover, we establish the following dichotomies: for regular specifications, completeness thresholds are either linear or exponential, whereas for ω-regular specifications, completeness thresholds are either linear or at least quadratic in the recurrence diameter of the model under consideration. Given a formula in a temporal logic such as LTL or MTL, a fundamental problem underpinning automata-based model checking is the complexity of evaluating the formula on a given finite word. For LTL, the complexity of this task was recently shown to be in NC [KF09]. In the second part of the thesis we present an NC algorithm for MTL, a quantitative (or metric) extension of LTL, and give an AC¹ algorithm for UTL, the unary fragment of LTL. We then establish a connection between LTL path checking and planar circuits which, among others, implies that the complexity of LTL path checking depends on the Boolean connectives allowed: adding Boolean exclusive or yields a temporal logic with P-complete path-checking problem. In the third part of the thesis we study the decidability of the reachability problem for parametric timed automata. The problem was introduced over 20 years ago by Alur, Henzinger, and Vardi [AHV93]. It is known that for three or more parametric clocks the problem is undecidable. We translate the problem to reachability questions in certain extensions of parametric one-counter machines. By further reducing to satisfiability in Presburger arithmetic with divisibility, we obtain decidability results for several classes of parametric one-counter machines. As a corollary, we show that, in the case of a single parametric clock (with arbitrarily many nonparametric clocks) the reachability problem is NEXP-complete, improving the nonelementary decision procedure of Alur et al. The case of two parametric clocks is open. Here, we show that the reachability is decidable in this case of automata with a single parameter.

La vérification de logiciels est une activité dont l'importance est cruciale pour les logiciels embarqués critiques. Les différentes approches envisageables peuvent être classées en quatre catégories : les méthodes d'analyse statique non formelles, les méthodes d'analyse statique formelles, les méthodes d'analyse dynamique non formelles et les méthodes d'analyse dynamique formelles. L'objectif de cette thèse est de vérifier des propriétés temporelles dans un cadre industriel, par analyse dynamique formelle.La contribution comporte trois parties. Un langage adapté à l'expression des propriétés à vérifier, tirées du contexte industriel d'Airbus, a été dé ni. Il repose notamment sur la logique temporelle linéaire mais également sur un langage d'expressions régulières.La vérification d'une propriété temporelle s'effectue sur une trace d'exécution d'un logiciel, générée à partir d'un cas de test pré-existant. L'analyse statique est utilisée pour générer la trace en fonction des informations nécessaires à la vérification de la propriété temporelle formalisée.Cette approche de vérification propose une solution pragmatique au problème posé par le caractère ni des traces considérées. Des adaptations et des optimisations ont également été mises en œuvre pour améliorer l'efficacité de l'approche et faciliter son utilisation dans un contexte industriel. Deux prototypes ont été implémentés,des expérimentations ont été menées sur différents logiciels d'Airbus. / Software Verification is decisive for embedded software. The different verification approaches can be classified in four categories : non formal static analysis,formal static analysis, non formal dynamic analysis and formal dynamic analysis.The main goal of this thesis is to verify temporal properties on real industrial applications,with the help of formal dynamic analysis.There are three parts for this contribution. A language, which is well adapted to the properties we want to verify in the Airbus context was defined. This language is grounded on linear temporal logic and also on a regular expression language.Verification of a temporal property is done on an execution trace, generated from an existing test case. Generation also depends on required information to verify the formalized property. Static analysis is used to generate the trace depending on the formalized property.The thesis also proposes a pragmatic solution to the end of trace problem. In addition,specific adaptations and optimisations were defined to improve efficiency and user-friendliness and thus allow an industrial use of this approach. Two applications were implemented. Some experiments were led on different Airbus software.

abstract: Cyber-Physical Systems (CPS) are being used in many safety-critical applications. Due to the important role in virtually every aspect of human life, it is crucial to make sure that a CPS works properly before its deployment. However, formal verification of CPS is a computationally hard problem. Therefore, lightweight verification methods such as testing and monitoring of the CPS are considered in the industry. The formal representation of the CPS requirements is a challenging task. In addition, checking the system outputs with respect to requirements is a computationally complex problem. In this dissertation, these problems for the verification of CPS are addressed. The first method provides a formal requirement analysis framework which can find logical issues in the requirements and help engineers to correct the requirements. Also, a method is provided to detect tests which vacuously satisfy the requirement because of the requirement structure. This method is used to improve the test generation framework for CPS. Finally, two runtime verification algorithms are developed for off-line/on-line monitoring with respect to real-time requirements. These monitoring algorithms are computationally efficient, and they can be used in practical applications for monitoring CPS with low runtime overhead. / Dissertation/Thesis / Doctoral Dissertation Computer Science 2017

Correct behavior of programs can be defined by their temporal properties. One of the options for formal specification of such properties is  linear temporal logic - LTL . This master's thesis describes design and implementation of a tool for automatic checking of temporal properties of programs, that are specified using Past-Time LTL formulae. The trace of a given program is analyzed in run-time and any violation of given formulae is reported in details to help to find the code location with a root cause of the bug.

Ontology-based data access (OBDA) augments classical query answering in databases by including domain knowledge provided by an ontology. An ontology captures the terminology of an application domain and describes domain knowledge in a machine-processable way. Formal ontology languages additionally provide semantics to these specifications. Systems for OBDA thus may apply logical reasoning to answer queries; they use the ontological knowledge to infer new information, which is only implicitly given in the data. Moreover, they usually employ the open-world assumption, which means that knowledge not stated explicitly in the data or inferred is neither assumed to be true nor false. Classical OBDA regards the knowledge however only w.r.t. a single moment, which means that information about time is not used for reasoning and hence lost; in particular, the queries generally cannot express temporal aspects. We investigate temporal query languages that allow to access temporal data through classical ontologies. In particular, we study the computational complexity of temporal query answering regarding ontologies written in lightweight description logics, which are known to allow for efficient reasoning in the atemporal setting and are successfully applied in practice. Furthermore, we present a so-called rewritability result for ontology-based temporal query answering, which suggests ways for implementation. Our results may thus guide the choice of a query language for temporal OBDA in data-intensive applications that require fast processing, such as context recognition.