Abstrakt. Vi beskriver våra erfarenheter av att använda Spin för att verifiera delar av det parallella processhanteringssystemet Multi Purpose Daemon (MPD). MPD är en distribuerad samling processer anslutna av Unix nätverksuttag. MPD är dynamisk: processer och anslutningar bland dem skapas och förstörs som MPD initieras, körs användarprocesser, återhämtar sig från fel, och avslutar. Denna dynamiska natur är lätt att uttrycka i ramen Spin/Promela men innebär prestanda- och skalbarhetsutmaningar. Vi presenterar här resultaten av att uttrycka några av de parallella algoritmerna i MPD och utföra både simulering och verifiering körs med Spin.
Matlin m.fl. REF använde Spin för att verifiera en del av MCI-infrastrukturen.