×

Correct transformation: from object-based graph grammars to PROMELA. (English) Zbl 1243.68155

Summary: 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.

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q42 Grammars and rewriting systems
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] , Handbook of graph grammars and computing by graph transformations, volume 1: foundations (1997) · Zbl 0908.68095
[2] Dotti, F. L.; Ribeiro, L.: Specification of mobile code systems using graph grammars, IFIP conference Proceedings 177, 45-63 (2000) · Zbl 0968.68100
[3] Ehrig, H.: Introduction to the algebraic theory of graph grammars, Lecture notes in computer science (LNCS) 73, 1-69 (1979) · Zbl 0407.68072
[4] , Handbook of graph grammars and computing by graph transformation: vol. 2: applications, languages, and tools 2 (1999) · Zbl 0951.68049
[5] , Handbook of graph grammars and computing by graph transformation: vol. 3: concurrency, parallelism, and distribution 3 (1999) · Zbl 0951.68049
[6] Guerraoui, R.; Hurfin, M.; Mostefaoui, A.; Oliveira, R.; Raynal, M.; Schiper, A.; Krakowiak, S. S. S.: Consensus in asynchronous distributed systems: a concise guided tour, Lecture notes in computer science (LNCS), 33-47 (1999)
[7] F.L. Dotti, L. Foss, L. Ribeiro, O.M. Santos, Especificação e verificação formal de sistemas distribuídos, in: 17o Simpósio Brasileiro de Engenharia de Software, Brasil, 2003, pp. 225–240 (in Portuguese).
[8] Santos, O. M.; Dotti, F. L.; Ribeiro, L.: Verifying object-based graph grammars, Electronic notes in theoretical computer science 109, 125-136 (2004) · Zbl 1271.68125
[9] Dotti, F.; Ribeiro, L.; Dos Santos, O.; Pasini, F.: Verifying object-based graph grammars: an assume-guarantee approach, Software and systems modeling 5, No. 3, 289-311 (2006)
[10] Copstein, B.; Móra, M. C.; Ribeiro, L.: An environment for formal modeling and simulation of control systems, , 74-82 (2000)
[11] F.L. Dotti, L.M. Duarte, B. Copstein, L. Ribeiro, Simulation of mobile applications, in: Communication Networks and Distributed Systems Modeling and Simulation Conference, SCS, USA, 2002, pp. 261–267.
[12] Mendizabal, O. M.; Dotti, F. L.; Ribeiro, L.: Stochastic object-based graph grammars, Electronic notes in theoretical computer science 184, 151-170 (2007) · Zbl 1279.68117
[13] Plateau, B.; Atif, K.: Stochastic automata network of modeling parallel systems, IEEE transactions on software engineering 17, No. 10, 1093-1108 (1991)
[14] Michelon, L. R. Leonardo: Simone André da costa, formal specification and verification of real-time systems using graph grammars, Journal of the Brazilian computer society 13, No. 4, 51-68 (2007)
[15] Pasini, F.; Dotti, F. L.: Code generation for parallel applications modelled with object-based graph grammars, Electronic notes on theoretical computer science 184, 113-131 (2007) · Zbl 1279.68059
[16] Snir, M.; Otto, S. W.; Walker, D. W.; Dongarra, J.; Huss-Lederman, S.: MPI: the complete reference, (1995)
[17] Dotti, F. L.; Ribeiro, L.; Santos, O. M.: Specification and analysis of fault behaviours using graph grammars, Lecture notes in computer science (LNCS) 3062, 120-133 (2004)
[18] Dotti, F. L.; Mendizabal, O. M.; Dos Santos, O. M.: Verifying fault-tolerant distributed systems using object-based graph grammars, Lecture notes in computer science (LNCS) 3747, 80-100 (2005)
[19] Gärtner, F. C.: Transformational approaches to the specification and verification of fault-tolerant systems: formal background and classification, Journal of universal computer science 5, No. 10, 668-692 (1999) · Zbl 0967.68108
[20] Ribeiro, L.; Dotti, F. L.; Bardohl, R.: A formal framework for the development of concurrent object-based systems, Lecture notes in computer science (LNCS) 3393, 385-401 (2005) · Zbl 1075.68621 · doi:10.1007/b106390
[21] Dotti, F. L.; Duarte, L. M.; Foss, L.; Ribeiro, L.; Russi, D.; Santos, O. M.: An environment for the development of concurrent object-based applications, Electronic notes in theoretical computer science 127-1, 3-13 (2005)
[22] L. Duarte, F. Dotti, Development of an active network architecture using mobile agents – a case study, Tech. Rep. TR-043, FACIN - PPGCC - PUCRS, 2004.
[23] Dotti, F. L.; Foss, L.; Ribeiro, L.; Santos, O. M.: Verification of object-based distributed systems, Lecture notes in computer science (LNCS) 2884, 261-275 (2003) · Zbl 1253.68059
[24] Holzmann, G. J.: The model checker SPIN, IEEE transactions on software engineering 23, No. 5, 279-295 (1997)
[25] Hoare, C. A. R.: An axiomatic basis for computer programming, Communications of the ACM 12, No. 10, 576-580 (1969) · Zbl 0179.23105 · doi:10.1145/363235.363259
[26] R. Milner, An algebraic definition of simulation between programs, Tech. Rep. CS-TR-71-205, Stanford University, Stanford, CA, USA, 1971.
[27] Burstall, R. M.: An algebraic description of programs with assertions, verification and simulation, SIGACT news 14, 7-14 (1972)
[28] Gerhart, S. L.: Correctness-preserving program transformations, , 54-66 (1975) · Zbl 0361.68013
[29] Harel, D.; Puneli, A.; Stavi, J.: A complete axiomatic system for proving deductions about recursive programs, , 249-260 (1977)
[30] Jones, C. B.: The early search for tractable ways of reasoning about programs, IEEE annals history of computing 25, No. 2, 26-49 (2003)
[31] Schmidt, D. C.: Guest editor’s introduction: model-driven engineering, IEEE computer 39, No. 2, 25-31 (2006)
[32] Baldan, P.; Corradini, A.; König, B.: A framework for the verification of infinite-state graph transformation systems, Information and computation 206, No. 7, 869-907 (2008) · Zbl 1153.68034 · doi:10.1016/j.ic.2008.04.002
[33] Da Costa, S. A.; Ribeiro, L.: Formal verification of graph grammars using mathematical induction, Electronic notes in theoretical computer science 240, 43-60 (2009) · Zbl 1347.68243
[34] Rensink, A.; Schmidt, Á; Varró, D.: Model checking graph transformations: a comparison of two approaches, Lecture notes in computer science (LNCS) 3256, 226-241 (2004) · Zbl 1116.68486 · doi:10.1007/b100934
[35] Kastenberg, H.; Rensink, A.: Model checking dynamic states in GROOVE, Lecture notes in computer science (LNCS) 3925, 299-305 (2006)
[36] Leue, S.; Holzmann, G.: V-promela: a visual, object oriented language for SPIN, , 14-23 (1999)
[37] Lilius, J.; Paltor, I. P.: Vuml: a tool for verifying UML models, , 255-258 (1999)
[38] Chen, J.; Cui, H.: Translation from adapted uml to promela for corba-based applications, Lecture notes in computer science (LNCS) 2989, 234-251 (2004) · Zbl 1125.68340 · doi:10.1007/b96721
[39] Varró, D.: Automated formal verification of visual modeling languages by model checking, Software and systems modeling 3, No. 2, 85-113 (2004)
[40] , Abstract state machines: A method for high-level system design and analysis (2003) · Zbl 1040.68042
[41] C. Demartini, R. Iosif, R. Sisto, Modeling and validation of Java multithreading applications using SPIN, in: G. Holzmann, E. Najm, A. Serhrouchni (Eds.), Proc. of the 4th SPIN workshop, France, 1998.
[42] Corbett, J. C.: Bandera: extracting finite-state models from Java source code, , 439-448 (2000)
[43] Castillo, G. D.: Towards comprehensive tool support for abstract state machines: the ASM workbench tool environment and architecture, Lecture notes in computer science (LNCS) 1641, 311-325 (1999)
[44] Winter, K.; Duke, R.: Model checking object-Z using ASM, Lecture notes in computer science (LNCS) 2335, 165-184 (2002) · Zbl 1057.68636
[45] Sirjani, M.; Movaghar, A.; Shali, A.; De Boer, F. S.: Modeling and verification of reactive systems using rebeca, Fundamenta informticae 63, No. 4, 385-410 (2004) · Zbl 1082.68007
[46] Alavizadeh, F.; Nekoo, A. H.; Sirjani, M.: Reuml: a uml profile for modeling and verification of reactive systems, , 50 (2007)
[47] Dijkstra, E. W.: Hierarchical ordering of sequential processes, Acta informatica 1, 115-138 (1971)
[48] Ricart, G.; Agrawala, A. K.: An optimal algorithm for mutual exclusion in computer networks, Communications of the ACM 24, No. 1, 9-17 (1981)
[49] Ehrig, H.; Heckel, R.; Korff, M.; Löwe, M.; Ribeiro, L.; Wagner, A.; Corradini, A.: Algebraic approaches to graph transformation. Part ii: Single pushout approach and comparison with double pushout approach, , 247-312 (1997)
[50] Corradini, A.; Montanari, U.; Rossi, F.: Graph processes, Fundamenta informaticae 26, No. 3/4, 241-265 (1996) · Zbl 0854.68054
[51] L. Ribeiro, Parallel composition and unfolding semantics of graph grammars, Ph.D. thesis, Technical University of Berlin, Germany, 1996.
[52] Dwyer, M. B.; Avrunin, G. S.; Corbett, J. C.: Patterns in property specifications for finite-state verification, , 411-420 (1999)
[53] Manna, Z.; Pnueli, A.: The temporal logic of reactive and concurrent systems–specification, (1992) · Zbl 0753.68003
[54] Chechik, M.; Păun, D. O.: Events in property patterns, Lecture notes in computer science (LNCS) 1680, 154-167 (1999)
[55] Dwyer, M. B.; Avrunin, G. S.; Corbett, J. C.: Property specification patterns for finite-state verification, , 7-15 (1998)
[56] Dotti, F. L.: An environment for the development of concurrent object-based applications, Electronic notes in theoretical computer science 127, 3-13 (2005)
[57] Research Bell-Labs, SPIN version 3.3: Language reference, 2003. http://spinroot.com/spin/Man/promela.html.
[58] Hoare, C. A. R.: Communicating sequential processes, (1985) · Zbl 0637.68007
[59] C. Weise, An incremental formal semantics for PROMELA, in: 3rd International SPIN Workshop, The Netherlands, 1997.
[60] Milner, R.: Communication and concurrency, (1995)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.