The Challenges of Building Advanced Mechatronic Systems

ABSTRACT

Mechatronics is an engineering discipline integrating the fields of mechanical engineering, electrical engineering and computer science. While the word "mechatronics" already has a long history, it is only the last ten years that we see their application all around us. Cars, CD players, washing machines, railways are all examples of mechatronic systems. The main characteristic (and driving force) of recent advances is the progressively tighter coupling of mechanic and electronic components with software. This makes software engineering (together with network technology) the main computer science discipline involved in mechatronics. In this paper we survey current developments and discuss future trends in mechatronics, in particular from a software engineering point of view. The future of mechatronics will specifically see a move towards a high degree of adaptibility and self-organisation. This poses new challenges on software engineering, especially on modelling, code generation and analysis. We exemplify existing as well as future strands by a collaborative research and development project of a mechatronic rail system from the University of Paderborn.

REFERENCES

• 1: [1] E. Ábrahám, T. Schubert, B. Becker, M. Fränzle, and C. Herde. Parallel SAT solving in bounded model checking. In Proc. of PDMC'06, Lecture Notes in Computer Science. Springer Verlag, 2006.
• 2: Rajeev Alur , Franjo Ivancic , Jesung Kim , Insup Lee , Oleg Sokolsky, Generating embedded software from hierarchical hybrid models, Proceedings of the 2003 ACM SIGPLAN conference on Language, compiler, and tool for embedded systems, June 11-13, 2003, San Diego, California, USA
• 3: Thomas Ball , Andreas Podelski , Sriram K. Rajamani, Boolean and Cartesian Abstraction for Model Checking C Programs, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.268-283, April 02-06, 2001
• 4: [4] C. Barrett, L. de Moura, and A. Stump. SMT-COMP: Satisfiability Modulo Theories Competition. In K. Etessami and S. Rajamani, editors, 17th International Conference on Computer Aided Verification, pages 20-23. Springer, 2005.
• 5: [5] A. Bauer, M. Broy, J. Romberg, B. Schätz, P. Braun, U. Freund, N. Mata, R. Sandner, and D. Ziegenbein. AutoMoDe -- Notations, Methods, and Tools for Model-Based Development of Automotive Software. In Proceedings of the SAE 2005 World Congress. Society of Automotive Engineers, 2005.
• 6: Jorg Bauer , Ina Schaefer , Tobe Toben , Bernd Westphal, Specification and Verification of Dynamic Communication Systems, Proceedings of the Sixth International Conference on Application of Concurrency to System Design, p.189-200, June 28-30, 2006 [doi>10.1109/ACSD.2006.29]
• 7: Basil Becker , Dirk Beyer , Holger Giese , Florian Klein , Daniela Schilling, Symbolic invariant verification for systems with dynamic structural adaptation, Proceeding of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China [doi>10.1145/1134285.1134297]
• 8: [8] G. Behrmann, A. David, K. G. Larsen, O. Möller, P. Pettersson, and W. Yi. Uppaal - Present and Future. In 40th IEEE Conference on Decision and Control. IEEE Computer Society Press, 2001.
• 9: [9] K. Bender, M. Broy, I. Peter, A. Pretschner, and T. Stauner. Model based development of hybrid systems. In Modelling, Analysis, and Design of Hybrid Systems, volume 279 of Lecture Notes on Control and Information Sciences, pages 37- 52. Springer Verlag, July 2002.
• 10: [10] K. Berkenkötter, S. Bisanz, U. Hannemann, and J. Peleska. Executable HybridUML and its Application to Train Control Systems. In H. Ehrig, W. Damm, J. Desel, M. Große-Rhode, W. Reif, E. Schnieder, and E. Westkämper, editors, Integration of Software Specification Techniques for Applications in Engineering, volume 3147 of Lecture Notes in Computer Science, pages 145-173. Springer Verlag, 2004.
• 11: [11] E. Böde, W. Damm, J. Høyem, B. Josko, J. Niehaus, and M. Segelken. Adding value to automotive models. In M. Broy, I. H. Krüger, and M. Meisinger, editors, ASWSD, volume 4147 of Lecture Notes in Computer Science, pages 86-102. Springer, 2004.
• 12: J. R. Burch , E. M. Clarke , K. L. McMillan , D. L. Dill , L. J. Hwang, Symbolic model checking: 1020 states and beyond, Information and Computation, v.98 n.2, p.142-170, June 1992 [doi>10.1016/0890-5401(92)90017-A]
• 13: [13] S. Burmester, M. Tichy, and H. Giese. Modeling Reconfigurable Mechatronic Systems with Mechatronic UML. In Proc. of Model Driven Architecture: Foundations and Applications (MDAFA 2004), Linköping, Sweden (U. Asmann, ed.), pages 155-169, June 2004.
• 14: Armin Biere , Alessandro Cimatti , Edmund M. Clarke , Yunshan Zhu, Symbolic Model Checking without BDDs, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.193-207, March 22-28, 1999
• 15: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 16: Edmund Clarke , Armin Biere , Richard Raimi , Yunshan Zhu, Bounded Model Checking Using Satisfiability Solving, Formal Methods in System Design, v.19 n.1, p.7-34, July 2001 [doi>10.1023/A:1011276507260]
• 17: Edmund Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith, Counterexample-guided abstraction refinement for symbolic model checking, Journal of the ACM (JACM), v.50 n.5, p.752-794, September 2003 [doi>10.1145/876638.876643]
• 18: Matthew B. Dwyer , John Hatcliff , Robby Robby , Corina S. Pasareanu , Willem Visser, Formal Software Analysis Emerging Trends in Software Model Checking, 2007 Future of Software Engineering, p.120-136, May 23-25, 2007 [doi>10.1109/FOSE.2007.6]
• 19: Stefan Edelkamp , Stefan Leue , Alberto Lluch-Lafuente, Directed explicit-state model checking in the validation of communication protocols, International Journal on Software Tools for Technology Transfer (STTT), v.5 n.2, p.247-267, March 2004 [doi>10.1007/s10009-002-0104-3]
• 20: Robert France , Bernhard Rumpe, Model-driven Development of Complex Software: A Research Roadmap, 2007 Future of Software Engineering, p.37-54, May 23-25, 2007 [doi>10.1109/FOSE.2007.14]
• 21: Holger Giese , Sven Burmester , Wilhelm Schäfer , Oliver Oberschelp, Modular design and verification of component-based mechatronic systems with online-reconfiguration, Proceedings of the 12th ACM SIGSOFT twelfth international symposium on Foundations of software engineering, October 31-November 06, 2004, Newport Beach, CA, USA
• 22: [22] H. Giese, S. Glesner, J. Leitner, W. Schäfer, and R. Wagner. Towards Verified Model Transformations. In Proc. of the 3rd Workshop on Model design and Validation (MoDeV²a), October 2006.
• 23: Holger Giese , Matthias Tichy , Sven Burmester , Stephan Flake, Towards the compositional verification of real-time UML designs, Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering, September 01-05, 2003, Helsinki, Finland
• 24: [24] T. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech: A Model Checker for Hybrid Systems. Software Tools for Technology Transfer, (1):110-122, 1997.
• 25: Christoph Meyer Kirsch , Marco A. A. Sanvido , Thomas A. Henzinger , Wolfgang Pree, A Giotto-Based Helicopter Control System, Proceedings of the Second International Conference on Embedded Software, p.46-60, October 07-09, 2002
• 26: Jeff Kramer , Jeff Magee, Self-Managed Systems: an Architectural Challenge, 2007 Future of Software Engineering, p.259-268, May 23-25, 2007 [doi>10.1109/FOSE.2007.19]
• 27: C. Loiseaux , S. Graf , J. Sifakis , A. Bouajjani , S. Bensalem, Property preserving abstractions for the verification of concurrent systems, Formal Methods in System Design, v.6 n.1, p.11-44, Jan. 1995 [doi>10.1007/BF01384313]
• 28: Zohar Manna , Amir Pnueli, Temporal verification of reactive systems: safety, Springer-Verlag New York, Inc., New York, NY, 1995
• 29: [29] M. Mutz, M. Huhn, U. Goltz, and C. Krömke. Model Based System Development in Automotive. In Proceedings SAE World Congress. Society of Automotive Engineers, 2003.
• 30: [30] B. I. Silva and B. H. Krogh. Formal Verification of Hybrid System Using CheckMate: A Case Study. In American Control Conference, 2000.
• 31: [31] S. M. L. S. S. SysML Partner, November 2005. version 1.0 alpha, document ad/05-11-14.
• 32: [32] H. Wehrheim. Inheritance of Temporal Logic Properties. In FMOODS 2003: Formal Methods for Open Object-based Distributed Systems, number 2884 in LNCS, pages 79-93. Springer, 2003.
• 33: [33] H. Wehrheim. Preserving Properties under Change. In F. de Boer, M. Bonsague, and W. de Roever, editors, Formal Methods for Components and Objects, volume 3188 of LNCS. Springer, 2004.
• 34: [34] S. Yovine. Kronos: A verification tool for real-time systems. Software Tools for Technology Transfer, 1(1/2), 1997.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.0 General

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.m Miscellaneous

General Terms:
Theory