En la darrera dècada, el disseny de sistemes de supervisió per a processos industrials ha rebut força atenció. Aquest fet s'explica per l'augment de la demanda en prestacions, flexibilitat i seguretat causada per la creixent conscienciació en qüestions de qualitat , legislació ambiental, i productivitat. L'interès principal d'aquesta Tesi es centra en el disseny d'un Sistema de Supervisió Intel·ligent (SIS). La tasca encomanada al SIS és la vigilància del procés, que consisteix en identificar i notificar a l'operador el seu estat de funcionament. Així per exemple, si el SIS detecta un estat de fallada, l'operador podrà emprendre les accions correctores adequades.La originalitat d'aquest treball es basa en la proposta d'una metodologia de disseny basada en la interpretació d'esdeveniments significatius, detectats en els senyals mesurats. En aquesta metodologia, l'expert té un paper rellevant, proporcionant el seu coneixement heurístic del procés. Es proposa una arquitectura de supervisió estructurada en dos nivells: la interfície i el supervisor.La interfície és l'encarregada d'abstraure informació significativa del procés, a partir de l'anàlisi dels senyals mesurats. Per aquest nivell, s'ha formalitzat una metodologia de disseny fonamentada en el paradigma de les finestres lliscants. Una finestra és un conjunt de dades consecutives d'un senyal, caracteritzada per una amplada i un desplaçament. Aplicant un càlcul determinat sobre aquestes dades és possible obtenir una nova dada. Així, l'anàlisi de diverses finestres consecutives proporciona un nou senyal sobre el que es pot aplicar un procediment similar. Continuant aquest procés iteratiu, es pot arribar a abstraure un senyal amb un contingut prou significatiu per a l'expert. Aquesta informació és transmesa al supervisor en forma d'esdeveniments.El supervisor s'encarrega d'interpretar els diversos encadenaments d'esdeveniments observats, i notifica l'estat de funcionament del procés a l'operador. Per aquest nivell, s'ha desenvolupat una metodologia per a l'obtenció d'un model comportamental de la planta, com a màquina d'estats finits. El procediment de modelatge proposat considera la definició de models associats a diversos components del procés i a les interaccions que s'estableixen entre ells. L'autòmat final s'obté per composició de tots aquests models.Ambdós nivells es nodreixen del coneixement heurístic de l'operador: definint els esdeveniments significatius a detectar mitjançant l'anàlisi dels senyals, i associant els encadenaments esperats a estats de funcionament.La metodologia de disseny del SIS ha estat validada satisfactòriament mitjançant l'aplicació a un procés biotecnològic i a una estació de mecanitzat.Diversos resultats d'aquest treball han estat presentats a congressos nacionals i internacionals. / OF THE THESISOver the last decade, the design of supervisory systems for industrial processes has received a great deal of attention. One reason for this is the increased demands on performance, flexibility, and safety caused by increased awareness, environmental regulations, and customer-driven productivity.The main purpose of this Thesis is the design of a Supervisory Intelligent System (SIS). The proposed SIS is concerned with process monitoring, consisting in process functional state identification and its notification to the operator. For example, on faulty state detection, the operator could apply the appropriate corrective action.The originality of this work consists in proposing a design methodology based on the interpretation of significative events, detected from measured signals. In this methodology, heuristic knowledge supplied by operators and experts is very important. A two level supervision architecture is proposed: the interface and the supervisor.The interface deals with abstracting significative process information by means of measured signals data analysis. For this level, a design methodology based on the sliding window paradigm has been formalised. A window is a signal data set, characterised by a duration and a sliding time. Running a specific computation on this data set produces new data. So, the analysis of different consecutive windows leads to a new signal on which a similar procedure can then be applied. Following this iterative process, a signal can be derived which carries enough significative information according to the operator. This information is transmitted to the supervisor as events. The supervisor translates observed event sequences into process states, which later are notified to the operator. For this level, we propose a design methodology that supplies a behavioural plant model by means of a finite state machine description. This procedure is based on modelling process components and interactions between them. The final automaton is obtained by the composition of all these models.Both SIS levels depend on the available operator heuristic knowledge: defining significative events which are to be detected using data analysis, and linking expected event sequences to functional states.The SIS design methodology has been successfully validated through its application to a biotechnological process and a milling machine.Several results in this dissertation have been presented at national and international conferences.

