Using Timed Automata for Modeling Distributed Systems with Clocks: Challenges and Solutions

Authors Guillermo Rodríguez-Navas González | Julián Proenza Arenas
In IEEE Transactions on Software Engineering, IEEE Computer Society, vol. 39, no. 6, pp. 857-868, 2013.

The application of model checking for the formal verification of distributed embedded systems requires the adoption of techniques for realistically modeling the temporal behavior of such systems. This paper discusses how to model with timed automata the different types of relationships that may be found among the computer clocks of a distributed system, namely ideal clocks, drifting clocks and synchronized clocks. For each kind of relationship, a suitable modeling pattern is thoroughly described and formally verified.


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.