{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,4]],"date-time":"2026-04-04T10:00:42Z","timestamp":1775296842045,"version":"3.50.1"},"publisher-location":"Cham","reference-count":47,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030047702","type":"print"},{"value":"9783030047719","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-030-04771-9_27","type":"book-chapter","created":{"date-parts":[[2018,12,5]],"date-time":"2018-12-05T17:02:53Z","timestamp":1544029373000},"page":"367-386","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Towards a Hybrid Verification Approach"],"prefix":"10.1007","author":[{"given":"Nahla","family":"Elaraby","sequence":"first","affiliation":[]},{"given":"Eva","family":"K\u00fchn","sequence":"additional","affiliation":[]},{"given":"Anita","family":"Messinger","sequence":"additional","affiliation":[]},{"given":"Sophie Therese","family":"Radschek","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,12,6]]},"reference":[{"key":"27_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)"},{"key":"27_CR2","volume-title":"The B-Book: Assigning Programs to Meanings","author":"JR Abrial","year":"2005","unstructured":"Abrial, J.R., Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)"},{"key":"27_CR3","volume-title":"ACTORS: A Model of Concurrent Computation in Distributed Systems","author":"GA Agha","year":"1990","unstructured":"Agha, G.A.: ACTORS: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge (1990)"},{"key":"27_CR4","doi-asserted-by":"crossref","unstructured":"Barthe, G., et al.: Preservation of proof obligations for hybrid verification methods. In: 6th IEEE International Conference on Software Engineering and Formal Methods, pp. 127\u2013136 (2008)","DOI":"10.1109\/SEFM.2008.10"},{"key":"27_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/3-540-48119-2_22","volume-title":"FM 99 \u2014 Formal Methods","author":"P Behm","year":"1999","unstructured":"Behm, P., Benoit, P., Faivre, A., Meynadier, J.-M.: M\u00e9t\u00e9or: a successful application of B in a large project. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 369\u2013387. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48119-2_22"},{"key":"27_CR6","doi-asserted-by":"crossref","unstructured":"Behrend, J., et al.: Optimized hybrid verification of embedded software. In: 15th Latin American Test Workshop (LATW), pp. 1\u20136 (2014)","DOI":"10.1109\/LATW.2014.6841906"},{"key":"27_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"561","DOI":"10.1007\/10722167_45","volume-title":"Computer Aided Verification","author":"T Bienm\u00fcller","year":"2000","unstructured":"Bienm\u00fcller, T., Damm, W., Wittke, H.: The Statemate verification environment. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 561\u2013567. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722167_45"},{"issue":"4","key":"27_CR8","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1023\/A:1016503426126","volume":"6","author":"M Butler","year":"2002","unstructured":"Butler, M.: A system-based approach to the formal development of embedded controllers for a railway. Des. Autom. Embed. Syst. 6(4), 355\u2013366 (2002)","journal-title":"Des. Autom. Embed. Syst."},{"key":"27_CR9","doi-asserted-by":"crossref","unstructured":"Campos, S., et al.: Verus: a tool for quantitative analysis of finite-state real-time systems. In: ACM SIGPLAN 1995 Workshop on Languages, Compilers and Tools for Real-time Systems. LCTES, pp. 70\u201378 (1995)","DOI":"10.1145\/216636.216661"},{"key":"27_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/3-540-63010-4_5","volume-title":"Transformation-Based Reactive Systems Development","author":"S Campos","year":"1997","unstructured":"Campos, S., Clarke, E.: The verus language: representing time efficiently with BDDs. In: Bertran, M., Rus, T. (eds.) ARTS 1997. LNCS, vol. 1231, pp. 64\u201378. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63010-4_5"},{"key":"27_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-49646-7_22","volume-title":"Computer Safety, Reliability and Security","author":"A Cimatti","year":"1998","unstructured":"Cimatti, A., Giunchiglia, F., Mongardi, G., Romano, D., Torielli, F., Traverso, P.: Model checking safety critical software with SPIN: an application to a railway interlocking system. In: Ehrenberger, W. (ed.) SAFECOMP 1998. LNCS, vol. 1516, pp. 284\u2013293. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/3-540-49646-7_22"},{"key":"27_CR12","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/j.entcs.2003.05.004","volume":"88","author":"K Claessen","year":"2004","unstructured":"Claessen, K.: Safety property verification of cyclic synchronous circuits. Electron. Notes Theor. Comput. Sci. 88, 55\u201369 (2004)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"27_CR13","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Schlingloff, B.H.: Model checking. In: Handbook of Automated Reasoning, pp. 1635\u20131790. Elsevier (2001)","DOI":"10.1016\/B978-044450813-3\/50026-6"},{"key":"27_CR14","doi-asserted-by":"crossref","unstructured":"Cra\u00df, S., K\u00fchn, E., Salzer, G.: Algebraic foundation of a data model for an extensible space-based collaboration protocol. In: International Database Engineering and Applications Symposium (IDEAS), pp. 301\u2013306. ACM (2009)","DOI":"10.1145\/1620432.1620466"},{"issue":"2","key":"27_CR15","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1023\/A:1011279932612","volume":"19","author":"W Damm","year":"2001","unstructured":"Damm, W., Klose, J.: Verification of a radio-based signaling system using the STATEMATE verification environment. Formal Methods Syst. Des. 19(2), 121\u2013141 (2001)","journal-title":"Formal Methods Syst. Des."},{"key":"27_CR16","doi-asserted-by":"crossref","unstructured":"Drusinky, D., Shing, M.T.: Verification of timing properties in rapid system prototyping. In: 14th IEEE International Workshop on Rapid System Prototyping, pp. 47\u201353 (2003)","DOI":"10.1109\/IWRSP.2003.1207029"},{"key":"27_CR17","doi-asserted-by":"crossref","unstructured":"Du, Q., et al.: High availability verification framework for OpenStack based on fault injection. In: 11th International Conference on Reliability, Maintainability and Safety (ICRMS), pp. 1\u20137 (2016)","DOI":"10.1109\/ICRMS.2016.8050168"},{"key":"27_CR18","doi-asserted-by":"crossref","unstructured":"Feng, C., et al.: Complexity and vulnerability of high-speed rail network in China. In: 236th Chinese Control Conference (CCC), pp. 10034\u201310039 (2017)","DOI":"10.23919\/ChiCC.2017.8028958"},{"key":"27_CR19","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-14261-1_11","volume-title":"FORMS\/FORMAT 2010","author":"A Ferrari","year":"2011","unstructured":"Ferrari, A., Magnani, G., Grasso, D., Fantechi, A.: Model checking interlocking control tables. In: Schnieder, E., Tarnai, G. (eds.) FORMS\/FORMAT 2010, pp. 107\u2013115. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-14261-1_11"},{"issue":"1","key":"27_CR20","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1145\/2363.2433","volume":"7","author":"D Gelernter","year":"1985","unstructured":"Gelernter, D.: Generative communication in linda. ACM Trans. Program. Lang. Syst. (TOPLAS) 7(1), 80\u2013112 (1985)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"issue":"2","key":"27_CR21","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1145\/129630.376083","volume":"35","author":"D Gelernter","year":"1992","unstructured":"Gelernter, D., Carriero, N.: Coordination languages and their significance. Commun. ACM (CACM) 35(2), 96\u2013107 (1992)","journal-title":"Commun. ACM (CACM)"},{"key":"27_CR22","unstructured":"Glosser, R.J., et al.: Black channel communications apparatus and method, US Patent, WO2016039737, GE Intelligent Platorms Inc. (2016)"},{"key":"27_CR23","volume-title":"Modeling Reactive Systems with Statecharts: The STATEMATE Approach","author":"D Harel","year":"1998","unstructured":"Harel, D., Politi, M.: Modeling Reactive Systems with Statecharts: The STATEMATE Approach. McGraw-Hill, New York City (1998)"},{"key":"27_CR24","doi-asserted-by":"crossref","unstructured":"Hazelhurst, S., et al.: A hybrid verification approach: getting deep into the design. In: Design Automation Conference (IEEE Cat. No. 02CH37324), pp. 111\u2013116 (2002)","DOI":"10.1145\/513918.513948"},{"key":"27_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-319-47169-3_21","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications","author":"P James","year":"2016","unstructured":"James, P., Moller, F., Nguyen, H.N., Roggenbach, M., Treharne, H., Wang, X.: OnTrack: the railway verification toolset. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 294\u2013296. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47169-3_21"},{"key":"27_CR26","unstructured":"James, P., Roggenbach, M.: Automatically verifying railway interlockings using SAT-based model checking. ECEASST 35 (2010)"},{"key":"27_CR27","doi-asserted-by":"publisher","DOI":"10.1007\/b137706","volume-title":"Secure Systems Development with UML","author":"J Jrjens","year":"2005","unstructured":"Jrjens, J.: Secure Systems Development with UML. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/b137706"},{"key":"27_CR28","doi-asserted-by":"crossref","unstructured":"Kaneko, S., et al.: Experimental verification on the prediction of the trend in radio resource availability in cognitive radio. In: IEEE 66th Vehicular Technology Conference, pp. 1568\u20131572 (2007)","DOI":"10.1109\/VETECF.2007.333"},{"key":"27_CR29","doi-asserted-by":"crossref","unstructured":"Kang, K.C., Ko, K.I.: Formalization and verification of safety properties of statechart specifications. In: Asia-Pacific Software Engineering Conference, pp. 16\u201327 (1996)","DOI":"10.1109\/APSEC.1996.566736"},{"key":"27_CR30","doi-asserted-by":"crossref","unstructured":"Khan, U., et al.: Real time modeling of interlocking control system of Rawalpindi Cantt train yard. In: 13th International Conference on Frontiers of Information Technology (FIT), pp. 347\u2013352. IEEE (2015)","DOI":"10.1109\/FIT.2015.28"},{"key":"27_CR31","unstructured":"K\u00fchn, E.: Peer Model White Paper. Technical report, TU Wien (2012\u20132018)"},{"issue":"04","key":"27_CR32","doi-asserted-by":"publisher","first-page":"1740001","DOI":"10.1142\/S0218843017400019","volume":"25","author":"Eva K\u00fchn","year":"2016","unstructured":"K\u00fchn, E.: Reusable coordination components: reliable development of cooperative information systems. Int. J. Coop. Inf. Syst. (IJCIS) 25(4) (2016)","journal-title":"International Journal of Cooperative Information Systems"},{"key":"27_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-319-68972-2_8","volume-title":"Fundamentals of Software Engineering","author":"E K\u00fchn","year":"2017","unstructured":"K\u00fchn, E.: Flexible transactional coordination in the peer model. In: Dastani, M., Sirjani, M. (eds.) FSEN 2017. LNCS, vol. 10522, pp. 116\u2013131. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68972-2_8"},{"key":"27_CR34","doi-asserted-by":"crossref","unstructured":"K\u00fchn, E., et al.: Introducing the concept of customizable structured spaces for agent coordination in the production automation domain. In: 8th International Conference on Autonomous Agents and Multiagent System (AAMAS), IFAAMAS, pp. 625\u2013632 (2009)","DOI":"10.65109\/YXNP3580"},{"key":"27_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-642-38493-6_9","volume-title":"Coordination Models and Languages","author":"E K\u00fchn","year":"2013","unstructured":"K\u00fchn, E., Cra\u00df, S., Joskowicz, G., Marek, A., Scheller, T.: Peer-based programming model for coordination patterns. In: De Nicola, R., Julien, C. (eds.) COORDINATION 2013. LNCS, vol. 7890, pp. 121\u2013135. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38493-6_9"},{"key":"27_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"574","DOI":"10.1007\/978-3-319-74781-1_38","volume-title":"Software Engineering and Formal Methods","author":"E K\u00fchn","year":"2018","unstructured":"K\u00fchn, E., Radschek, S.T.: An initial user study comparing the readability of a graphical coordination model with Event-B notation. In: Cerone, A., Roveri, M. (eds.) SEFM 2017. LNCS, vol. 10729, pp. 574\u2013590. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-74781-1_38"},{"key":"27_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-319-92408-3_9","volume-title":"Coordination Models and Languages","author":"E K\u00fchn","year":"2018","unstructured":"K\u00fchn, E., Radschek, S.T., Elaraby, N.: Distributed coordination runtime assertions for the peer model. In: Di Marzo Serugendo, G., Loreti, M. (eds.) COORDINATION 2018. LNCS, vol. 10852, pp. 200\u2013219. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-92408-3_9"},{"key":"27_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003: Formal Methods","author":"M Leuschel","year":"2003","unstructured":"Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855\u2013874. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45236-2_46"},{"issue":"1","key":"27_CR39","doi-asserted-by":"publisher","first-page":"3:1","DOI":"10.1145\/3156017","volume":"40","author":"J Lidman","year":"2017","unstructured":"Lidman, J., Mckee, S.A.: Verifying reliability properties using the hyperball abstract domain. ACM Trans. Program. Lang. Syst. 40(1), 3:1\u20133:29 (2017)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"27_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-642-11747-3_13","volume-title":"Engineering Secure Software and Systems","author":"N Moebius","year":"2010","unstructured":"Moebius, N., Stenzel, K., Reif, W.: Formal verification of application-specific security properties in a model-driven approach. In: Massacci, F., Wallach, D., Zannone, N. (eds.) ESSoS 2010. LNCS, vol. 5965, pp. 166\u2013181. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11747-3_13"},{"key":"27_CR41","unstructured":"Petri, C.A.: Kommunikation mit Automaten. Ph.D. thesis, Technische Hochschule Darmstadt (1962)"},{"key":"27_CR42","doi-asserted-by":"crossref","unstructured":"Ribeiro, F.G.C., et al.: Guidelines for using MARTE profile packages considering concerns of real-time embedded systems. In: 15th International Conference on Industrial Informatics (INDIN), pp. 917\u2013922 (2017)","DOI":"10.1109\/INDIN.2017.8104894"},{"issue":"3","key":"27_CR43","doi-asserted-by":"publisher","first-page":"12140","DOI":"10.3182\/20140824-6-ZA-1003.02212","volume":"47","author":"\u0130brahim \u015eENER","year":"2014","unstructured":"Sener, I., et al.: Specification and formal verification of safety properties in point automation system by using timed-arc Petri nets. In: 19th IFAC World Congress. IFAC Proceedings Volumes, vol. 47, no. 3, pp. 12140\u201312145 (2014)","journal-title":"IFAC Proceedings Volumes"},{"issue":"22","key":"27_CR44","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/S1474-6670(17)46663-8","volume":"28","author":"A.G. Stothert","year":"1995","unstructured":"Stothert, A., MacLeod, I.: Modelling and verifying timing properties in distributed computer control systems. In: 13th IFAC Workshop on Distributed Computer Control Systems (DCCS). IFAC Proceedings Volumes, vol. 28, no. 22, pp. 25\u201330 (1995)","journal-title":"IFAC Proceedings Volumes"},{"key":"27_CR45","doi-asserted-by":"crossref","unstructured":"Thapa, V., Song, E., Kim, H.: An approach to verifying security and timing properties in UML models. In: 15th IEEE International Conference on Engineering of Complex Computer Systems, pp. 193\u2013202 (2010)","DOI":"10.1109\/ICECCS.2010.10"},{"key":"27_CR46","doi-asserted-by":"crossref","unstructured":"Wang, L., Cai, F.: Reliability analysis for flight control systems using probabilistic model checking. In: 8th IEEE International Conference on Software Engineering and Service Science (ICSESS), pp. 161\u2013164 (2017)","DOI":"10.1109\/ICSESS.2017.8342887"},{"key":"27_CR47","unstructured":"Winter, K., et al.: Tool support for checking railway interlocking designs. In: Tenth Australian Workshop on Safety-Related Programmable Systems (SCS). CRPIT, ACS, vol. 55, pp. 101\u2013107 (2005)"}],"container-title":["Lecture Notes in Computer Science","Software Technologies: Applications and Foundations"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-04771-9_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,4]],"date-time":"2026-04-04T09:26:03Z","timestamp":1775294763000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-04771-9_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030047702","9783030047719"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-04771-9_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"STAF","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Federation of International Conferences on Software Technologies: Applications and Foundations","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Toulouse","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 June 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 June 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"staf2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.staf2018.fr\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}