The focus of this thesis is the fast network anomaly detection based on automata learning. It describes and compares several chosen automata learning algorithms including their adaptation for the learning of network characteristics. In this work, various network anomaly detection methods based on learned automata are proposed which can detect sequential as well as statistical anomalies in target communication. For this purpose, they utilize automata's mechanisms, their transformations, and statistical analysis. Proposed detection methods were implemented and evaluated using network traffic of the protocol IEC 60870-5-104 which is commonly used in industrial control systems.

Les systèmes embarqués mobiles font partis intégrante de notre quotidien. Afin de les rendre plus adaptésaux usages, ils ont été miniaturisés et leur autonomie a été augmentée, parfois de façon très considérable.Toutefois, les propositions d’amélioration butent désormais sur les possibilités de la technologie des circuitsintégrés. Pour aller plus loin, il faut donc envisager de repenser la chaîne de traitement du signal afin deréduire la consommation de ces dispositifs. Cette thèse développe une approche originale pour exploiterefficacement l’échantillonnage par traversée de niveaux d’une part et, d’autre part, associe cet échantillonnageà une logique évènementielle afin de réduire drastiquement la consommation d’énergie des systèmesintégrés autonomes. Une méthode de discrétisation adaptée à une application de reconnaissance de signauxphysiologiques, utilisée comme exemple dans cette thèse, y est présentée. Un premier prototype en logiqueévènementielle (asynchrone) sur circuit FPGA a permis de valider cette stratégie et de démontrer les bénéficesde cet échantillonnage dédié en termes de réduction de l’activité par rapport à un échantillonnage uniforme.Un second prototype en logique asynchrone et conçu en technologie CMOS AMS 0.35 μm a permis de validerpar simulation électrique un gain extrêmement important sur la consommation électrique du dispositif. / Our everyday life is highly dependent on mobile embedded systems. In order to make them suitable to differentapplications, they have underwent size reduction and lifetime extension. However, these improvementsare currently limited by the possibilities of the integrated circuits technologies. In order to push back theboundaries, it is necessary to reconsider the whole digital signal processing chain from scratch to sustain thepower consumption reduction in this kind of system. This work develops on the first hand a strategy thatsmartly uses the level-crossing sampling scheme and on the other combines this sampling method with eventlogicto highly reduce the power consumption in mobile embedded systems. A discretisation method adaptedto the recognition of physiological patterns application is described. A first event-logic (asynchronous) prototypeimplemented on FPGA proved the potential benefits that an adapted sampling scheme could offersto reduce activity compared to a uniform sampling scheme. Electrical simulations performed on a secondprototype, also designed in asynchronous logic, with CMOS AMS 0.35 μm technology, validated a high gainin power consumption.

Le concept d’automate, central en théorie des langages, est l’outil d’appréhension naturel et efficace de nombreux problèmes concrets. L’usage intensif des automates finis dans un cadre algorithmique s ’illustre par de nombreux travaux de recherche. La correction et l’ évaluation sont les deux questions fondamentales de l’algorithmique. Une méthode classique d’ évaluation s’appuie sur la génération aléatoire contrôlée d’instances d’entrée. Les travaux d´écrits dans cette thèse s’inscrivent dans ce cadre et plus particulièrement dans le domaine de la génération aléatoire uniforme d’automates finis.L’exposé qui suit propose d’abord la construction d’un générateur aléatoire d’automates à pile déterministes, real time. Cette construction s’appuie sur la méthode symbolique. Des résultats théoriques et une étude expérimentale sont exposés.Un générateur aléatoire d’automates non-déterministes illustre ensuite la souplesse d’utilisation de la méthode de Monte-Carlo par Chaînes de Markov (MCMC) ainsi que la mise en œuvre de l’algorithme de Metropolis - Hastings pour l’ échantillonnage à isomorphisme près. Un résultat sur le temps de mélange est donné dans le cadre général .L’ échantillonnage par méthode MCMC pose le problème de l’évaluation du temps de mélange dans la chaîne. En s’inspirant de travaux antérieurs pour construire un générateur d’automates partiellement ordonnés, on montre comment différents outils statistiques permettent de s’attaquer à ce problème. / The concept of automata, central to language theory, is the natural and efficient tool to apprehendvarious practical problems.The intensive use of finite automata in an algorithmic framework is illustrated by numerous researchworks.The correctness and the evaluation of performance are the two fundamental issues of algorithmics.A classic method to evaluate an algorithm is based on the controlled random generation of inputs.The work described in this thesis lies within this context and more specifically in the field of theuniform random generation of finite automata.The following presentation first proposes to design a deterministic, real time, pushdown automatagenerator. This design builds on the symbolic method. Theoretical results and an experimental studyare given.This design builds on the symbolic method. Theoretical results and an experimental study are given.A random generator of non deterministic automata then illustrates the flexibility of the Markov ChainMonte Carlo methods (MCMC) as well as the implementation of the Metropolis-Hastings algorithm tosample up to isomorphism. A result about the mixing time in the general framework is given.The MCMC sampling methods raise the problem of the mixing time in the chain. By drawing on worksalready completed to design a random generator of partially ordered automata, this work shows howvarious statistical tools can form a basis to address this issue.

