La vérification et la validation des composants logiciels des systèmes temps réel est un des enjeuxmajeurs pour le développement de systèmes automatisés. Les modèles de tels systèmes doiventêtre vérifiés, et la conformité de leur implémentation par rapport à leur modèle doit être validée. Nous nous plaçons dans le cadre des systèmes récursifs temps réels modélisables par des automates à pile temporisés avec deadlines (TPAIO). Les deadlines imposent des conditions de progression du temps. L’objectif de cette thèse est de proposer des méthodes de génération de tests pour les TPAIO.Nos contributions sont les suivantes. Premièrement, une relation de conformité pour les TPAIO est introduite. Deuxièmement, une méthode polynomiale de génération de tests à partir d’un TPAIO déterministe avec deadline lazy est définie. Elle consiste à définir un algorithme de calcul d’un automate temporisé d’accessibilité incomplet en respectant les contraintes de pile. Cette méthode est incomplète. L’incomplétude n'étant pas un problème car l’activité de test est par essence incomplète. Troisièmement, nous définissons une méthode générant des cas de tests à partir d’un TPAIO déterministe avec sorties seulement et deadline delayable seulement. Elle d’applique aux abstractions de programmes récursifs temporisés. Elle consiste à générer des cas de tests en calculant un testeur sur-approximé. Finalement, nous avons proposé une généralisation du processus de génération de tests à partir d’un TPAIO général avec entrées/sorties et avec deadlines quelconques. La capacité de cette dernière méthode à détecter des implémentations non conformes est évaluée par une technique de mutation. / The verification and validation of software components for real-time systems is a major challenge for the development of automated systems. The models of such systems must be verified and the conformance of their implementation w.r.t their model must be validated. Our framework is that of real-time recursive systems modelled by timed pushdown automata with deadlines (TPAIO). The deadlines impose time progress conditions. The objective of this thesis is to propose test generation methods from TPAIO.Our contributions are as follows. Firstly, a conformance relation for TPAIO is introduced. Secondly, a polynomial method of test generation from a deterministic TPAIO with only lazy deadlines is defined. It consists of defining a polynomial algorithm that computes a partial reachability timed automaton by removing the stack constraints. This method is incomplete. The incompleteness is not a problem because software testing is an incomplete activity by nature. Thirdly, we define a method for generating test cases from a deterministic TPAIO with only outputs and delayable deadlines. It applies to the abstractions of timed recursive programs. It consists of generating test cases by computing an over-approximated tester. Finally, we propose a generalization of the test generation process from a non deterministic TPAIO with any deadlines. Its ability to detect non conform implementation is assessed by a mutation technique.

I have in my thesis produced a start of a multiplayer, voxel, strategy sandbox game with advanced AI. The world is made out of voxels in the form of blocks that both the players and other units can affect and change. In a world where every block follows the laws of physics for both fluids and physics. The game is designed for several players that fights for controll over land and resources. / Jag har i mitt examensarbete producerat en början av ett flerspelar, voxel, strategi och sandlådespel med avancerad AI. Världen är uppbyggd av voxlar i form av block som både spelaren och andra enheter har möjlighet att påverka och förändra. En värld där varje block följer fysiska lagar för både vätska och fysik. Spelet är designat för flera spelare som strider om områden och resurser med hjälp av sina AI kontrollerade bybor.

