Return to search

From timed models to timed implementations

<p align="justify">Computer Science is currently facing a grand challenge :finding good design practices for embedded systems. Embedded systems are essentially computers interacting with some physical process. You could find one in a braking systems or in a nuclear power plant for example. They present several design difficulties :first they are reactive systems, interacting indefinitely with their environment. Second,they must satisfy real-time constraints specifying when they should respond, and not only how. Finally, their environment is often deeply continuous, presenting complex dynamics. The formal models of choice for specifying such systems are timed and hybrid automata for which model checking is pretty well studied.</p> <p><p align="justify">In a first part of this thesis, we study a complete design approach, including verification and code generation, for timed automata. We have to define a new semantics for timed automata, the AASAP semantics, that preserves the decidability properties for model checking and at the same time is implementable. Our notion of implementability is completely novel, and relies on the simulation of a semantics that is obviously implementable on a real platform. We wrote tools for the analysis and code generation and exemplify them on a case study about the well known Philips Audio Control Protocol.</p> <p><p align="justify">In a second part of this thesis, we study the problem of controller synthesis for an environment specified as a hybrid automaton. We give a new solution for discrete controllers having only an imperfect information about the state of the system. In the process, we defined a new algorithm, based on the monotonicity of the controllable predecessors operator, for efficiently finding a controller and we show some promising applications on a classical problem :the universality test for finite automata. / Doctorat en sciences, Spécialisation Informatique / info:eu-repo/semantics/nonPublished

Identiferoai:union.ndltd.org:ulb.ac.be/oai:dipot.ulb.ac.be:2013/210797
Date20 December 2006
CreatorsDe Wulf, Martin
ContributorsRaskin, Jean-François, Devillers, Raymond, Markey, Nicolas NM, Massart, Thierry, Bruyère, Véronique, Cardinal, Jean, Larsen, Kim G.
PublisherUniversite Libre de Bruxelles, Université libre de Bruxelles, Faculté des Sciences – Informatique, Bruxelles
Source SetsUniversité libre de Bruxelles
LanguageFrench
Detected LanguageEnglish
Typeinfo:eu-repo/semantics/doctoralThesis, info:ulb-repo/semantics/doctoralThesis, info:ulb-repo/semantics/openurl/vlink-dissertation
Format1 v., No full-text files

Page generated in 0.0025 seconds