Title
Using Timed Automata for Modeling Distributed Systems with Clocks: Challenges and Solutions
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.
Year
DOI
Venue
2013
10.1109/TSE.2012.73
IEEE Trans. Software Eng.
Keywords
Field
DocType
computer clock,temporal behavior,model checking,different type,timed automata,ideal clock,paper discusses,formal verification,embedded system,suitable modeling pattern,embedded systems,automata,real time systems,automata theory,distributed processing,clock synchronization
Synchronization,Automata theory,Model checking,Computer science,Automaton,Real-time computing,Theoretical computer science,Clock synchronization,Formal verification,Distributed computing
Journal
Volume
Issue
ISSN
39
6
0098-5589
Citations 
PageRank 
References 
6
0.52
14
Authors
3
Name
Order
Citations
PageRank
Guillermo Rodriguez-Navas1233.47
Julian Proenza213418.99
Rodriguez-Navas, G.360.52