Paper Info
Title
Mapping template semantics to SMV
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.
Year
DOI
Venue
2004
10.1109/ASE.2004.1342756
ASE
Keywords
Field
DocType
user-provided parameters,model-based notation,mapping template semantics,program interpreters,matching language construct,template semantics,smv language,matching language,customized semantics,model checking,specification languages,complex composition operator,complex composition operators,semantics-based parameterized translator,smv model,specification semantics,model-based notations,parameterized translator,program verification,formal specification,user-provided parameter,composition operator
Specification language,Operational semantics,Programming language,Model checking,Computer science,Denotational semantics,Action semantics,Theoretical computer science,Formal specification,Language Of Temporal Ordering Specification,Formal methods
Conference
ISSN
ISBN
Citations 
1938-4300
0-7695-2131-2
7
PageRank 
References 
Authors
0.44
16
4
Name
Order
Citations
PageRank
Yun Lu170.44
Joanne M. Atlee293175.70
Nancy A. Day324321.26
Jianwei Niu427526.61