Sökning: WFRF:(Rodriguez Navas Guillermo) >
Synthesizing time-t...
-
Avni, G.IST Austria, Klosterneuburg, Austria.
(författare)
Synthesizing time-triggered schedules for switched networks with faulty links
- Artikel/kapitelEngelska2016
Förlag, utgivningsår, omfång ...
-
2016-10
-
New York, NY, USA :ACM,2016
-
printrdacarrier
Nummerbeteckningar
-
LIBRIS-ID:oai:DiVA.org:mdh-34027
-
https://urn.kb.se/resolve?urn=urn:nbn:se:mdh:diva-34027URI
-
https://doi.org/10.1145/2968478.2968499DOI
Kompletterande språkuppgifter
-
Språk:engelska
-
Sammanfattning på:engelska
Ingår i deldatabas
Klassifikation
-
Ämneskategori:ref swepub-contenttype
-
Ämneskategori:kon swepub-publicationtype
Anmärkningar
-
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 och genrebeteckningar
Biuppslag (personer, institutioner, konferenser, titlar ...)
-
Guha, S.Hebrew Univ Jerusalem, Jerusalem, Israel
(författare)
-
Rodriguez-Navas, GuillermoMälardalens högskola,Inbyggda system(Swepub:mdh)grs01
(författare)
-
IST Austria, Klosterneuburg, Austria.Hebrew Univ Jerusalem, Jerusalem, Israel
(creator_code:org_t)
Sammanhörande titlar
-
Ingår i:Proceedings of the 13th International Conference on Embedded Software, EMSOFT 2016New York, NY, USA : ACM9781450344852
Internetlänk
Hitta via bibliotek
Till lärosätets databas