A SOC-Based Formal Specification and Verification of Hybrid Systems

  • Ning Yu
  • Martin Wirsing
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9463)


In order to specify hybrid systems in a SOC paradigm, we define Hybrid Doubly Labeled Transition Systems and the hybrid trace of it. Then we extend SRML notations with a set of differential equation-based expressions and hybrid programs and interpret the notations over Hybrid Doubly Labeled Transition Systems. By redefining the dynamic temporal logic dTL, we provide a logic basis for reasoning about the behavior of hybrid transition systems. We illustrate our approach by a case study about the control of a moving train, in which the movement of the train is regulated by ordinary differential equations.


Hybrid transition systems SRML Differential equations dTL 


  1. 1.
    Georgakopoulos, D., Papazoglou, M.: Service-Oriented Computing. The MIT Press Cambridge, Massachusetts (2009)Google Scholar
  2. 2.
    van der Schaft, A., Schumacher, H.: An Introduction to Hybrid Dynamical Systems. Springer, London, UK (1999)zbMATHGoogle Scholar
  3. 3.
    Abreu, J., Bocchi, L., Fiadeiro, J.L., Lopes, A.: Specifying and composing interaction protocols for service-oriented system modelling. In: Derrick, J., Vain, J. (eds.) FORTE 2007. LNCS, vol. 4574, pp. 358–373. Springer, Heidelberg (2007) CrossRefGoogle Scholar
  4. 4.
    Building Systems using a Service Oriented Architecture. White paper version 0.9 (2005)Google Scholar
  5. 5.
    Fiadeiro, J., Lopes, A., Bocchi, L., Abreu, J.: The Sensoria reference modelling language. In: Wirsing, M., Hölzl, M. (eds.) SENSORIA. LNCS, vol. 6582, pp. 61–114. Springer, Heidelberg (2011) CrossRefGoogle Scholar
  6. 6.
    Abreu, J.: Modelling business conversations in service component architectures. Ph.D thesis, University of Leicester (2009)Google Scholar
  7. 7.
    Yu, N.: Injecting continuous time execution into service-oriented computing. Ph.D thesis, Ludwig-Maximilians-Universität München (to be appeared)Google Scholar
  8. 8.
    Platzer, A.: Towards a hybrid dynamic logic for hybrid dynamic systems. In: Blackburn, P., Bolander, T., Braüner, T., de Paiva, V., Villadsen, J. (eds.) LICS International Workshop on Hybrid Logic 2006, Seattle USA, ENTCS (2007)Google Scholar
  9. 9.
    Henzinger, T., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for read-time systems. In: LICS, pp. 394–406. IEEE Computer Society (1992)Google Scholar
  10. 10.
    Alonso, G., Casati, F., Kuno, H., Machiraju, V.: Web Services. Springer, New York (2004)CrossRefzbMATHGoogle Scholar
  11. 11.
    ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: An action/state-based model-checking approach for the analysis of communication protocols for service-oriented applications. In: Leue, S., Merino, P. (eds.) FMICS 2007. LNCS, vol. 4916, pp. 133–148. Springer, Heidelberg (2008) CrossRefGoogle Scholar
  12. 12.
    Platzer, A.: AVACS - Automatic verification and analysis of complex systems. Technical report No. 12, AVACS (2007)Google Scholar
  13. 13.
    Henzinger, T.A.: The theory of hybrid automata. In: Lnan, M.K., et al. (eds.) LICS 1996, vol. 170, pp. 256–292. Springer, Berlin (2000)Google Scholar
  14. 14.
    Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) HTCS, vol. A, pp. 995–1072. Elsevier, Amsterdam (1995)Google Scholar
  15. 15.
    Harel, D., Kozen, D.: Dynamic Logic. The MIT Press Cambridge, Massachusetts (2000)zbMATHGoogle Scholar
  16. 16.
    Fiadeiro, J., Lopes, A., Bocchi, L.: An abstract model of service discovery and binding. In: Formal Aspects of Computing, vol. 23, pp. 433–463. Springer, Berlin (2011)Google Scholar
  17. 17.
    Fadlisyah, M., Ölveczky, P.C., Ábrahám, E.: Formal modeling and analysis of human body exposure to extreme heat in HI-maude. In: Durán, F. (ed.) WRLA 2012. LNCS, vol. 7571, pp. 139–161. Springer, Heidelberg (2012) CrossRefGoogle Scholar
  18. 18.
    Quesel, J., Mitsch, S., Loos, S., Aréchiga, N., Platzer, A.: How to model and prove hybrid systems with KeYmaera: A tutorial on safety. In: STTT (2015)Google Scholar
  19. 19.
    European Train Control System (ETCS) Open Proofs - Open Source.

Copyright information

© Springer International Publishing Switzerland 2015

Open Access This chapter is distributed under the terms of the Creative Commons Attribution Noncommercial License, which permits any noncommercial use, distribution, and reproduction in any medium, provided the original author(s) and source are credited.

Authors and Affiliations

  1. 1.Programmierung und Softwaretechnik, Institut für informatikLudwig-Maximilians-Universität MünchenMunichGermany

Personalised recommendations