{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,13]],"date-time":"2026-11-13T00:45:31Z","timestamp":1794530731427,"version":"4.9.1"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319471686","type":"print"},{"value":"9783319471693","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-47169-3_36","type":"book-chapter","created":{"date-parts":[[2016,10,4]],"date-time":"2016-10-04T17:56:23Z","timestamp":1475603783000},"page":"433-446","source":"Crossref","is-referenced-by-count":4,"title":["Towards Incremental Validation of Railway Systems"],"prefix":"10.1007","author":[{"given":"Reiner","family":"H\u00e4hnle","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Radu","family":"Muschevici","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,10,5]]},"reference":[{"key":"36_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B Book: Assigning Programs to Meanings","author":"JR Abrial","year":"1996","unstructured":"Abrial, J.R.: The B Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"key":"36_CR2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B \u2014 System and Software Engineering","author":"J Abrial","year":"2010","unstructured":"Abrial, J.: Modeling in Event-B \u2014 System and Software Engineering. Cambridge University Press, Cambridge (2010)"},{"key":"36_CR3","unstructured":"Deliverable 1.2 of project FP7-231620 (HATS): Full ABS Modeling Framework, March 2011. http:\/\/www.hats-project.eu"},{"key":"36_CR4","unstructured":"The ABS Language Specification (2016). http:\/\/abs-models.org\/documentation\/manual\/"},{"key":"36_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"562","DOI":"10.1007\/978-3-642-54862-8_46","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Albert","year":"2014","unstructured":"Albert, E., Arenas, P., Flores-Montoya, A., Genaim, S., G\u00f3mez-Zamalloa, M., Martin-Martin, E., Puebla, G., Rom\u00e1n-D\u00edez, G.: SACO: static analyzer for concurrent objects. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 562\u2013567. Springer, Heidelberg (2014). doi: 10.1007\/978-3-642-54862-8_46"},{"key":"36_CR6","doi-asserted-by":"crossref","unstructured":"Albert, E., Arenas, P., G\u00f3mez-Zamalloa, M., Wong, P.Y.H.: aPET: a test case generation tool for concurrent objects. In: Meyer, B., Baresi, L., Mezini, M. (eds.) Joint Meeting European Software Engineering Conference and ACM SIGSOFT Symposium on Foundations of Software Engineering, ESEC\/FSE, St Petersburg, pp. 595\u2013598. ACM (2013)","DOI":"10.1145\/2491411.2494590"},{"issue":"4","key":"36_CR7","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1007\/s11761-013-0148-0","volume":"8","author":"E Albert","year":"2014","unstructured":"Albert, E., de Boer, F.S., H\u00e4hnle, R., Johnsen, E.B., Schlatte, R., Tapia Tarifa, S.L., Wong, P.Y.H.: Formal modeling of resource management for cloud architectures: an industrial case study using Real-Time ABS. J. Service-Oriented Comput. Appl. 8(4), 323\u2013339 (2014)","journal-title":"J. Service-Oriented Comput. Appl."},{"issue":"5","key":"36_CR8","doi-asserted-by":"crossref","first-page":"49","DOI":"10.5381\/jot.2009.8.5.c5","volume":"8","author":"S Apel","year":"2009","unstructured":"Apel, S., K\u00e4stner, C.: An overview of feature-oriented software development. J. Object Technol. 8(5), 49\u201384 (2009)","journal-title":"J. Object Technol."},{"key":"36_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-07317-0_1","volume-title":"Formal Methods for Executable Software Models","author":"R Bubel","year":"2014","unstructured":"Bubel, R., Montoya, A.F., H\u00e4hnle, R.: Analysis of executable software models. In: Bernardo, M., Damiani, F., H\u00e4hnle, R., Johnsen, E.B., Schaefer, I. (eds.) SFM 2014. LNCS, vol. 8483, pp. 1\u201325. Springer, Heidelberg (2014). doi: 10.1007\/978-3-319-07317-0_1"},{"key":"36_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/978-3-662-45231-8_9","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"R Bubel","year":"2014","unstructured":"Bubel, R., H\u00e4hnle, R., Pelevina, M.: Fully abstract operation contracts. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014, Part II. LNCS, vol. 8803, pp. 120\u2013134. Springer, Heidelberg (2014). doi: 10.1007\/978-3-662-45231-8_9"},{"key":"36_CR11","unstructured":"Butler, M.: Incremental design of distributed systems with event-b. In: Broy, M., Sitou, W., Hoare, T. (eds.) Engineering Methods and Tools for Software Safety and Security: Marktoberdorf Summer School 2008, pp. 131\u2013160. IOS Press (2009). http:\/\/eprints.soton.ac.uk\/266910\/ . Chap. 4"},{"issue":"1","key":"36_CR12","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/s00165-007-0061-4","volume":"20","author":"MJ Butler","year":"2008","unstructured":"Butler, M.J., Yadav, D.: An incremental development of the Mondex system in Event-B. Formal Aspects Comput. 20(1), 61\u201377 (2008)","journal-title":"Formal Aspects Comput."},{"key":"36_CR13","unstructured":"Deutsche Bahn Netz AG, Frankfurt, Germany: Fahrdienstvorschrift Richtlinie 408, December 2015. http:\/\/fahrweg.dbnetze.com\/fahrweg-de\/nutzungsbedingungen\/regelwerke\/betriebl_technisch\/eiu_interne_regeln_ril_408.html"},{"key":"36_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1007\/978-3-319-21401-6_35","volume-title":"Automated Deduction - CADE-25","author":"CC Din","year":"2015","unstructured":"Din, C.C., Bubel, R., H\u00e4hnle, R.: KeY-ABS: a deductive verification tool for the concurrent modelling language ABS. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 517\u2013526. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-21401-6_35"},{"issue":"3","key":"36_CR15","doi-asserted-by":"crossref","first-page":"551","DOI":"10.1007\/s00165-014-0322-y","volume":"27","author":"CC Din","year":"2015","unstructured":"Din, C.C., Owe, O.: Compositional reasoning about active objects with shared futures. Formal Aspects Comput. 27(3), 551\u2013572 (2015)","journal-title":"Formal Aspects Comput."},{"key":"36_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-319-25423-4_14","volume-title":"Formal Methods and Software Engineering","author":"CC Din","year":"2015","unstructured":"Din, C.C., Tapia Tarifa, S.L., H\u00e4hnle, R., Johnsen, E.B.: History-based specification and verification of scalable concurrent and distributed systems. In: Butler, M., Conchon, S., Za\u00efdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 217\u2013233. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-25423-4_14"},{"issue":"6","key":"36_CR17","doi-asserted-by":"crossref","first-page":"643","DOI":"10.1007\/s10009-014-0342-1","volume":"16","author":"A Fantechi","year":"2014","unstructured":"Fantechi, A., Flammini, F., Gnesi, S.: Formal methods for railway control systems. STTT 16(6), 643\u2013646 (2014)","journal-title":"STTT"},{"key":"36_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1007\/978-3-319-21401-6_36","volume-title":"Automated Deduction - CADE-25","author":"N Fulton","year":"2015","unstructured":"Fulton, N., Mitsch, S., Quesel, J.-D., V\u00f6lp, M., Platzer, A.: KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 527\u2013538. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-21401-6_36"},{"key":"36_CR19","doi-asserted-by":"crossref","unstructured":"Giachino, E., Laneve, C., Lienhardt, M.: A framework for deadlock detection in core abs. Softw. Syst. Model. 1\u201336 (2015)","DOI":"10.1007\/s10270-014-0444-y"},{"key":"36_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-40615-7_1","volume-title":"Formal Methods for Components and Objects","author":"R H\u00e4hnle","year":"2013","unstructured":"H\u00e4hnle, R.: The abstract behavioral specification language: a tutorial introduction. In: Giachino, E., H\u00e4hnle, R., de Boer, F.S., Bonsangue, M.M. (eds.) Formal Methods for Components and Objects. LNCS, vol. 7866, pp. 1\u201337. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-40615-7_1"},{"key":"36_CR21","doi-asserted-by":"crossref","unstructured":"Henrio, L., Rochas, J.: From modelling to systematic deployment of distributed active objects\u2013extended version. Research Report $$<$$ < hal-01299817 $$>$$ > , I3S, April 2016","DOI":"10.1007\/978-3-319-39519-7_13"},{"key":"36_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/978-3-319-11164-3_21","volume-title":"Runtime Verification","author":"M Hentschel","year":"2014","unstructured":"Hentschel, M., Bubel, R., H\u00e4hnle, R.: Symbolic execution debugger (SED). In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 255\u2013262. Springer, Heidelberg (2014). doi: 10.1007\/978-3-319-11164-3_21"},{"issue":"6","key":"36_CR23","doi-asserted-by":"crossref","first-page":"685","DOI":"10.1007\/s10009-014-0304-7","volume":"16","author":"P James","year":"2014","unstructured":"James, P., Moller, F., Nga, N.H., Roggenbach, M., Schneider, S.A., Treharne, H.: Techniques for modelling and verifying railway interlockings. STTT 16(6), 685\u2013711 (2014)","journal-title":"STTT"},{"key":"36_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-25271-6_8","volume-title":"Formal Methods for Components and Objects","author":"EB Johnsen","year":"2011","unstructured":"Johnsen, E.B., H\u00e4hnle, R., Sch\u00e4fer, J., Schlatte, R., Steffen, M.: ABS: a core language for abstract behavioral specification. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) Formal Methods for Components and Objects. LNCS, vol. 6957, pp. 142\u2013164. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-25271-6_8"},{"key":"36_CR25","doi-asserted-by":"crossref","unstructured":"Kang, K.C., Cohen, S., Hess, J., Nowak, W., Peterson, S.: Feature-Oriented domain analysis (FODA) feasibility study. Technical report, CMU\/SEI-90-TR-021, Carnegie Mellon University Software Engineering Institute (1990)","DOI":"10.21236\/ADA235785"},{"key":"36_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-642-10373-5_13","volume-title":"Formal Methods and Software Engineering","author":"A Platzer","year":"2009","unstructured":"Platzer, A., Quesel, J.-D.: European train control system: a case study in formal verification. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 246\u2013265. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-10373-5_13"},{"key":"36_CR27","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-28901-1","volume-title":"Software Product Line Engineering","author":"K Pohl","year":"2005","unstructured":"Pohl, K., B\u00f6ckle, G., van der Linden, F.: Software Product Line Engineering. Springer, Heidelberg (2005)"},{"key":"36_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-41135-4_1","volume-title":"Tests and Proofs","author":"K Reichl","year":"2016","unstructured":"Reichl, K., Fischer, T., Tummeltshammer, P.: Using formal methods for verification and validation in railway. In: Aichernig, B.K., Furia, C.A. (eds.) Tests and Proofs. LNCS, vol. 9762, pp. 3\u201313. Springer, Heidelberg (2016). doi: 10.1007\/978-3-319-41135-4_1"},{"key":"36_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-642-15579-6_6","volume-title":"Software Product Lines: Going Beyond","author":"I Schaefer","year":"2010","unstructured":"Schaefer, I., Bettini, L., Bono, V., Damiani, F., Tanzarella, N.: Delta-oriented programming of software product lines. In: Bosch, J., Lee, J. (eds.) SPLC 2010. LNCS, vol. 6287, pp. 77\u201391. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-15579-6_6"},{"issue":"4","key":"36_CR30","doi-asserted-by":"crossref","first-page":"390","DOI":"10.1007\/s00165-005-0076-7","volume":"17","author":"S Schneider","year":"2005","unstructured":"Schneider, S., Treharne, H.: CSP theorems for communicating B machines. Formal Aspects Comput. 17(4), 390\u2013422 (2005)","journal-title":"Formal Aspects Comput."},{"issue":"2","key":"36_CR31","doi-asserted-by":"crossref","first-page":"374","DOI":"10.1002\/cpe.3480","volume":"28","author":"V Serbanescu","year":"2016","unstructured":"Serbanescu, V., Azadbakht, K., de Boer, F.S., Nagarajagowda, C., Nobakht, B.: A design pattern for optimizations in data intensive applications using ABS and JAVA 8. Concurrency Comput. Pract. Experience 28(2), 374\u2013385 (2016)","journal-title":"Concurrency Comput. Pract. Experience"},{"key":"36_CR32","doi-asserted-by":"crossref","unstructured":"Setyautami, M.R.A., Azurat, A., H\u00e4hnle, R., Muschevici, R.: A UML profile for delta-oriented programming to support software product line engineering. In: International Software Product Line Conference. ACM Press (2016)","DOI":"10.1145\/2934466.2934479"},{"key":"36_CR33","doi-asserted-by":"crossref","unstructured":"Sun, P., Dutilleul, S.C., Bon, P.: A model pattern of railway interlocking system by Petri nets. In: International Conference on Models and Technologies for Intelligent Transportation Systems (MT-ITS), Budapest, Hungary, pp. 442\u2013449. IEEE (2015)","DOI":"10.1109\/MTITS.2015.7223292"},{"key":"36_CR34","doi-asserted-by":"crossref","unstructured":"Th\u00fcm, T., Schaefer, I., Hentschel, M., Apel, S.: Family-based deductive verification of software product lines. In: Ostermann, K., Binder, W. (eds.) Generative Programming and Component Engineering, GPCE 2012, Dresden, Germany, pp. 11\u201320. ACM (2012)","DOI":"10.1145\/2371401.2371404"},{"issue":"5","key":"36_CR35","doi-asserted-by":"crossref","first-page":"567","DOI":"10.1007\/s10009-012-0250-1","volume":"14","author":"PYH Wong","year":"2012","unstructured":"Wong, P.Y.H., Albert, E., Muschevici, R., Proen\u00e7a, J., Sch\u00e4fer, J., Schlatte, R.: The ABS tool suite: modelling, executing and analysing distributed adaptable object-oriented systems. STTT 14(5), 567\u2013588 (2012)","journal-title":"STTT"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-47169-3_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,14]],"date-time":"2019-09-14T04:09:12Z","timestamp":1568434152000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47169-3_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319471686","9783319471693"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47169-3_36","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-319-47169-3","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}