Sökning: onr:"swepub:oai:DiVA.org:mdh-34027" >
Synthesizing time-t...
Synthesizing time-triggered schedules for switched networks with faulty links
-
- Avni, G. (författare)
- IST Austria, Klosterneuburg, Austria.
-
- Guha, S. (författare)
- Hebrew Univ Jerusalem, Jerusalem, Israel
-
- Rodriguez-Navas, Guillermo (författare)
- Mälardalens högskola,Inbyggda system
-
IST Austria, Klosterneuburg, Austria Hebrew Univ Jerusalem, Jerusalem, Israel (creator_code:org_t)
- 2016-10
- 2016
- Engelska.
-
Ingår i: Proceedings of the 13th International Conference on Embedded Software, EMSOFT 2016. - New York, NY, USA : ACM. - 9781450344852
- Relaterad länk:
-
http://dl.acm.org/ft...
-
visa fler...
-
https://urn.kb.se/re...
-
https://doi.org/10.1...
-
visa färre...
Abstract
Ämnesord
Stäng
- Time-triggered (TT) switched networks are a deterministic communication infrastructure used by real-time distributed embedded systems. These networks rely on the notion of globally discretized time (i.e. time slots) and a static TT schedule that prescribes which message is sent through which link at every time slot, such that all messages reach their destination before a global timeout. These schedules are generated offline, assuming a static network with fault-free links, and entrusting all error-handling functions to the end user. Assuming the network is static is an over-optimistic view, and indeed links tend to fail in practice. We study synthesis of TT schedules on a network in which links fail over time and we assume the switches run a very simple error-recovery protocol once they detect a crashed link. We address the problem of finding a pk; qresistant schedule; namely, one that, assuming the switches run a fixed error-recovery protocol, guarantees that the number of messages that arrive at their destination by the timeout is at least no matter what sequence of at most k links fail. Thus, we maintain the simplicity of the switches while giving a guarantee on the number of messages that meet the timeout. We show how a pk; q-resistant schedule can be obtained using a CEGAR-like approach: find a schedule, decide whether it is pk; q-resistant, and if it is not, use the witnessing fault sequence to generate a constraint that is added to the program. The newly added constraint disallows the schedule to be regenerated in a future iteration while also eliminating several other schedules that are not pk; q-resistant. We illustrate the applicability of our approach using an SMT-based implementation.
Ämnesord
- TEKNIK OCH TEKNOLOGIER -- Elektroteknik och elektronik (hsv//swe)
- ENGINEERING AND TECHNOLOGY -- Electrical Engineering, Electronic Engineering, Information Engineering (hsv//eng)
Nyckelord
- Fault tolerance
- Real-time communication
- Satisfiability Modulo Theory
- Scheduling
- Computer system recovery
- Embedded software
- Embedded systems
- Errors
- Switching networks
- Time switches
- Deterministic communications
- Distributed embedded system
- Error handling
- Fault sequences
- Satisfiability modulo Theories
- Static networks
- Time triggered
- Real time systems
Publikations- och innehållstyp
- ref (ämneskategori)
- kon (ämneskategori)
Hitta via bibliotek
Till lärosätets databas