MER Arbiter: JPL’s Mars Exploration Rover (MER) software is multithreaded software that must deal with shared resources. The arbiter module prevents potential conflicts between resource requests, and enforces priorities. It was the subject of a case study using SPIN described in (Holzmann and Joshi 2004) and has been mentioned in on Model-Driven verification. Model checking the original problem, with 11 threads and 15 resources, was deemed infeasible. In the study, three versions of a reduced problem with fewer threads and resources were modeled: a hand-built Promela model; a version using the original C code, with all relevant state information tracked using c_track; and finally a version like the second but using data abstraction with only essential data retained. SPIN found safety and liveness property violations in each version, but nothing considered serious by the engineers; thus the application of SPIN gave more confidence that the design was correct. The first model was efficient, but relies on the accuracy of the hand-built model. The second was inefficient, but adhered to the original C code. The third was efficient, yet still adhered to the original C code.