UNIVERSITÄTSBIBLIOTHEK

Model-based Design of Embedded Systems by Desynchronization

  • In this thesis we developed a desynchronization design flow in the goal of easing the de- velopment effort of distributed embedded systems. The starting point of this design flow is a network of synchronous components. By transforming this synchronous network into a dataflow process network (DPN), we ensures important properties that are difficult or theoretically impossible to analyze directly on DPNs are preserved by construction. In particular, both deadlock-freeness and buffer boundedness can be preserved after desyn- chronization. For the correctness of desynchronization, we developed a criteria consisting of two properties: a global property that demands the correctness of the synchronous network, as well as a local property that requires the latency-insensitivity of each local synchronous component. As the global property is also a correctness requirement of synchronous systems in general, we take this property as an assumption of our desyn- chronization. However, the local property is in general not satisfied by all synchronous components, and therefore needs to be verified before desynchronization. In this thesis we developed a novel technique for the verification of the local property that can be carried out very efficiently. Finally we developed a model transformation method that translates a set of synchronous guarded actions – an intermediate format for synchronous systems – to an asynchronous actor description language (CAL). Our theorem ensures that one passed the correctness verification, the generated DPN of asynchronous pro- cesses (or actors) preserves the functional behavior of the original synchronous network. Moreover, by the correctness of the synchronous network, our theorem guarantees that the derived DPN is deadlock-free and can be implemented with only finitely bounded buffers.

Volltext Dateien herunterladen

  • _YuBai-Doktorarbeit.pdf
    eng

    Der Zugriff auf den Volltext wurde auf Wunsch des Herausgebers gesperrt, da eine neuere Version dieses Dokumentes existiert. Bitte verwenden Sie den unten in den Metadaten aufgeführten Link zur aktuellen Version.

Metadaten exportieren

Metadaten
Verfasserangaben:Yu Bai
URN (Permalink):urn:nbn:de:hbz:386-kluedo-42618
Betreuer:Klaus Schneider
Dokumentart:Dissertation
Sprache der Veröffentlichung:Englisch
Veröffentlichungsdatum (online):05.01.2016
Jahr der Veröffentlichung:2016
Veröffentlichende Institution:Technische Universität Kaiserslautern
Titel verleihende Institution:Technische Universität Kaiserslautern
Datum der Annahme der Abschlussarbeit:17.12.2015
Datum der Publikation (Server):05.01.2016
Seitenzahl:XVII, 148
Fachbereiche / Organisatorische Einheiten:Fachbereich Informatik
DDC-Sachgruppen:0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik
Lizenz (Deutsch):Standard gemäß KLUEDO-Leitlinien vom 30.07.2015
Neuere Dokument-Versionen:urn:nbn:de:hbz:386-kluedo-43999