{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T00:10:02Z","timestamp":1748736602359,"version":"3.41.0"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319281131"},{"type":"electronic","value":"9783319281148"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-28114-8_9","type":"book-chapter","created":{"date-parts":[[2015,12,29]],"date-time":"2015-12-29T12:57:37Z","timestamp":1451393857000},"page":"151-169","source":"Crossref","is-referenced-by-count":1,"title":["A SOC-Based Formal Specification and Verification of Hybrid Systems"],"prefix":"10.1007","author":[{"given":"Ning","family":"Yu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Wirsing","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,12,30]]},"reference":[{"key":"9_CR1","volume-title":"Service-Oriented Computing","author":"D Georgakopoulos","year":"2009","unstructured":"Georgakopoulos, D., Papazoglou, M.: Service-Oriented Computing. The MIT Press Cambridge, Massachusetts (2009)"},{"key":"9_CR2","volume-title":"An Introduction to Hybrid Dynamical Systems","author":"A Schaft van der","year":"1999","unstructured":"van der Schaft, A., Schumacher, H.: An Introduction to Hybrid Dynamical Systems. Springer, London, UK (1999)"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/978-3-540-73196-2_23","volume-title":"Formal Techniques for Networked and Distributed Systems \u2013 FORTE 2007","author":"J Abreu","year":"2007","unstructured":"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\u2013373. Springer, Heidelberg (2007)"},{"key":"9_CR4","unstructured":"Building Systems using a Service Oriented Architecture. White paper version 0.9 (2005)"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-642-20401-2_5","volume-title":"Rigorous Software Engineering for Service-Oriented Systems: Results of the SENSORIA Project on Software Engineering for Service-Oriented Computing","author":"J Fiadeiro","year":"2011","unstructured":"Fiadeiro, J., Lopes, A., Bocchi, L., Abreu, J.: The Sensoria reference modelling language. In: Wirsing, M., H\u00f6lzl, M. (eds.) SENSORIA. LNCS, vol. 6582, pp. 61\u2013114. Springer, Heidelberg (2011)"},{"key":"9_CR6","unstructured":"Abreu, J.: Modelling business conversations in service component architectures. Ph.D thesis, University of Leicester (2009)"},{"key":"9_CR7","unstructured":"Yu, N.: Injecting continuous time execution into service-oriented computing. Ph.D thesis, Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen (to be appeared)"},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"Platzer, A.: Towards a hybrid dynamic logic for hybrid dynamic systems. In: Blackburn, P., Bolander, T., Bra\u00fcner, T., de Paiva, V., Villadsen, J. (eds.) LICS International Workshop on Hybrid Logic 2006, Seattle USA, ENTCS (2007)","DOI":"10.1016\/j.entcs.2006.11.026"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Henzinger, T., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for read-time systems. In: LICS, pp. 394\u2013406. IEEE Computer Society (1992)","DOI":"10.1109\/LICS.1992.185551"},{"key":"9_CR10","volume-title":"Web Services","author":"G Alonso","year":"2004","unstructured":"Alonso, G., Casati, F., Kuno, H., Machiraju, V.: Web Services. Springer, New York (2004)"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/978-3-540-79707-4_11","volume-title":"Formal Methods for Industrial Critical Systems","author":"MH Beek ter","year":"2008","unstructured":"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\u2013148. Springer, Heidelberg (2008)"},{"key":"9_CR12","unstructured":"Platzer, A.: AVACS - Automatic verification and analysis of complex systems. Technical report No. 12, AVACS (2007)"},{"key":"9_CR13","first-page":"256","volume-title":"Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, LNCS","author":"TA Henzinger","year":"2000","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: Lnan, M.K., et al. (eds.) LICS 1996, vol. 170, pp. 256\u2013292. Springer, Berlin (2000)"},{"key":"9_CR14","first-page":"995","volume-title":"HTCS","author":"EA Emerson","year":"1995","unstructured":"Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) HTCS, vol. A, pp. 995\u20131072. Elsevier, Amsterdam (1995)"},{"key":"9_CR15","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"D Harel","year":"2000","unstructured":"Harel, D., Kozen, D.: Dynamic Logic. The MIT Press Cambridge, Massachusetts (2000)"},{"issue":"4","key":"9_CR16","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/s00165-010-0166-z","volume":"23","author":"Jos\u00e9 Luiz Fiadeiro","year":"2010","unstructured":"Fiadeiro, J., Lopes, A., Bocchi, L.: An abstract model of service discovery and binding. In: Formal Aspects of Computing, vol. 23, pp. 433\u2013463. Springer, Berlin (2011)","journal-title":"Formal Aspects of Computing"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-642-34005-5_8","volume-title":"Rewriting Logic and Its Applications","author":"M Fadlisyah","year":"2012","unstructured":"Fadlisyah, M., \u00d6lveczky, P.C., \u00c1brah\u00e1m, E.: Formal modeling and analysis of human body exposure to extreme heat in HI-maude. In: Dur\u00e1n, F. (ed.) WRLA 2012. LNCS, vol. 7571, pp. 139\u2013161. Springer, Heidelberg (2012)"},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Quesel, J., Mitsch, S., Loos, S., Ar\u00e9chiga, N., Platzer, A.: How to model and prove hybrid systems with KeYmaera: A tutorial on safety. In: STTT (2015)","DOI":"10.1007\/s10009-015-0367-0"},{"key":"9_CR19","unstructured":"European Train Control System (ETCS) Open Proofs - Open Source. http:\/\/openetcs.org\/"}],"container-title":["Lecture Notes in Computer Science","Recent Trends in Algebraic Development Techniques"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-28114-8_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T23:30:41Z","timestamp":1748734241000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-28114-8_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319281131","9783319281148"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-28114-8_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}