Eighth Asia-Pacific Software Engineering Conference (APSEC'01) Model Checking Object-Z Classes: Some Experiments with FDR Macao, China December 04-December 07 ISBN: 0-7695-1408-1
This paper investigates model checking Object-Z classes via their translation to the input notation of the CSP model checker FDR. Such a translation must not only be concerned with preserving the semantics of the original specification, but also with how efficiently the resulting specification can be model checked. Hence, the paper investigates alternative translation schemes and compares how efficiently the resulting specifications can be checked.
Citation:
Geoff Kassel, Graeme Smith, "Model Checking Object-Z Classes: Some Experiments with FDR," apsec, pp.445, Eighth Asia-Pacific Software Engineering Conference (APSEC'01), 2001 Usage of this product signifies your acceptance of the Terms of Use. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||