Modeling the ASCB-D Synchronization Algorithm with SPIN: A Case Study

In this paper, we describe our application of SPIN 1 to model an algorithm used to synchronize the clocks of modules that provide periodic real-time communication over a network. We used the SPIN model to check certain performance properties of the system; in particular, we were able to verify that the algorithm achieves synchronization within a time bound, even in the presence of certain types of faults. Our results suggest that state space explosion in models of time-dependent systems can be most e ectively managed by explicit modeling of time; by imposing determinism on execution orderings, and justifying that determinism in a domain-speci c manner; and by splitting up the space of execution sequences according to initial conditions.

• Type: Conference
• Year: 2000
• Where: SPIN
• Authors: Nicholas Weininger, Darren D. Cofer
• Keywords: Algorithm Achieves Synchronization, Certain Performance Properties, Periodic Real-time Communication, SPIN 2000, Theoretical Computer Science