Abstract
In this paper, the authors introduce an extension of UML for the purpose of hybrid systems modeling. The construction uses the profile mechanism of UML 2.0 which is the standard procedure for extending the Unified Modeling Language. The “intuitive semantics” of the syntactic extension is based on the semantics for hierarchic Hybrid Automata, as suggested by Alur et. al. In contrast to Alur’s formalism, HybridUML allows to label transitions not only with conditions and assignments, but also with signals. Furthermore, our approach associates formal semantics by definition of a transformation from HybridUML specifications into programs of a “low-level” language which is both executable in hard real-time and semantically well-defined. When compared to approaches assigning semantics directly to the high-level constructs of a formal specification language, the transformation approach offers two main advantages: First, semantics can be more easily adapted to syntactic extensions by extending the transformation in an appropriate way. Second, all models are automatically executable, since the low-level language is.
The work presented in this article has been investigated by the authors in the context of the HYBRIS (Efficient Specification of Hybrid Systems) project supported by the Deutsche Forschungsgemeinschaft DFG as part of the priority programme on Software Specification – Integration of Software Specification Techniques for Applications in Engineering.
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., Grosu, R., Lee, I., Sokolsky, O.: Compositional refinement for hierarchical hybrid systems. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 33–48. Springer, Heidelberg (2001)
Bienmüller, T., Bohn, J., Brinkmann, H., Brockmeyer, U., Damm, W., Hungar, H., Jansen, P.: Verification of automotive control units. In: Olderog, E.-R., Steffen, B. (eds.) Correct System Design. LNCS, vol. 1710, pp. 319–341. Springer, Heidelberg (1999)
Berkenkötter, K., Bisanz, S., Hannemann, U., Peleska, J., Tsiolakis, A.: The Hybrid Low Level Language HL3. Technical Report 34, Technologie Zentrum Informatik TZI, Universität Bremen (July 2004) (to appear)
Berkenkötter, K., Bisanz, S., Hannemann, U., Peleska, J.: The HybridUML Profile for UML 2.0. Technical Report 32, Technologie Zentrum Informatik TZI, Universität Bremen (June 2004)
Berkenkötter, K., Bisanz, S., Hannemann, U., Peleska, J., Tsiolakis, A.: Automated Test Data Generation for Hybrid Systems
Priority Programme Software Specification – Integration of Software Specification Techniques for Applications in Engineering, http://tfs.cs.tuberlin.de/projekte/indspec/SPP
Dipartimento di Ingegneria Aerospaziale Politecnico di Milano. RTAI homepage (2003), http://www.aero.polimi.it/rtai/about/index.html
Damm, W., Josko, B., Hungar, H., Pnueli, A.: A compositional real-time semantics of STATEMATE designs. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 186–238. Springer, Heidelberg (1998)
de Roever, W.-P., de Boer, F., Hannemann, U., Hooman, J., Lakhneche, Y., Poel, M., Zwiers, J.: Concurrency Verification, April 2001. Cambridge Tracts in Theoretical Computer Science, vol. 54. Cambridge University Press, Cambridge (2001)
Henzinger, T.A.: The theory of hybrid automata. In: Proceedings of the 11th Annual Symposium on Logic in Computer Science (LICS), pp. 278–292. IEEE Computer Society Press, Los Alamitos (1996)
Henzinger, T.A., Horowitz, B., Kirsch, C.M.: Giotto: A time-triggered language for embedded programming. Proceedings of the IEEE 91, 84–99 (2003)
Heitmeyer, C., Lynch, N.: The generalized railroad crossing: A case study in formal verification of real-time systems. In: IEEE Real-Time Systems Symposium, pp. 120–131. IEEE Computer Society, Los Alamitos (1994)
Kesten, Y., Manna, Z., Pnueli, A.: Verification of clocked and hybrid systems. Acta Informatica 36(11), 836–912 (2000)
Kopetz, H.: Real-Time Systems – Design Principles for Distributed Embedded Applications. The Kluwer International Series in Engineering and Computer Science. Kluwer Academic Publishers, Dordrecht (1997)
FSM Labs. RT-Linux homepage, http://www.rtlinux.org (2004)
OMG. UML 2.0 Infrastructure Specification, OMG Adopted Specification (September 2003), http://www.omg.org/cgi-bin/apps/doc?ptc/03-09-15.pdf
OMG. UML 2.0 Superstructure Specification, OMG Adopted Specification (August 2003), http://www.omg.org/cgi-bin/apps/doc?ptc/03-08-02.pdf
Rumbaugh, J., Jacobson, I., Booch, G.: The Unified Modeling Language – Reference Manual. Addison-Wesley, Reading (1999)
Rönnkö, M., Ravn, A.P., Sere, K.: Hybrid action systems. Theoretical Computer Science 290, 937–973 (2003)
Verified Systems. RT-Tester 6.x – User Manual. Technical Report Verified-INT-014-2003, Verified Systems International GmbH, Bremen (2004)
Zhou, C., Ravn, A.P., Hansen, M.R.: An extended duration calculus for hybrid real-time systems. In: Hybrid Systems, pp. 36–59. The Computer Society of the IEEE, Los Alamitos (1993) (extended abstract)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Berkenkötter, K., Bisanz, S., Hannemann, U., Peleska, J. (2004). Executable HybridUML and Its Application to Train Control Systems. In: Ehrig, H., et al. Integration of Software Specification Techniques for Applications in Engineering. Lecture Notes in Computer Science, vol 3147. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27863-4_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-27863-4_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23135-6
Online ISBN: 978-3-540-27863-4
eBook Packages: Springer Book Archive