Subject: [TICTOC] Using Timed Automata for Modeling Distributed Systems with Clocks: Challenges and Solutions

From: Yaakov Stein <[email-masked]>
Date: Thu, 30 May 2013 04:42:22 +0000

Hi all,

A paper that just appeared in IEEE Transactions on Software Engineering might interest some of you.

Abstract below.

Y(J)S

Using Timed Automata for Modeling Distributed Systems with Clocks: Challenges and Solutions
Guillermo Rodriguez-Navas<http://www.computer.org/search/results?action=authorsearch&resultsPerPage=50&queryOption1=DC_CREATOR&sortOrder=descending&queryText1=Guillermo%20Rodriguez-Navas>, Universitat de les Illes Balears, Palma de Mallorca
Julián Proenza<http://www.computer.org/search/results?action=authorsearch&resultsPerPage=50&queryOption1=DC_CREATOR&sortOrder=descending&queryText1=Juli&#x00E1;n%20Proenza>, Universitat de les Illes Balears, Palma de Mallorca
June 2013 (vol. 39 no. 6)  pp. 857-868

Guillermo Rodriguez-Navas, Julián Proenza, "Using Timed Automata for Modeling Distributed Systems with Clocks: Challenges and Solutions," IEEE Transactions on Software Engineering, vol. 39, no. 6, pp. 857-868, June, 2013.

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2012.73

Abstract
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.