Abstract
Correctness of model transformations is a prerequisite for generating correct implementations from models. Given refining model transformations that preserve desirable properties, models can be transformed into correct-by-construction implementations. However, proving that model transformations preserve properties is far from trivial. Therefore, we aim for simple correctness proofs by designing model transformations that are as fine-grained as possible. Furthermore, we advocate the reuse of model transformations to reduce the number of proofs. For a simple domain-specific language, SLCO, we define a formal framework to reason about the correctness, reusability, and composition of the fine-grained model transformations used to transform a given model to three target languages: NQC, Promela and POOSL. The correctness criterion induces that the original model and the resulting model obtained after a proper sequence of transformations have the same observable behavior.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
van Amstel, M.F., van den Brand, M.G.J., Engelen, L.J.P.: An Exercise in Iterative Domain-Specific Language Design. In: Proc. of EVOL/IWPSE 2010, pp. 48–57. ACM (2010)
van Amstel, M.F., van den Brand, M.G.J., Engelen, L.J.P.: Using a DSL and Fine-Grained Model Transformations to Explore the Boundaries of Model Verification. In: Proc. ICSTW 2011, pp. 63–66. IEEE Computer Society (2011)
van Amstel, M.F., van den Brand, M.G.J., Protić, Z., Verhoeff, T.: Transforming Process Algebra Models into UML State Machines: Bridging a Semantic Gap? In: Vallecillo, A., Gray, J., Pierantonio, A. (eds.) ICMT 2008. LNCS, vol. 5063, pp. 61–75. Springer, Heidelberg (2008)
Andova, S., van den Brand, M.G.J., Engelen, L.: Prototyping the Semantics of a DSL using ASF+SDF: Link to Formal Verification of DSL Models. In: AMMSE, pp. 65–79 (2011)
Baum, D.: NQC Programmer’s Guide (2003)
De Nicola, R., Vaandrager, F.W.: Three logics for branching bisimulation. Journal of the ACM 42, 458–487 (1995)
Ehrig, H., Ermel, C.: Semantical Correctness and Completeness of Model Transformations Using Graph and Rule Transformation. In: Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G. (eds.) ICGT 2008. LNCS, vol. 5214, pp. 194–210. Springer, Heidelberg (2008)
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)
Giese, H., Glesner, S., Leitner, J., Schäfer, W., Wagner, R.: Towards Verified Model Transformations. In: Proc. MoDeVa 2006, pp. 78–93 (2006)
van Glabbeek, R.J.: The Linear Time–Branching Time Spectrum II: The Semantics of Sequential Systems with Silent Moves. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 66–81. Springer, Heidelberg (1993)
van Glabbeek, R.J., Weijland, P.: Branching Time and Abstraction in Bisimulation Semantics. Journal of the ACM 43, 555–600 (1996)
Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering 23(5), 279–295 (1997)
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)
Plotkin, G.D.: A Structural Approach to Operational Semantics. Technical Report DAIMI FN-19, University of Aarhus (1981)
Schätz, B.: Verification of Model Transformations. ECEASST 29 (2010)
Schmidt, D.C.: Model-Driven Engineering. Computer 39(2), 25–31 (2006)
Theelen, B.D., et al.: Software/Hardware Engineering with the Parallel Object-Oriented Specification Language. In: Proc. MEMOCODE 2007, pp. 139–148. IEEE (2007)
Varró, D.: Automated formal verification of visual modeling languages by model checking. Software and System Modeling 3(2), 85–113 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Andova, S., van den Brand, M.G.J., Engelen, L. (2012). Reusable and Correct Endogenous Model Transformations. In: Hu, Z., de Lara, J. (eds) Theory and Practice of Model Transformations. ICMT 2012. Lecture Notes in Computer Science, vol 7307. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30476-7_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-30476-7_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-30475-0
Online ISBN: 978-3-642-30476-7
eBook Packages: Computer ScienceComputer Science (R0)