SMV and the Production Cell Control Problem

Citation: Kirsten Winter, "Model Checking for Abstract State Machines", Journal of Universal Computer Science, vol. 3, no. 5 (1997), 689--701.
Summary: The use of the model checker SMV to verify ASM models (in particular, the production cell control model) is discussed.
Subjects: Benchmark Examples, Mechanical Verification
Download: PostScript, PDF, Compressed PostScript
Notes: See also the description of the ASM solution to the production cell control problem, and its C++ implementation. See also extensions of this work to automatic ASM-to-SMV translation and the FLASH cache coherency protocol. Included in Winter's Ph.D. thesis. Courtesy of Springer-Verlag.