@article {39, title = {State-based scheduling with tree schedules: analysis and evaluation}, journal = {Real-Time Systems}, volume = {48}, year = {2012}, pages = {430 - 462}, abstract = {
Distributed real-time systems require bounded communication delays and achieve them by means of a predictable and verifiable control mechanism for the communication medium. Real-time bus arbitration mechanisms control access to the medium and guarantee bounded communication delays. These arbitration mechanisms can be static dispatch tables or dynamic, algorithmic approaches.
In this work, we introduce a real-time bus arbitration mechanism called tree schedules that takes the best parts of both sides: It can be analyzed like static dispatch tables, and it provides a certain degree of flexibility similar to algorithmic approaches. We present tree schedules as a framework to specify real-time traffic and introduce mechanisms to analyze it. We discuss how tree schedules can capture application-specific behavior in a time-triggered state-based supply model by means of conditional branching built into the model. We present analysis results for this model specifically aiming at schedulability in fixed and dynamic priority schemes and waiting time analysis. Finally, we demonstrate the advantages of state-based supply over stateless supply by means of two case studies.
}, keywords = {network code}, issn = {0922-6443}, doi = {10.1007/s11241-012-9151-3}, author = {Madhukar Anand and Sebastian Fischmeister and Insup Lee and Linh T. X. Phan} } @inproceedings {62, title = {Design Choices for High-Confidence Distributed Real-time Software}, booktitle = {Proc. of the International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA)}, year = {2010}, month = {October}, pages = {327-342}, address = {Heraclion, Crete, Greece}, abstract = {

Safety-critical distributed real-time systems, such as networked medical devices, must operate according to their specification, because incorrect behaviour can have fatal consequences. A system\’s design and architecture influences how difficult it is to provide confidence that the system follows the specification. In this work, we summarize and discuss three design choices and the underlying concepts that aim at increasing predictability and analyzability. We investigate mandatory resource reservation to guarantee resource availability, separation of resource consumptions to better manage resource inter-dependency, and enumerative reconfiguration. We use the example of a distributed monitoring system for the human cardiovascular system to substantiate our arguments.

}, keywords = {network code, safety, state based schedule}, isbn = {3-642-16560-5 978-3-642-16560-3}, doi = {10.1007/978-3-642-16561-0_32}, url = {http://www.springerlink.com/content/414j200175704528/}, author = {Fischmeister, Sebastian and Akramul Azim} } @article {59, title = {Generating Reliable Code from Hybrid-Systems Models}, journal = {IEEE Transactions on Computers}, volume = {59}, year = {2010}, month = {July}, pages = {1281{\textendash}1294}, abstract = {

Hybrid systems have emerged as an appropriate formalism to model embedded systems as they capture the theme of continuous dynamics with discrete control. Under this paradigm, distributed embedded systems can be modeled as a network of communicating hybrid automata. Several techniques for code generation from these models have also been proposed and commercially implemented. Providing formal guarantees of the generated code with respect to the model, however, has turned out to be a hard problem. While the model is set in continuous time with concurrent execution and instantaneous switching, the code running on an inherently discrete platform, can be affected by the sampling interval, round-off errors, and communication delays between the sensor, controller, and actuators. Consequently, semantic differences between the model and its code can arise with potentially different system behavior. This paper proposes a criterion for faithful implementation of the hybrid-systems model with a focus on its switching semantics. We discuss different techniques to ensure a faithful implementation of the model, and test the feasibility of our concepts by implementing a model heater system. In this heater case study, we successfully eliminate all fault transitions and, thereby, generate code with correct behavior complying with the specification.

}, keywords = {Formal languages, network code, software engineering}, issn = {0018-9340}, doi = {10.1109/TC.2010.84}, url = {http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=5453343}, author = {Anand, Madhukar and Fischmeister, Sebastian and Hur, Yerang and Kim, Jesung and Lee, Insup} } @inproceedings {56, title = {Semantics-Preserving Implementation of Synchronous Specifications Over Dynamic TDMA Distributed Architectures}, booktitle = {Proc. of the International Conference on Embedded Software (EMSOFT)}, year = {2010}, month = {October}, pages = {199-208}, address = {Scottsdale, Arizona, USA}, abstract = {

We propose a technique to automatically synthesize programs and schedules for hard real-time distributed (embedded) systems from synchronous data-flow models. Our technique connects the SynDEx scheduling tool and the Network Code toolchain in a seamless flow of automatic model transformations that go all the way from specification to implementation. Our contribution is the non-trivial connection between the models manipulated by SynDEx and by the Network Code toolchain, at both formal and tool level. We provide an algorithm for converting the data-dependent schedule tables output by SynDEx into Network Code programs which can be seen as an \‘\‘assembly code\’\’ level for time-driven distributed real-time systems. The main difficulty is to ensure the preservation of both functionality and the real-time guarantees computed by SynDEx in the presence of clock drifts (which are abstracted away in the scheduling model of SynDEx). Existing tools can convert the resulting Network Code programs into software and hardware-accelerated execution units.

}, keywords = {clock synchronization, Clocked Graphs, distributed real-time implementation, dynamic TDMA, network code, synchronous model, SynDEx}, isbn = {978-1-60558-904-6}, doi = {10.1145/1879021.1879048}, url = {http://dl.acm.org/citation.cfm?doid=1879021.1879048}, author = {Dumitru Potop-Butucaru and Akramul Azim and Fischmeister, Sebastian} } @article {41, title = {A Verifiable Language for Programming Real-Time Communication Schedules}, journal = {IEEE Transactions on Computers}, volume = {56}, year = {2007}, month = {11/2007}, pages = {1505 - 1519}, keywords = {network code}, issn = {0018-9340}, doi = {10.1109/TC.2007.70747}, author = {Fischmeister, Sebastian and Sokolsky, Oleg and Lee, Insup} }