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.

[an error occurred while processing this directive]

Abstract State Machines