Name
Abstract | ||
|---|---|---|
Model transformation is an approach that, among other advantages, enables the reuse of existing analysis and implementation techniques, languages and tools. The area of formal verification makes wide use of model transformation because the cost of constructing efficient model checkers is extremely high. There are various examples of translations from specification and programming languages to the input languages of prominent model checking tools, like SPIN. However, this approach provides a safe analysis method only if there is a guarantee that the transformation process preserves the semantics of the original specification/program, that is, that the transformation is correct. Depending on the source and/or target languages, this notion of correctness is not easy to achieve. In this paper, we tackle this problem in the context of Object-Based Graph Grammars (OBGG). OBGG is a formal language suitable for the specification of distributed systems, with a variety of tools and techniques centered around the transformation of OBGG models. We describe in details the model transformation from OBGG models to PROMELA, the input language of the SPIN model checker. Amongst the contributions of this paper are: (a) the correctness proof of the transformation from OBGG models to PROMELA; (b) a generalization of this process in steps that may be used as a guide to prove the correctness of transformations from different specification/programming languages to PROMELA. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1016/j.scico.2011.03.010 | Sci. Comput. Program. |
Keywords | Field | DocType |
spin model checker,model transformation,transformation process,efficient model checker,obgg model,correct transformation,graph grammars,different specification,programming language,prominent model checking tool,original specification,object-based graph grammar,promela,input language,correctness | Rule-based machine translation,Model transformation,Formal language,Model checking,Programming language,Computer science,Correctness,Theoretical computer science,Promela,SPIN model checker,Formal verification | Journal |
Volume | Issue | ISSN |
77 | 3 | Science of Computer Programming |
Citations | PageRank | References |
1 | 0.35 | 41 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Leila Ribeiro | 1 | 297 | 28.81 |
| Osmar Marchi dos Santos | 2 | 110 | 8.34 |
| Fernando Luís Dotti | 3 | 107 | 11.57 |
| Luciana Foss | 4 | 94 | 14.44 |