This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Using Timed Automata for Modeling Distributed Systems with Clocks: Challenges and Solutions
June 2013 (vol. 39 no. 6)
pp. 857-868
G. Rodriguez-Navas, Dept. de Cienc. Mat. i Inf., Univ. de les Illes Balears, Palma de Mallorca, Spain
J. Proenza, Dept. de Cienc. Mat. i Inf., Univ. de les Illes Balears, Palma de Mallorca, Spain
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.
Index Terms:
Real-time systems,Automata,Formal verification,Distributed processing,Embedded systems,hybrid automata,Embedded systems,real-time systems,clock synchronization,model checking,timed automata
Citation:
G. Rodriguez-Navas, J. 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:10.1109/TSE.2012.73
Usage of this product signifies your acceptance of the Terms of Use.