Cette thèse a pour objectif de proposer une approche formelle basée sur les automates d’interface pour spécifier les contrats des composants réutilisables et vérifier leur interopérabilité fonctionnelle. Cette interopérabilité se traduit par la vérification des trois niveaux : signature, sémantique, et protocole. Le formalisme des automates d’interface est basé sur une approche « optimiste» qui prend en compte les contraintes de l’environnement. Cette approche considère que deux composants sont compatibles s’il existe un environnement convenable avec lequel ils peuvent interagir correctement. Dans un premier temps, nous proposons une approche préliminaire qui intègre la sémantique des paramètres des actions dans la vérification de la compatibilité et de la substitution des composants spécifiés par des automates d’interface. Dans un second temps, nous nous somme intéressés à adapter les composants réutilisables dont les contrats sont décrits par des automates d’interface enrichis par la sémantique des actions. En ce sens, nous avons proposé un algorithme qui permet de générer automatiquement la spécification d’un adaptateur de deux composants lorsque celui-ci existe. Dans un troisième temps, nous avons augmenté le pouvoir d’expression de notre approche proposée pour vérifier l’interopérabilité et les propriétés de sûreté des composants qui communiquent par des variables définies au niveau de leurs contrats d’interface. En particulier, nous étudions la préservation des invariants par composition et par raffinement. / The aim of this thesis is to propose a formal approach based on interface automata to specify the contracts of reusable components and to verify their functional interoperability. The functional interoperability is checked at three levels : signature, semantics, and protocol. Interface automata are based on an « optimistic » approach that takes into account the environment constraints. This approach considers that two components are compatible if there is a suitable environment with which they can interact properly. First, we propose an approach allowing the integration of the semantics of the action parameters in interface automata in order to strengthen the compatibility and substitution check between components. Second, we were interested in adapting reusable components whose contracts are described by interface automata enriched by the action semantics. In this context, we propose an algorithm of automatic generation of an adaptor of two mismatched components if possible. Third, we have increased the expressive power of our proposed approach to verify the interoperability and the safety properties of components that communicate by interface variables defined at the level of their contracts. In particular, we study the preservation of invariants by composition and refinement.

L'objectif principal de cette thèse est de proposer une approche efficace de modélisation et de résolution pour le problème d’ordonnancement, en mettant l’accent sur le partage multi-ressources et sur l’incertitude potentielle d’occurrence de certains événements. L'ordonnancement a pour objectif de réaliser un ensemble de tâches à la fois en respectant des contraintes prédéfinies et en optimisant le temps. Ce travail s’intéresse en particulier à la minimisation du temps total d’exécution. La plupart des approches existantes préconisent une modélisation mathématique exprimant des équations et des contraintes pour décrire et résoudre des problèmes d’ordonnancement. De telles démarches ont une complexité inhérente. Cependant dans l’industrie, la tâche de planification est récurrente et peut requérir des changements fréquents des contraintes. Outre cela, la prise en compte d’événements incertains est peu supportée par les approches existantes; cela peut toutefois augmenter la robustesse d’un ordonnancement. Pour répondre à ces problématiques, après une introduction, le chapitre 2 aborde le problème de l’ordonnancement à travers une démarche de modélisation visuelle, expressive et formelle, s’appuyant sur les automates pondérés et sur la théorie des automates temporisés. L’originalité des modèles proposés réside aussi dans leur capacité de décrire le partage de ressources multiples et proposer une approche de résolution efficace. Ces modèles ont l’avantage d’être directement exploitables par des outils de vérification formelle, à travers une démarche de preuve par contradiction vis-à-vis de l’existence d’une solution. Les résultats effectifs sont obtenus grâce à l’outil UPPAAL. La complexité inhérente à la production d’une solution optimale est abordée à travers un algorithme de recherche et d’amélioration itérative de solutions, offrant une complexité très prometteuse sur la classe de problèmes étudiés. Dans le chapitre 3, une composition synchrone est d’automates pondérés est proposée dans le but de résoudre le problème d’ordonnancement en effectuant une analyse d’atteignabilité optimale directement sur les modèles automates pondérés. Dans le quatrième chapitre, divers comportements incontrôlables tels que le temps de début, la durée de la tâche et l'occurrence d’échec dans un problème d‘ordonnancement sont modélisés par des automates de jeu temporisés. Ensuite, le problème est résolu en effectuant une synthèse de stratégie optimale dans le temps dans l'outil de synthèse TIGA. / The objective of scheduling problems is to find the optimal performing sequence for a set of tasks by respecting predefined constraints and optimizing a cost: time, energy, etc. Despite classical approaches, automata models are expressive and also robust against changes in the parameter setting and against changes in the problem specification. Besides, few studies have used formal verification approaches for addressing scheduling problems; yet none of them considered challenging and practical issues such as multi-resource sharing aspect, uncontrollable environment and reaching the optimal schedule in a reasonable time for industrializing the model. The main objective of this thesis is to propose an efficient modeling and solving approach for the scheduling problem, considering multi-resource sharing and potential uncertainty in occurrence of certain events. For this purpose, after an introduction in Chapter 1, Chapter 2 addresses the problem of scheduling through a visual, expressive and formal modeling approach, based on weighted automata and the theory of timed automata. The originality of the proposed approach lies in ability of handling the sharing of multiple resources and proposing an efficient solving approach. The proposed models have the advantage of being directly exploitable by means of formal verification tools. The results are obtained using the UPPAAL tool. To solve the problem, an algorithm is developed based on iterating reachability analysis to obtain sub-optimal makespan. Results show the proposed model and solving approach provides a very promising complexity on the class of studied problems and can be applied to industrial cases. In Chapter 3, a synchronous composition of weighted automata is proposed to solve the scheduling problem by performing an optimal reachability analysis directly on the weighted automata models. In the fourth chapter, various uncontrollable behaviors such as the start time, the duration of the task and the failure occurrence in a scheduling problem are modeled by timed game automata. Then, the problem is solved by performing an optimal strategy synthesis over time in TIGA as a synthesis tool.

