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