Abstract
Advanced mechatronic systems, like smart cars or smart trains, perform reconfiguration as a reaction to their changing environment. The reconfiguration behaviour of such systems is safety-critical and needs to be verified by formal verification procedures. In the past, graph transformation systems have proven to be a suitable formalism for specification and verification of such systems. However, existing approaches do not consider that reconfiguration operations consume time. Considering their duration, several reconfiguration operations can be executed concurrently in a running system, possibly resulting in undesired behaviour. In this paper, we introduce durations for graph transformation rules and a locking mechanism that ensures the safe concurrent execution of time-consuming operations. Additionally, we show how graph transformation rules with durations are mapped to an existing verification framework which enables the formal verification of graph transformation systems with durative rules. We illustrate our approach using an example of a smart train system.
This is a preview of subscription content, log in via an institution to check access.
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
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)
Becker, B., Beyer, D., Giese, H., Klein, F., Schilling, D.: Symbolic invariant verification for systems with dynamic structural adaptation. In: Proc. of the 28th Intern. Conf. on Software Engineering (ICSE). ACM Press, Shanghai (May 2006)
Bengtsson, J.E., Yi, W.: Timed automata: Semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2004. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004)
Boronat, A., Ölveczky, P.C.: Formal real-time model transformations in MOMENT2. In: Rosenblum, D.S., Taentzer, G. (eds.) FASE 2010. LNCS, vol. 6013, pp. 29–43. Springer, Heidelberg (2010)
Cheng, B.H.C., et al.: Software engineering for self-adaptive systems: A research roadmap. In: Cheng, B.H.C., de Lemos, R., Giese, H., Inverardi, P., Magee, J. (eds.) Self-Adaptive Systems. LNCS, vol. 5525, pp. 1–26. Springer, Heidelberg (2009)
Eckardt, T., Heinzemann, C., Henkler, S., Hirsch, M., Priesterjahn, C., Schäfer, W.: Modeling and verifying dynamic communication structures based on graph transformations. Computer Science - Research and Development 28(1), 3–22 (2013)
Ehrig, H., Heckel, R., Korff, M., Löwe, M., Ribeiro, L., Wagner, A., Corradini, A.: Handbook of graph grammars and computing by graph transformation. Foundations, vol. 1, pp. 247–312. World Scientific Publishing Co., Inc., River Edge (1997)
Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. Monographs in Theoretical Computer Science. Springer (2006)
Habel, A., Heckel, R., Taentzer, G.: Graph grammars with negative application conditions. Fundamenta Informaticae 26, 287–313 (1995)
Kastenberg, H., Rensink, A.: Model checking dynamic states in groove. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 299–305. Springer, Heidelberg (2006)
de Lara, J., Vangheluwe, H.: Automating the transformation-based analysis of visual languages. Form. Asp. Comput. 22, 297–326 (2010)
de Lara, J., Guerra, E., Boronat, A., Heckel, R., Torrini, P.: Domain-specific discrete event modelling and simulation using graph transformation. Software and Systems Modeling (2012), doi:10.1007/s10270-012-0242-3
Michelon, L., da Costa, S.A., Ribeiro, L.: Formal specification and verification of real-time systems using graph grammars. J. Braz. Comp. Soc. 13(4), 51–68 (2007)
Ölveczky, P.C., Meseguer, J.: Semantics and pragmatics of Real-Time Maude. Higher-Order and Symbolic Computation 20(1-2), 161–196 (2007)
Rivera, J.E., Duran, F., Vallecillo, A.: A graphical approach for modeling time-dependent behavior of DSLs. Visual Languages - Human Centric Computing, 51–55 (2009)
Suck, J., Heinzemann, C., Schäfer, W.: Formalizing model checking on timed graph transformation systems. Tech. Rep. tr-ri-11-316, Software Engineering Group, Heinz Nixdorf Institute, University of Paderborn (September 2011)
Ziegert, S., Heinzemann, C.: Durative graph transformation rules. Tech. Rep. tr-ri-13-329, Heinz Nixdorf Institute, University of Paderborn (March 2013)
Ziegert, S., Wehrheim, H.: Temporal reconfiguration plans for self-adaptive systems. In: Software Engineering (SE 2013). LNI, Gesellschaft für Informatik e.V, GI (February 2013)
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
Ziegert, S., Heinzemann, C. (2013). Durative Graph Transformation Rules for Modelling Real-Time Reconfiguration. In: Liu, Z., Woodcock, J., Zhu, H. (eds) Theoretical Aspects of Computing – ICTAC 2013. ICTAC 2013. Lecture Notes in Computer Science, vol 8049. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39718-9_25
Download citation
DOI: https://doi.org/10.1007/978-3-642-39718-9_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39717-2
Online ISBN: 978-3-642-39718-9
eBook Packages: Computer ScienceComputer Science (R0)