The focus of this thesis is the comparison of languages and the reduction of automata used in network traffic monitoring. In this work, several approaches for approximate (language non-preserving) reduction of automata and comparison of their languages are proposed. The reductions are based on either under-approximating the languages of automata by pruning their states, or over-approximating the language by introducing new self-loops (and pruning redundant states later). The proposed approximate reduction methods and the proposed probabilistic distance utilize information from a network traffic. Formal guarantees with respect to a model of network traffic, represented using a probabilistic automaton are provided. The methods were implemented and evaluated on automata used in network traffic filtering.

Formal verification methods offer a large potential to provide automated software correctness checking (based on sound mathematical roots), which is of vital importance. One such technique is abstract regular model checking, which encodes sets of reachable configurations and one-step transitions between them using finite automata and transducers, respectively. Though this method addresses problems that are undecidable in general, it facilitates termination in many practical cases, while also significantly reducing the state space explosion problem. This is achieved by accelerating the computation of reachability sets using incrementally refinable abstractions, while eliminating spurious counterexamples caused by overapproximation using a counterexample-guided abstraction refinement technique. The aim of this thesis is to create a well designed tool for abstract regular model checking, which has so far only been implemented in prototypes. The new tool will model systems using symbolic automata and transducers instead of their (less concise) classic alternatives.

In this work a novel algorithm for testing language equivalence and inclusion on tree automata is proposed and implemented as a module in the VATA library. First, existing approaches to equivalence and inclusion testing on both word and tree automata are examined. These existing approaches are then modified to create bisimulation up-to congruence algorithm for tree automata and a formal proof of the soundness of the new algorithm is provided. Efficiency of this new approach is compared with existing language equivalence and inclusion testing methods for tree automata, showing the performance of our algorithm on hard cases is often superior.

Vyhledávání regulárních výrazů má ve vývoji softwaru nezastupitelné místo. Rychlost vyhledávání může ovlivnit použitelnost softwaru, a proto je na ni kladen velký důraz. Pro určité druhy regulárních výrazů mají standardní přístupy pro vyhledávání vysokou složitost. Kvůli tomu jsou náchylné k útokům založeným na vysoké náročnosti vyhledávání regulárních výrazů (takzvané ReDoS útoky). Regulární výrazy s omezeným opakováním, které se v praxi často vyskytují, jsou jedním z těchto druhů. Efektivní reprezentace a rychlé vyhledávání těchto regulárních výrazů je možné s použítím automatu s čítači. V této práci představujeme implementaci vyhledávání regulárních výrazů založeném na automatech s čítači v C++. Vyhledávání je implementováno v rámci RE2, rychlé moderní knihovny pro vyhledávání regulárních výrazů. V práci jsme provedli experimenty na v praxi používaných regulárních výrazech. Výsledky experimentů ukázaly, že implementace v rámci nástroje RE2 je rychleší než původní implementace v jazyce C#.

This paper addresses the issue of design and implementation of syntactic analysis based on the context sensitive languages, respectively, grammars that contains constructs, which isn't possible to analyze with the help of the standard parsers based on the context free grammars. More specifically, this paper deals with the possibility of adding context sensitive support to the classic LL-analysis by replacing the standard pushdown automata (PDA) with deep pushdown automata (DP), which were introduced and published by prof. Alexander Meduna.

This work deals with the modification of classical grammar systems with context-free base and defines new, modified linear grammar systems with linear grammar base. Also it deals with modification in automata systems, where each automaton is generative as strong as linear grammar, which is satisfied with the usage of one-turn push-down automata. This thesis also contains view on program realisation of theoretical models, which were described in theoretical part and introduces two programs for syntax analysis built based on it.