Model Checking for Abstract State Machines Export

@article{citeulike:507550, abstract = {In this paper, we discuss the use of a model checker in combination with the specification method of Abstract State Machines (ASMs). A schema is introduced for transforming ASM models into the language of a model checker. We prove that the transformation preserves the semantics of ASMs and provide a theoretical framework for a transformation tool. Experience with model-checking the ASM model of the Production Cell demonstrates that this approach offers effective support for verifying ASM specifications.}, author = {Winter, Kirsten}, citeulike-article-id = {507550}, journal = {Journal of Universal Computer Science}, keywords = {abstract\_state\_machines, formal\_specification, formal\_verification}, number = {5}, pages = {689--701}, posted-at = {2006-02-17 11:21:43}, priority = {2}, title = {Model Checking for Abstract State Machines}, volume = {3}, year = {1997} }

TY - JOUR ID - citeulike:507550 L3 - citeulike-article-id:507550 N2 - In this paper, we discuss the use of a model checker in combination with the specification method of Abstract State Machines (ASMs). A schema is introduced for transforming ASM models into the language of a model checker. We prove that the transformation preserves the semantics of ASMs and provide a theoretical framework for a transformation tool. Experience with model-checking the ASM model of the Production Cell demonstrates that this approach offers effective support for verifying ASM specifications. IS - 5 JF - Journal of Universal Computer Science EP - 701 TI - Model Checking for Abstract State Machines VL - 3 SP - 689 KW - abstract_state_machines KW - formal_specification KW - formal_verification AU - Winter, Kirsten PY - 1997/// ER -