The rampant growth of the Internet has been coupled with an equivalent growth in cyber crime over the Internet. With our increased reliance on the Internet for commerce, social networking, information acquisition, and information exchange, intruders have found financial, political, and military motives for their actions. Network Intrusion Detection Systems (NIDSs) intercept the traffic at an organization’s periphery and try to detect intrusion attempts. Signature-based NIDSs compare the packet to a signature database consisting of known attacks and malicious packet fingerprints. The signatures use regular expressions to model these intrusion activities. This thesis presents a memory efficient pattern matching system for the class of regular expressions appearing frequently in the NIDS signatures. Proposed Cascaded Automata Architecture is based on two stage automata. The first stage recognizes the sub-strings and character classes present in the regular expression. The second stage consumes symbol generated by the first stage upon receiving input traffic symbols. The basic idea is to utilize the research done on string matching problem for regular expression pattern matching. We formally model the class of regular expressions mostly found in NIDS signatures. The challenges involved in using string matching algorithms for regular expression matching has been presented. We introduce length-bound transitions, counter-based states, and associated counter arrays in the second stage automata to address these challenges. The system uses length information along with counter arrays to keep track of overlapped sub-strings and character class based transition. We present efficient implementation techniques for counter arrays. The evaluation of the architecture on practical expressions from Snort rule set showed compression in number of states between 50% to 85%. Because of its smaller memory footprint, our solution is suitable for both software based implementations on network chips as well as FPGA based designs.

This thesis introduces syntax-directed translation based on deep pushdown automata. Necessary theoretical models are introduced in the theoretical part. The most important model, introduced in this thesis, is a deep pushdown transducer. The transducer should be used in syntax analysis, significant part of translation. Practical part consists of an implementation of simple-language interpret based on these models.

Cílem této práce je vývoj technik umožňujících praktické využití nedeterministických konečných automatů, zejména nedeterministických stromových automatů. Jde zvláště o techniky pro redukci velikosti a testování jazykové inkluze, jež hrají zásadní roli v mnoha oblastech aplikace konečných automatů. V oblasti redukce velikosti vycházíme z dobře známých metod pro slovní automaty které jsou založeny na relacích simulace.  Navrhli jsme efektivní algoritmy pro výpočet stromových variant simulačních relací a identifikovali jsme nový typ relace založený na kombinaci takzvaných horních a dolních simulací nad stromovými automaty. Tyto kombinované relace jsou zvláště vhodné pro redukci velikosti automatů slučováním stavů. Navržený princip kombinace relací simulace je relevantní i pro slovní automaty.  Náš přínos v oblasti testování jazykové inkluze je dvojí. Nejprve jsme zobecnili na stromové automaty takzvané protiřetězcové algoritmy, které byly původně navrženy pro slovními automaty. Dále se nám podařilo použitím simulačních relací výrazně zefektivnit protiřetězcové algoritmy pro testování jazykové inkluze jak pro slovní, tak pro stromové automaty. Relevanci našich technik pro praxi jsme demonstrovali jejich nasazením v rámci regulárního stromového model checkingu, což je verifikační metoda založená na stromových automatech. Použití našich algoritmů zde vedlo k výraznému zrychlení a zvětšení škálovatelnosti celé metody. Základní myšlenky našich algoritmů pro redukci velikosti automatů a testování jazykové inkluze jsou aplikovatelné i na jiné typy automatů. Příkladem jsou naše redukční techniky pro alternující Büchiho automaty prezentované v poslední části práce.

