Formal Verification of the FTTRS Mechanisms for the Consistent Update of the Traffic Schedule

Authors Daniel Bujosa Mateu | Sergi Arguimbau Guarinos | Patricia Arguimbau Guarinos | Julián Proenza Arenas | Manuel Alejandro Barranco González
In Proceedings of the IEEE 24th International Conference on Emerging Technologies and Factory Automation (ETFA 2019), Zaragoza, 2019.

Critical Adaptive Distributed Embedded Systems (ADESs) are nowadays the focus of many researchers. ADESs are envisioned to dynamically modify their behavior to support changes of their real-time and dependability requirements at runtime as the conditions of the environment in which they operate vary. To provide ADESs with an adequate communication infrastructure, our research group proposed the Flexible-Time-Triggered Replicated Star (FTTRS). FTTRS provides highly reliable communication services on top of Ethernet, while keeping the adaptivity benefits that the Flexible- Time-Triggered (FTT) communication paradigm offers from a real-time perspective. This paper formally verifies, by means of model checking, the correctness of the mechanisms FTTRS includes to enforce consistent changes of the communication scheduling at runtime.


Uso de cookies

Este sitio web utiliza cookies para que usted tenga la mejor experiencia de usuario. Si continúa navegando está dando su consentimiento para la aceptación de las mencionadas cookies y la aceptación de nuestra política de cookies, pinche el enlace para mayor información.

Aviso de cookies