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

fYear

2004

Firstpage

320

Lastpage

325

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Automated Software Engineering, 2004. Proceedings. 19th International Conference on

ISSN

1938-4300

Print_ISBN

0-7695-2131-2

Type

conf

DOI

10.1109/ASE.2004.1342756

Filename

1342756