SwePub - sökning: L773:1424403790

Numrering	Referens	Omslagsbild	Hitta
1.	Rodriguez-Navas, Guillermo, et al. (författare) An UPPAAL Model for Formal Verification of Master/Slave Clock 2006 Ingår i: Factory Communication Systems, 2006 IEEE International Workshop on. - 1424403790 ; , s. 3-12 Konferensbidrag (refereegranskat)abstract Many distributed applications require a clock synchronization service. We have previously proposed a clock synchronization service for the Controller Area Network (CAN), which we have claimed to provide highly synchronized clocks even in the occurrence of faults in the system. In this paper we substantiate this claim by providing a formal model and verification of our fault tolerant clock synchronization mechanism. We base our modeling and verification on timed automata theory as implemented by the model checking tool UPPAAL. In the modeling we introduce a novel technique for modeling drifting clocks. The verification shows that a precision in the order of 2 Î¼s is guaranteed despite nodeâ€™s faults as well as consistent channel faults. It also shows that inconsistent channel faults may significantly worsen the achievable precision, but that this effect can be reduced by choosing a suitable resynchronization period.

Rodriguez-Navas, Guillermo, et al. (författare)
An UPPAAL Model for Formal Verification of Master/Slave Clock
2006
Ingår i: Factory Communication Systems, 2006 IEEE International Workshop on. - 1424403790 ; , s. 3-12
Konferensbidrag (refereegranskat)abstract
- Many distributed applications require a clock synchronization service. We have previously proposed a clock synchronization service for the Controller Area Network (CAN), which we have claimed to provide highly synchronized clocks even in the occurrence of faults in the system. In this paper we substantiate this claim by providing a formal model and verification of our fault tolerant clock synchronization mechanism. We base our modeling and verification on timed automata theory as implemented by the model checking tool UPPAAL. In the modeling we introduce a novel technique for modeling drifting clocks. The verification shows that a precision in the order of 2 Î¼s is guaranteed despite nodeâ€™s faults as well as consistent channel faults. It also shows that inconsistent channel faults may significantly worsen the achievable precision, but that this effect can be reduced by choosing a suitable resynchronization period.

Träfflista för sökning "L773:1424403790 "