Tato práce se zaměřuje na konečné automaty nad konečnými slovy a konečnými stromy, a použití těchto automatů při formální verifikaci nekonečně stavových systémů. Práce se nejdříve věnuje rozšíření existujícího přístupu pro verifikaci programů které manipulují s haldou (konkrétně programů s dynamickými datovými strukturami), jenž je založen na stromových automatech. V práci je navrženo několik rozšíření tohoto přístupu, jako například jeho plná automatizace či jeho rozšíření o podporu uspořádaných dat. V práci jsou popsány nové rozhodovací procedury pro dvě logiky, které jsou často používány ve formální verifikaci: pro separační logiku a pro slabou monadickou druhořádovou logiku s následníkem. Obě tyto rozhodovací procedury jsou založeny na převodu jejich problému do automatové domény a následné manipulaci v této cílové doméně. Posledním přínosem této práce je vývoj nových algoritmů k efektivní manipulaci se stromovými automaty, s důrazem na testování inkluze jazyků těchto automatů a manipulaci s automaty s velkými abecedami, a implementace těchto algoritmů v knihovně pro obecné použití. Tyto vyvinuté algoritmy jsou použity jako klíčová technologie, která umožňuje použití výše uvedených technik v praxi.

Tato práce se zabývá vývojem efektivních technik pro konečné automaty a jejich aplikace. Zejména se věnujeme konečným automatům použitých pří detekci útoků v síťovém provozu a automatům v rozhodovacích procedurách a verifikaci. V první části práce navrhujeme techniky přibližné redukce nedeterministických automatů, které snižují spotřebu zdrojů v hardwarově akcelerovaném zkoumání obsahu paketů. Druhá část práce je je věnována automatům v rozhodovacích procedurách, zejména slabé monadické logice druhého řádů k následníků (WSkS) a teorie nad řetězci. Navrhujeme novou rozhodovací proceduru pro WS2S založenou na automatových termech, umožňující efektivně prořezávat stavový prostor. Dále studujeme techniky předzpracování WSkS formulí za účelem snížení velikosti konstruovaných automatů. Automaty jsme také aplikovali v rozhodovací proceduře teorie nad řetězci pro efektivní reprezentaci důkazového stromu. V poslední části práce potom navrhujeme optimalizace rank-based komplementace Buchiho automatů, které snižuje počet generovaných stavů během konstrukce komplementu.

Tato práce se věnuje vylepšení současného stavu formalní analýzy a verifikace založené na automatech a zaměřené na systémy s nekonečnými stavovými prostory. V první části se práce zabývá dvěma rozhodovacími procedurami pro logiku WS1S, které jsou založené na korespondenci mezi formulemi logiky WS1S a konečnými automaty. První metoda je založena na tzv. antiřetězcích, ale, je limitována pouze na formule v prenexním normálním tvaru. Následně je tento přístup zobecněn na libovolné formule, jsou zavedeny tzv. jazykové termy a na jejich základě je navržena nová procedura, která pracuje za běhu a zpracovává tyto termy "líným" způsobem. Abychom získali efektivní rozhodovací proceduru, je dále navržena sada optimalizací (přičemž některé nejsou limitovány pouze pro naše přístupy). Obě metody jsou srovnány s ostatními nástroji implementujícími různé známé rozhodovací procedury. Získané výsledky jsou povzbuzující a ukazují, že použitelnost logiky WS1S je možno rozšířit na širší třídu formulí. V druhé části se práce zabývá analýzou mezí zdrojů programů manipulujících s haldou. Je zde navržena nová třída tzv. tvarových norem založených na délkách cest mezi význačnými místy na haldě, které jsou automaticky odvozovány z analyzovaného programu. Na základě této třídy norem je dále navržen kalkul, který je schopen přesně odvodit změny odvozených normů a použít je k vygenerování odpovídající celočíselné reprezentace vstupního programu, která je následně využita pro následovanou dedikovanou analýzou mezí zdrojů. Tato metoda byla implementována nad analýzou tvaru založenou na tzv. lesních automatech, implementovanou v nástroji Forester, a dále byl použit dobře zavedený analyzátor mezí zdrojů, implementovaný v nástroji Loopus. V experimentální evaluaci bylo ukázáno, že je opravdu takto získán silný analyzátor, který je schopen odvodit meze programů, které ještě nikdy plně automatizovaně odvozené nebyly.