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.

Download full text files

  • _YuBai-Doktorarbeit.pdf

    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.

Export metadata

Author:Yu Bai
URN (permanent link):urn:nbn:de:hbz:386-kluedo-42618
Advisor:Klaus Schneider
Document Type:Doctoral Thesis
Language of publication:English
Publication Date:2016/01/05
Year of Publication:2016
Publishing Institute:Technische Universität Kaiserslautern
Granting Institute:Technische Universität Kaiserslautern
Acceptance Date of the Thesis:2015/12/17
Date of the Publication (Server):2016/01/05
Number of page:XVII, 148
Faculties / Organisational entities:Fachbereich Informatik
DDC-Cassification:0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik
Licence (German):Standard gemäß KLUEDO-Leitlinien vom 30.07.2015
Newer document versions:urn:nbn:de:hbz:386-kluedo-43999