Abstract
While traditionally the environment considered by an autonomous mechatronic systems only consists of the measurable, surrounding physical world, today advanced mechatronic systems also include the context established by the information technology. This trend makes mechatronic systems possible which consist of cooperating agents which optimize and reconfigure the system behavior by adjusting their local behavior and cooperation structure to better serve their current goals depending on the experienced mechanical and information environment. The Mechatronic UML approach enables the component-wise development of such self-optimizing mechatronic systems by providing a notion for hybrid components and support for modular verification of the safe online-reconfiguration. In this paper, we present an extension to the formerly presented solution which overcomes the restriction that only purely reactive behavior with restricted time constraints can be verified. We present how model checking can be employed to also verify the safe modular reconfiguration for systems which include components with complex time constraints and proactive behavior.
This work was developed in the course of the Special Research Initiative 614 – Self-optimizing Concepts and Structures in Mechanical Engineering – University of Paderborn, and was published on its behalf and funded by the Deutsche Forschungsgemeinschaft.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Sztipanovits, J., Karsai, G., Bapty, T.: Self-adaptive software for signal processing. Commun. ACM 41(5), 66–73 (1998)
Giese, H., Burmester, S., Schäfer, W., Oberschelp, O.: Modular Design and Verification of Component-Based Mechatronic Systems with Online-Reconfiguration. In: Proc. of 12th ACM SIGSOFT Foundations of Software Engineering 2004 (FSE 2004), Newport Beach, USA, November 2004, pp. 179–188. ACM Press, New York (2004)
Giese, H., Tichy, M., Burmester, S., Schäfer, W., Flake, S.: Towards the Compositional Verification of Real-Time UML Designs. In: Proc. of the European Software Engineering Conference (ESEC), Helsinki, Finland, September 2003, pp. 38–47. ACM Press, New York (2003)
Hestermeyer, T., Schlautmann, P., Ettingshausen, C.: Active suspension system for railway vehicles-system design and kinematics. In: Proc. of the 2nd IFAC - Confecence on mechatronic systems, Berkeley, California, USA, December 9-11 (2002)
Burmester, S., Giese, H., Schäfer, W.: Model-driven architecture for hard real-time systems: From platform independent models to code. In: Hartman, A., Kreische, D. (eds.) ECMDA-FA 2005. LNCS, vol. 3748, pp. 1–15. Springer, Heidelberg (2005)
Jensen, H.E., Guldstr, K., Guldstr, K., Skou, A.: Scaling up Uppaal Automatic Verification of Real-Time Systems using Compositionality and Abstraction. In: Joseph, M. (ed.) FTRTFT 2000. LNCS, vol. 1926, p. 19. Springer, Heidelberg (2000)
Tripakis, S.: Folk theorems on the determinization and minimization of timed automata. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 182–188. Springer, Heidelberg (2004)
Giese, H., Hirsch, M.: Timed and Hybrid Refinement in Mechtronic UML. Technical Report tr-ri-03-266, University of Paderborn, Paderborn, Germany (December 2005)
Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)
Burmester, S., Giese, H., Hirsch, M., Schilling, D.: Incremental design and formal verification with UML/RT in the FUJABA real-time tool suite. In: Proceedings of the International Workshop on Specification and vaildation of UML models for Real Time and embedded Systems, SVERTS 2004, Satellite Event of the 7th International Conference on the Unified Modeling Language, UML2004 (October 2004)
Agrawal, A., Simon, G., Karsai, G.: Semantic Translation of Simulink/Stateflow models to Hybrid Automata using Graph Transformations. In: International Workshop on Graph Transformation and Visual Modeling Techniques, Barcelona, Spain (2004)
Alur, R., Dang, T., Esposito, J., Fierro, R., Hur, Y., Ivancic, F., Kumar, V., Lee, I., Mishra, P., Pappas, G., Sokolsky, O.: Hierarchical Hybrid Modeling of Embedded Systems. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol. 2211, p. 14. Springer, Heidelberg (2001)
Henzinger, T.A.: Masaccio: A Formal Model for Embedded Components. In: Watanabe, O., Hagiya, M., Ito, T., van Leeuwen, J., Mosses, P.D. (eds.) TCS 2000. LNCS, vol. 1872, pp. 549–563. Springer, Heidelberg (2000)
Grosu, R., Stauner, T., Broy, M.: A modular visual model for hybrid systems. In: Ravn, A.P., Rischel, H. (eds.) FTRTFT 1998. LNCS, vol. 1486, p. 75. Springer, Heidelberg (1998)
Lynch, N., Segala, R., Vaandrager, F.: Hybrid I/O Automata Revisited. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 403–417. Springer, Heidelberg (2001)
Lamport, L.: Hybrid systems in tla+. In: Hybrid Systems, London, UK, pp. 77–102. Springer, Heidelberg (1993)
Henzinger, T.A., Minea, M., Prabhu, V.: Assume-Guarantee Reasoning for Hierarchical Hybrid Systems. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 275–290. Springer, Heidelberg (2001)
Henzinger, T.A., Kirsch, C.M., Sanvido, M.A.A., Pree, W.: From Control Models to Real-Time Code Using Giotto. EMSOFT 2002 23(1), 50–64 (2002); A preliminary report on this work appeared. Henzinger, T.A., Kirsch, C.M., Sanvido, M.A.A., Pree, W.: From Control Models to Real-Time Code Using Giotto. In: Sangiovanni-Vincentelli, A.L., Sifakis, J. (eds.) EMSOFT 2002. LNCS, vol. 2491, pp. 46–60. Springer, Heidelberg (2002)
Beyer, D.: Efficient reachability analysis and refinement checking of timed automata using BDDs. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 86–91. Springer, Heidelberg (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Giese, H., Hirsch, M. (2006). Modular Verification of Safe Online-Reconfiguration for Proactive Components in Mechatronic UML. In: Bruel, JM. (eds) Satellite Events at the MoDELS 2005 Conference. MODELS 2005. Lecture Notes in Computer Science, vol 3844. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11663430_8
Download citation
DOI: https://doi.org/10.1007/11663430_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-31780-7
Online ISBN: 978-3-540-31781-4
eBook Packages: Computer ScienceComputer Science (R0)