Abstract
In model-driven software development, models and model refinements are used to create software. To automatically generate correct software from abstract models by means of model refinement, desirable properties of the initial models must be preserved. We propose an explicit-state model checking technique to determine whether refinements are property preserving. We use networks of labelled transition systems (LTSs) to represent models with concurrent components, and formalise refinements as systems of LTS transformation rules. Property preservation checking involves determining how a rule system relates to an input network, and checking bisimilarity between behaviour subjected to transformation and the corresponding behaviour after transformation. In this way, one avoids generating the entire LTS of the new model. Experimental results demonstrate speedups of several orders of magnitude.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abadi, M., Lamport, L.: The Existence of Refinement Mappings. Theoretical Computer Science 82, 253–284 (1991)
Beydeda, S., Book, M., Gruhn, V. (eds.): Model-Driven Software Development. Springer, Heidelberg (2005)
Braunstein, C., Encrenaz, E.: CTL-Property Transformations Along an Incremental Design Process. In: Proceedings of the Fourth International Workshop on Automated Verification of Critical Systems. Electronic Notes in Theoretical Computer Science, vol. 128, pp. 263–278. Elsevier (2004)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (1999)
Combemale, B., Crégut, X., Garoche, P.-L., Thirioux, X.: Essay On Semantics Definition in MDE - An Instrumented Approach for Model Verification. Journal of Software 4(9), 943–958 (2009)
Dodds, M., Plump, D.: Graph Transformation in Constant Time. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol. 4178, pp. 367–382. Springer, Heidelberg (2006)
Ehrig, H., Pfender, M., Schneider, H.: Graph Grammars: an Algebraic Approach. In: IEEE Conference Record of 14th Annual Symposium on Switching and Automata Theory, pp. 167–180. IEEE (1973)
Engelen, L.J.P., Wijs, A.J.: Checking Property Preservation of Refining Transformations for Model-Driven Development. CS-Report 12-08, Eindhoven University of Technology (2012)
Eppstein, D., Galil, Z., Italiano, G.: Dynamic Graph Algorithms. In: CRC Handbook of Algorithms and Theory of Computation, ch. 22. CRC Press (1997)
Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 372–387. Springer, Heidelberg (2011)
van Glabbeek, R.J., Luttik, B., Trčka, N.: Branching Bisimilarity with Explicit Divergence. Fundamenta Informaticae 93(4), 371–392 (2009)
Groote, J.F., Keiren, J., Mathijssen, A., Ploeger, B., Stappers, F., Tankink, C., Usenko, Y., van Weerdenburg, M., Wesselink, W., Willemse, T., van der Wulp, J.: The mCRL2 Toolset. In: Proceedings of the 1st International Workshop on Academic Software Development Tools and Techniques (2008)
Groote, J.F., Vaandrager, F.: An Efficient Algorithm for Branching Bisimulation and Stuttering Equivalence. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 626–638. Springer, Heidelberg (1990)
Heckel, R.: Graph Transformation in a Nutshell. In: Proceedings of the School of SegraVis Research Training Network on Foundations of Visual Modelling Techniques. Electronic Notes in Theoretical Computer Science, vol. 148, pp. 187–198. Elsevier (2006)
Hülsbusch, M., König, B., Rensink, A., Semenyak, M., Soltenborn, C., Wehrheim, H.: Showing Full Semantics Preservation in Model Transformation - A Comparison of Techniques. In: Méry, D., Merz, S. (eds.) IFM 2010. LNCS, vol. 6396, pp. 183–198. Springer, Heidelberg (2010)
Karsai, G., Narayanan, A.: On the Correctness of Model Transformations in the Development of Embedded Systems. In: Kordon, F., Sokolsky, O. (eds.) Monterey Workshop 2006. LNCS, vol. 4888, pp. 1–18. Springer, Heidelberg (2007)
Kozen, D.: Results on the Propositional μ-calculus. Theoretical Computer Science 27, 333–354 (1983)
Lambers, L., Ehrig, H., Orejas, F.: Efficient Detection of Conflicts in Graph-based Model Transformation. In: Proceedings of the International Workshop on Graph and Model Transformation. Electronic Notes in Theoretical Computer Science, vol. 152, pp. 97–109. Elsevier (2006)
Lang, F.: Exp.Open 2.0: A Flexible Tool Integrating Partial Order, Compositional, and On-The-Fly Verification Methods. In: Romijn, J., Smith, G., van de Pol, J. (eds.) IFM 2005. LNCS, vol. 3771, pp. 70–88. Springer, Heidelberg (2005)
Lano, K.: The B Language and Method, A Guide to Practical Formal Development. Springer, Heidelberg (1996)
Mateescu, R., Wijs, A.: Property-Dependent Reductions for the Modal Mu-Calculus. In: Groce, A., Musuvathi, M. (eds.) SPIN 2011. LNCS, vol. 6823, pp. 2–19. Springer, Heidelberg (2011)
Narayanan, A., Karsai, G.: Towards Verifying Model Transformations. In: Proceedings of the International Workshop on Graph Transformation and Visual Modeling Techniques. Electronic Notes in Theoretical Computer Science, vol. 211, pp. 191–200 (2008)
Ramalingam, G., Reps, T.: On The Computational Complexity of Dynamic Graph Problems. Theoretical Computer Science 158, 233–277 (1996)
Saha, D.: An Incremental Bisimulation Algorithm. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 204–215. Springer, Heidelberg (2007)
Sokolsky, O.V., Smolka, S.A.: Incremental Model Checking in the Modal Mu-Calculus. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 351–363. Springer, Heidelberg (1994)
Swamy, G.M.: Incremental Methods for Formal Verification and Logic Synthesis. PhD thesis, University of California (1996)
Tarjan, R.: Depth-First Search and Linear Graph Algorithms. SIAM Journal on Computing 1(2), 146–160 (1972)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wijs, A., Engelen, L. (2013). Efficient Property Preservation Checking of Model Refinements. In: Piterman, N., Smolka, S.A. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2013. Lecture Notes in Computer Science, vol 7795. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-36742-7_41
Download citation
DOI: https://doi.org/10.1007/978-3-642-36742-7_41
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-36741-0
Online ISBN: 978-3-642-36742-7
eBook Packages: Computer ScienceComputer Science (R0)