Title :
Mapping template semantics to SMV
Author :
Lu, Yun ; Atlee, Joanne M. ; Day, Nancy A. ; Niu, Jianwei
Author_Institution :
Sch. of Comput. Sci., Waterloo Univ., Ont., Canada
Abstract :
We show how to create a semantics-based, parameterized translator from model-based notations to SMV, using template semantics. Our translator takes as input a specification and a set of user-provided parameters that encode the specification´s semantics; it produces an SMV model suitable for model checking. Using such a translator, we can model check a specification that has customized semantics. Our work also shows how to represent complex composition operators, such as rendezvous, in the SMV language, in which there is no matching language construct.
Keywords :
formal specification; program interpreters; program verification; specification languages; SMV language; SMV model; complex composition operators; customized semantics; matching language construct; model checking; model-based notations; semantics-based parameterized translator; specification semantics; template semantics; user-provided parameters; Algebra; Carbon capture and storage; Computational modeling; Computer science; Concurrent computing; High temperature superconductors; Software engineering; State-space methods; Writing;
Conference_Titel :
Automated Software Engineering, 2004. Proceedings. 19th International Conference on
Print_ISBN :
0-7695-2131-2
DOI :
10.1109/ASE.2004.1342756
