Paper Info
Title
Formal specification and analysis of functional properties of graph rewriting-based model transformation.
Abstract
Model processing programs are regularly used when working with models or synthetizing the code from them; therefore, their verification has become an essential component of constructing reliable software in model-based software engineering. Models are usually formalized and visualized as graphs; therefore, model processing programs based on algebraic graph rewriting systemssuch programs are called model transformationsare often applied, and their verification has become an important research area. The goal of our research is to support offline transformation analysis by automated methods, where offline means that only the definition of the program itself, the language definitions of its source and target models are used during the analysis. Therefore, the results are independent from concrete source models, and the analysis needs to be performed only once. Based on previous work, this paper provides the synthesis and of a set of individual components and improves them to provide a complete verification solution: (i) a language is introduced to specify the properties to be verified; (ii) a formalism to describe model transformations in a declarative way; and (iii) automated algorithms that can analyse the declarative transformations as well as the properties expressed by the language. Besides its theoretical basis, the implementation of a verification framework is presented, and its operation is illustrated on a case study. Although the formal verification of model transformation properties is algorithmically undecidable in general, our goal is to provide a practically usable, scoped framework that can largely facilitate the manual verification of model transformations. Copyright (c) 2013 John Wiley & Sons, Ltd.
Year
DOI
Venue
2013
10.1002/stvr.1502
SOFTWARE TESTING VERIFICATION & RELIABILITY
Keywords
Field
DocType
model processing,model transformation,graph rewriting,verification,offline analysis
Verification and validation of computer simulation models,Functional verification,Programming language,Computer science,Runtime verification,Theoretical computer science,Formal specification,Graph rewriting,High-level verification,Formal verification,Software verification
Journal
Volume
Issue
ISSN
23.0
SP5
0960-0833
Citations 
PageRank 
References 
4
0.41
10
Authors
3
Name
Order
Citations
PageRank
Márk Asztalos110810.94
László Lengyel217225.15
Tihamer Levendovszky323327.58