{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,4]],"date-time":"2025-12-04T18:51:21Z","timestamp":1764874281103,"version":"3.44.0"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783032009418"},{"type":"electronic","value":"9783032009425"}],"license":[{"start":{"date-parts":[[2025,8,28]],"date-time":"2025-08-28T00:00:00Z","timestamp":1756339200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,8,28]],"date-time":"2025-08-28T00:00:00Z","timestamp":1756339200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-00942-5_10","type":"book-chapter","created":{"date-parts":[[2025,8,27]],"date-time":"2025-08-27T12:03:08Z","timestamp":1756296188000},"page":"185-202","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Promise-Driven Modeling: A Structured Approach for\u00a0Modeling Cyber-Physical Systems"],"prefix":"10.1007","author":[{"given":"Felix","family":"Schaber","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Atif","family":"Mashkoor","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Leuschel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,8,28]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Leveson, N.: Engineering a Safer World: Systems Thinking Applied to Safety (2012). ISBN 978-0262533690","DOI":"10.7551\/mitpress\/8179.001.0001"},{"key":"10_CR2","unstructured":"Leveson, N., Thomas, J.: STPA Handbook, p. 188 (2018). https:\/\/psas.scripts.mit.edu\/home\/get_file.php?name=STPA_handbook.pdf"},{"key":"10_CR3","doi-asserted-by":"publisher","unstructured":"Leveson, N.G.: Design and assurance of control software. IEEE Trans. Softw. Eng. 51(3), 666\u2013672 (2025). https:\/\/doi.org\/10.1109\/TSE.2025.3539975. ISSN 0098-5589, 1939-3520, 2326-3881. Accessed 30 Mar 2025","DOI":"10.1109\/TSE.2025.3539975"},{"key":"10_CR4","unstructured":"Bergstra, J.A., Burgess, M.: Promise Theory: Principles and Applications. tAxis, Oslo (2014). ISBN 978-1-4954-3777-9"},{"key":"10_CR5","unstructured":"Abrial, J.-R.: Modeling in Event-B - System and Software Engineering. Cambridge University Press (2010). ISBN 978-0-521-89556-9"},{"key":"10_CR6","doi-asserted-by":"publisher","unstructured":"Mashkoor, A., Leuschel, M., Egyed, A.: Validation obligations: a novel approach to check compliance between requirements and their formal specification. In: 2021 IEEE\/ACM 43rd International Conference on Software Engineering: New Ideas and Emerging Results (ICSE-NIER), pp. 1\u20135 (2021). https:\/\/doi.org\/10.1109\/ICSE-NIER52604.2021.00009","DOI":"10.1109\/ICSE-NIER52604.2021.00009"},{"key":"10_CR7","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"J-R Abrial","year":"2010","unstructured":"Abrial, J.-R., et al.: Rodin: an open toolset for modelling and reasoning in event-B. Int. J. Softw. Tools Technol. Transfer 12, 447\u2013466 (2010)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Mashkoor, A., Jacquot, J.-P.: Observation-level-driven formal modeling. In: 2015 IEEE 16th International Symposium on High Assurance Systems Engineering (HASE), Daytona Beach, Shores, FL, USA, pp. 158\u2013165. IEEE (2015). ISBN 978-1-4799-8111-3. Accessed 24 Mar 2025","DOI":"10.1109\/HASE.2015.32"},{"key":"10_CR9","doi-asserted-by":"publisher","unstructured":"Schaber, F., Mashkoor, A., Leuschel, M.: Towards a novel approach to railway safety using STPA and promise theory. In: Liu, S. (ed.) Software Fault Prevention, Verification, and Validation, vol. 15393, pp. 263\u2013279. Springer, Singapore (2025). https:\/\/doi.org\/10.1007\/978-981-96-1621-3_17. Accessed 23 Mar 2025","DOI":"10.1007\/978-981-96-1621-3_17"},{"key":"10_CR10","doi-asserted-by":"publisher","unstructured":"Versluis, N.D., et al.: Real-time railway traffic management under moving-block signalling: a literature review and research agenda. Transp. Res. Part C: Emerg. Technol. 158, 104438 (2024). https:\/\/doi.org\/10.1016\/j.trc.2023.104438. ISSN 0968090X. Accessed 05 Apr 2025","DOI":"10.1016\/j.trc.2023.104438"},{"key":"10_CR11","unstructured":"UNISIG. SUBSET-026 System Requirements Specification (2023). https:\/\/www.era.europa.eu\/system\/files\/2023-09\/index004_-_SUBSET-026_v400.zip"},{"key":"10_CR12","unstructured":"EULYNX. Interface Specification SCI-TDS. https:\/\/rail-research.europa.eu\/wp-content\/uploads\/2023\/06\/20230628-Interface-specification-SCI-TDS-Eu.Doc.44-v4.0-2.A.pdf"},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-642-30885-7_14","volume-title":"Abstract State Machines, Alloy, B, VDM, and Z","author":"D D\u00e9harbe","year":"2012","unstructured":"D\u00e9harbe, D., Fontaine, P., Guyot, Y., Voisin, L.: SMT solvers for Rodin. In: Derrick, J., et al. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 194\u2013207. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-30885-7_14"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-030-48077-6_21","volume-title":"Rigorous State-Based Methods","author":"M Werth","year":"2020","unstructured":"Werth, M., Leuschel, M.: VisB: a lightweight tool to visualize formal models with SVG graphics. In: Raschke, A., M\u00e9ry, D., Houdek, F. (eds.) ABZ 2020. LNCS, vol. 12071, pp. 260\u2013265. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-48077-6_21"},{"key":"10_CR15","doi-asserted-by":"publisher","unstructured":"Thomas, J.: Extending and Automating a Systems-Theoretic Hazard Analysis for Requirements Generation and Analysis. SAND2012-4080, 1044959 (2012). https:\/\/doi.org\/10.2172\/1044959","DOI":"10.2172\/1044959"},{"key":"10_CR16","unstructured":"Colley, J., Butler, M.: A Formal, Systematic Approach to STPA Using Event-B Refinement and Proof (2013). https:\/\/eprints.soton.ac.uk\/352155\/1\/STPAandEventB.pdf"},{"key":"10_CR17","doi-asserted-by":"publisher","unstructured":"Howard, G., et al.: Formal analysis of safety and security requirements of critical systems supported by an extended STPA methodology. In: 2017 IEEE European Symposium on Security and Privacy Workshops (EuroS &PW), Paris, pp. 174\u2013180. IEEE (2017). https:\/\/doi.org\/10.1109\/EuroSPW.2017.68","DOI":"10.1109\/EuroSPW.2017.68"},{"key":"10_CR18","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1504\/IJCCBS.2019.098815","volume":"9","author":"G Howard","year":"2019","unstructured":"Howard, G., et al.: A methodology for assuring the safety and security of critical infrastructure based on STPA and event-B. Int. J. Critical Comput.-Based Syst. 9, 56\u201374 (2019)","journal-title":"Int. J. Critical Comput.-Based Syst."},{"key":"10_CR19","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). https:\/\/doi.org\/10.1007\/978-3-642-10373-5_13"},{"key":"10_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"762","DOI":"10.1007\/978-3-030-30942-8_46","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"MH ter Beek","year":"2019","unstructured":"ter Beek, M.H., et al.: Adopting formal methods in an industrial setting: the railways case. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 762\u2013772. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_46"},{"key":"10_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/978-3-030-18744-6_15","volume-title":"Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification","author":"A Ferrari","year":"2019","unstructured":"Ferrari, A., et al.: Survey on formal methods and tools in railways: the ASTRail approach. In: Collart-Dutilleul, S., Lecomte, T., Romanovsky, A. (eds.) RSSRail 2019. LNCS, vol. 11495, pp. 226\u2013241. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-18744-6_15"},{"key":"10_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-030-58298-2_8","volume-title":"Formal Methods for Industrial Critical Systems","author":"M Butler","year":"2020","unstructured":"Butler, M., et al.: The first twenty-five years of industrial use of the B-method. In: ter Beek, M.H., Ni\u010dkovi\u0107, D. (eds.) FMICS 2020. LNCS, vol. 12327, pp. 189\u2013209. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-58298-2_8"},{"key":"10_CR23","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-319-68499-4_5","volume-title":"RSSRail 2017","author":"M Butler","year":"2017","unstructured":"Butler, M., et al.: Formal modelling techniques for efficient development of railway control products. In: Fantechi, A., Lecomte, T., Romanovsky, A. (eds.) RSSRail 2017. LNCS, vol. 10598, pp. 71\u201386. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68499-4_5"},{"key":"10_CR24","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-319-68499-4_10","volume-title":"RSSRail 2017","author":"M Comptier","year":"2017","unstructured":"Comptier, M., Deharbe, D., Perez, J.M., Mussat, L., Pierre, T., Sabatier, D.: Safety analysis of a CBTC system: a rigorous approach with event-B. In: Fantechi, A., Lecomte, T., Romanovsky, A. (eds.) RSSRail 2017. LNCS, vol. 10598, pp. 148\u2013159. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68499-4_10"},{"key":"10_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-319-33951-1_2","volume-title":"Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification","author":"D Sabatier","year":"2016","unstructured":"Sabatier, D.: Using formal proof and B method at system level for industrial projects. In: Lecomte, T., Pinger, R., Romanovsky, A. (eds.) RSSRail 2016. LNCS, vol. 9707, pp. 20\u201331. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33951-1_2"},{"issue":"3","key":"10_CR26","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/s10009-020-00551-6","volume":"22","author":"D Hansen","year":"2020","unstructured":"Hansen, D., et al.: Validation and real-life demonstration of ETCS hybrid level 3 principles using a formal B model. Int. J. Softw. Tools Technol. Transfer 22(3), 315\u2013332 (2020). https:\/\/doi.org\/10.1007\/s10009-020-00551-6","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"10_CR27","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-981-99-7584-6_12","volume-title":"ICFEM 2023","author":"S Stock","year":"2023","unstructured":"Stock, S., Mashkoor, A., Egyed, A.: Validation-driven development. In: Li, Y., Tahar, S. (eds.) ICFEM 2023. LNCS, vol. 14308, pp. 191\u2013207. Springer, Singapore (2023). https:\/\/doi.org\/10.1007\/978-981-99-7584-6_12"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-00942-5_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,10]],"date-time":"2025-09-10T04:40:36Z","timestamp":1757479236000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-00942-5_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,28]]},"ISBN":["9783032009418","9783032009425"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-00942-5_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025,8,28]]},"assertion":[{"value":"28 August 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FMICS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Methods for Industrial Critical Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Aarhus","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Denmark","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 August 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 August 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fmics2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/FMICS2025.uni-muenster.de","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}