Abstract
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.
References
Georgakopoulos, D., Papazoglou, M.: Service-Oriented Computing. The MIT Press Cambridge, Massachusetts (2009)
van der Schaft, A., Schumacher, H.: An Introduction to Hybrid Dynamical Systems. Springer, London, UK (1999)
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)
Building Systems using a Service Oriented Architecture. White paper version 0.9 (2005)
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)
Abreu, J.: Modelling business conversations in service component architectures. Ph.D thesis, University of Leicester (2009)
Yu, N.: Injecting continuous time execution into service-oriented computing. Ph.D thesis, Ludwig-Maximilians-Universität München (to be appeared)
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)
Henzinger, T., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for read-time systems. In: LICS, pp. 394–406. IEEE Computer Society (1992)
Alonso, G., Casati, F., Kuno, H., Machiraju, V.: Web Services. Springer, New York (2004)
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)
Platzer, A.: AVACS - Automatic verification and analysis of complex systems. Technical report No. 12, AVACS (2007)
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)
Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) HTCS, vol. A, pp. 995–1072. Elsevier, Amsterdam (1995)
Harel, D., Kozen, D.: Dynamic Logic. The MIT Press Cambridge, Massachusetts (2000)
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)
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)
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)
European Train Control System (ETCS) Open Proofs - Open Source. http://openetcs.org/
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Appendices
Appendix 1: A Rule Schema of the dTL Calculus
A rule schema of the dTL calculus can be found in Table 1. In these rules, \(\phi ,\psi \in Fml\) and \(\pi \in Fml_{T}\); \(\chi _{1}\in EF\) and \(\chi _{2}\in {{E\text {-}EF}}\), \(T_{1},\ldots ,T_{n}\in ETERM\), \(T\in {{E\text {-}ETERM}}\) and \(t\in ETERM_{time}\). In D3, M is a first-order formula and the substitution of \(M_{T_{1}\ldots T_{n}}^{T'_{1}\ldots T'_{n}}\), which replaces \(T_{1}\ldots T_{n}\) by \(T'_{1}\ldots T'_{n}\) in M. In D7-D8, \(f_{v_{0}}\) is the solution of the initial value problem \(v_{time}=T,v^{\triangle (\sigma (0))}=v_{0}\), where \(\sigma (0)\) is the state in which variable v has the value \(v_{0}\). In P10, \(Cl_{\forall }(F_{0}\rightarrow G_{0})\rightarrow Cl_{\forall }(F\rightarrow G)\) is an instance of a first-order tautology of real arithmetic and \(Cl_{\forall }\) is the universal closure.
Appendix 2: SRML Specification of Module Train-Control
The SRML specification of service module Train-Control is shown in Fig. 6.
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Yu, N., Wirsing, M. (2015). A SOC-Based Formal Specification and Verification of Hybrid Systems. In: Codescu, M., Diaconescu, R., Țuțu, I. (eds) Recent Trends in Algebraic Development Techniques. WADT 2015. Lecture Notes in Computer Science(), vol 9463. Springer, Cham. https://doi.org/10.1007/978-3-319-28114-8_9
Download citation
DOI: https://doi.org/10.1007/978-3-319-28114-8_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-28113-1
Online ISBN: 978-3-319-28114-8
eBook Packages: Computer ScienceComputer Science (R0)