The Model Checker SPIN SPINisanefficientverificationsystemformodelsofdistributedsoftwaresystems.Ithasbeenusedtodetectdesignerrorsinapplicationsrangingfromhigh-leveldescripti