{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T09:51:09Z","timestamp":1773827469494,"version":"3.50.1"},"reference-count":62,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2016,2,4]],"date-time":"2016-02-04T00:00:00Z","timestamp":1454544000000},"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":["Softw Syst Model"],"published-print":{"date-parts":[[2018,2]]},"DOI":"10.1007\/s10270-016-0517-1","type":"journal-article","created":{"date-parts":[[2016,2,4]],"date-time":"2016-02-04T10:21:57Z","timestamp":1454581317000},"page":"295-317","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Scenario-based system design with colored Petri nets: an application to train control systems"],"prefix":"10.1007","volume":"17","author":[{"given":"Daohua","family":"Wu","sequence":"first","affiliation":[]},{"given":"Eckehard","family":"Schnieder","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,2,4]]},"reference":[{"key":"517_CR1","unstructured":"Aarhus University: CPN Tools Homepage. http:\/\/cpntools.org\/ (2000)"},{"key":"517_CR2","doi-asserted-by":"crossref","unstructured":"Ameedeen, M.A., Bordbar, B.: A model driven approach to represent sequence diagrams as free choice Petri nets. In: 2008 12th International IEEE Enterprise Distributed Object Computing Conference (EDOC), pp. 213\u2013221","DOI":"10.1109\/EDOC.2008.42"},{"issue":"1","key":"517_CR3","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1023\/A:1025890110119","volume":"24","author":"D Amyot","year":"2003","unstructured":"Amyot, D., Eberlein, A.: An evaluation of scenario notations and construction approaches for telecommunication systems development. Telecommun. Syst. 24(1), 61\u201394 (2003)","journal-title":"Telecommun. Syst."},{"key":"517_CR4","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)"},{"key":"517_CR5","unstructured":"Barbu, G.: SADT for elaboration and assessment of functional specifications of GNSS supported operation on low traffic density lines. In: Proceedings of Symposium FORMS\/FORMAT 2008. L\u2019Harmattan, Budapest and Hungary (2008)"},{"key":"517_CR6","unstructured":"Bj\u00f8rner, D.: On the use of formal methods in software development. In: Proceedings of the 9th International Conference on Software Engineering, pp. 17\u201329 (1987)"},{"key":"517_CR7","unstructured":"Bj\u00f8rner, D., George, C.W., Hansen, B.S., Laustrup, H., Prehn, S.: A Railway system\u2014coordination \u201997: Case Study Workshop Example. UNU\/IIST Report No. 93 (1996)"},{"key":"517_CR8","unstructured":"CENELEC: EN 50126\u20131:1999. Railway applications\u2014the specification and demonstration of reliability, availability, maintainability and safety (RAMS)\u2014Part 1: basic requirements and generic process (1999)"},{"key":"517_CR9","unstructured":"CENELEC: EN 50128:2001. Railway applications\u2014communications, signalling and processing systems\u2014software for railway control and protection systems (2001)"},{"key":"517_CR10","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1016\/j.ress.2011.12.010","volume":"100","author":"L Chen","year":"2012","unstructured":"Chen, L., Tang, T., Zhao, X., SchniedeR, E.: Verification of the safety communication protocol in train control system using colored Petri net. Reliab. Eng. Syst. Saf. 100, 8\u201318 (2012)","journal-title":"Reliab. Eng. Syst. Saf."},{"key":"517_CR11","doi-asserted-by":"crossref","unstructured":"Cheng, A., Christensen, S., Mortensen, K.H.: Model checking coloured Petri nets exploiting strongly connected components. DAIMI report series 26(519) (1997)","DOI":"10.7146\/dpb.v26i519.7048"},{"key":"517_CR12","volume-title":"Formal Specification and Development of a Safety-Critical Train Management System. Computer Safety, Reliability and Security","author":"A Chiappini","year":"1999","unstructured":"Chiappini, A., Cimatti, A., Porzia, C., Rotondo, G., Sebastiani, R., Traverso, P., Villafiorita, A.: Formal Specification and Development of a Safety-Critical Train Management System. Computer Safety, Reliability and Security. Springer, NewYork (1999)"},{"issue":"4","key":"517_CR13","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1007\/s001650050022","volume":"10","author":"A Cimatti","year":"1998","unstructured":"Cimatti, A., Giunchiglia, F., Mongardi, G., Romano, D., Torielli, F., Traverso, P.: Formal verification of a railway interlocking system using model checking. Form. Asp. Comput. 10(4), 361\u2013380 (1998)","journal-title":"Form. Asp. Comput."},{"issue":"4","key":"517_CR14","doi-asserted-by":"crossref","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"EM Clarke","year":"1996","unstructured":"Clarke, E.M., Wing, J.M.: Formal methods: state of the art and future directions. ACM Comput. Surv. (CSUR) 28(4), 626\u2013643 (1996)","journal-title":"ACM Comput. Surv. (CSUR)"},{"key":"517_CR15","doi-asserted-by":"crossref","unstructured":"Damas, C., Lambeau, B., van Lamsweerde, A.: Scenarios, goals, and state machines: a win-win partnership for model synthesis. In: Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 197\u2013207 (2000)","DOI":"10.1145\/1181775.1181800"},{"key":"517_CR16","unstructured":"Drewes, J., May, J., SchniedeR, E., K\u00f6nig, N.: Structured approach of a generic (signalling) hazard list for railway (interlocking) systems. In: Proceedings of the 5th European Congress and Exhibition on Intelligent Transport Systems and Services. Hannover and Germany (2005)"},{"key":"517_CR17","doi-asserted-by":"crossref","unstructured":"Elkoutbi, M., Keller, R.K.: User interface prototyping based on UML scenarios and high-level Petri nets. Application Theory Petri Nets, pp. 166\u2013186. Springer, Berlin, Heidelberg (2000)","DOI":"10.1007\/3-540-44988-4_11"},{"issue":"3\u20134","key":"517_CR18","first-page":"231","volume":"47","author":"J Esparza","year":"2001","unstructured":"Esparza, J., Schr\u00f6ter, C.: Unfolding based algorithms for the reachability problem. Fundam. Inform. 47(3\u20134), 231\u2013245 (2001)","journal-title":"Fundam. Inform."},{"key":"517_CR19","unstructured":"Espensen, K.L., Kjeldsen, M.K., Kristensen, L.M., Westergaard, M.: Towards automatic code generation from process-partitioned coloured Petri nets. In: Proceedings of 10th CPN Workshop, pp. 41\u201360"},{"key":"517_CR20","doi-asserted-by":"crossref","unstructured":"Fukuda, M., Hirao, Y., Ogino, T.: VDM specification of an interlocking system and a simulator for its validation. In: Proceedings of 9th IFAC Symposium on Control in Transportation Systems 2000, pp. 187\u2013192. Braunschweig and Germany (2000)","DOI":"10.1016\/S1474-6670(17)38144-2"},{"key":"517_CR21","volume-title":"Petri Nets for Systems Engineering: A Guide to Modeling, Verification, and Applications","author":"C Girault","year":"2001","unstructured":"Girault, C., Valk, R.: Petri Nets for Systems Engineering: A Guide to Modeling, Verification, and Applications. Springer, NewYork (2001)"},{"key":"517_CR22","doi-asserted-by":"crossref","unstructured":"Hansen, K.M.: Validation of a railway interlocking model. In: FME\u201994: Industrial Benefit of Formal Methods, vol. 873, pp. 582\u2013601 (1994)","DOI":"10.1007\/3-540-58555-9_117"},{"issue":"3","key":"517_CR23","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D Harel","year":"1987","unstructured":"Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8(3), 231\u2013274 (1987)","journal-title":"Sci. Comput. Program."},{"key":"517_CR24","unstructured":"Harper, R.: Programming in Standard ML. http:\/\/www.cs.cmu.edu\/rwh\/smlbook\/book.pdf (2011)"},{"issue":"8","key":"517_CR25","doi-asserted-by":"crossref","first-page":"687","DOI":"10.1109\/32.879808","volume":"26","author":"AE Haxthausen","year":"2000","unstructured":"Haxthausen, A.E., Peleska, J.: Formal development and verification of a distributed railway control system. IEEE Trans. Softw. Eng. 26(8), 687\u2013701 (2000)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"517_CR26","doi-asserted-by":"crossref","unstructured":"Meyer zu H\u00f6rste, M.: Modelling and simulation of train control systems using Petri nets. In: FMRail Workshop, vol. 3. St. P\u00f6lten and \u00d6sterreich (1999)","DOI":"10.1007\/3-540-48118-4_58"},{"key":"517_CR27","unstructured":"Meyer zu H\u00f6rste, M., SchniedeR, E.: Modelling functionality of train control systems using Petri nets. In: FM-RAIL-BOK Workshop. Madrid (2013)"},{"key":"517_CR28","unstructured":"Meyer zu H\u00f6rste, M., Weber, I., Illgen, I., Schrom, H., SchniedeR, E.: Distributed multi-train simulation with simulators for real components. In: Proceedings of Computers in Railways VII 2000-COMPRAIL 2000, pp. 1291\u20131300. WIT Press, Bologna and Italy (2000)"},{"key":"517_CR29","unstructured":"ITU-T: Message Sequence Chart (MSC): ITU-T Rec. Z.120 (02\/2011) (2011)"},{"key":"517_CR30","doi-asserted-by":"crossref","unstructured":"Janhsen, A., Lemmer, K., Ptok, B., SchniedeR, E.: Formal specifications of the european train control system. In: Proceedings of 8th IFAC Symposium on Transportation Systems, pp. 1215\u20131220. China (1997)","DOI":"10.1016\/S1474-6670(17)43974-7"},{"key":"517_CR31","unstructured":"Janota, A., Zahradn\u00edk, J.: UML\u2014an object oriented approach to formal specification of safety relevant systems. In: 4th International Scientific Conference ELEKTRO 2001. \u017dilina and Slovak Republic (2001)"},{"key":"517_CR32","unstructured":"Jansen, L., Meyer zu H\u00f6rste, M., Schniede R.E.: Technical issues in modelling the European train control system (ETCS) using coloured petri nets and the Design\/CPN tools. In: Proceedings of the Workshop on Practical Use of Coloured Petri Nets and Design\/CPN, pp. 103\u2013115. Aarhus and Denmark (1998)"},{"key":"517_CR33","doi-asserted-by":"crossref","DOI":"10.1007\/b95112","volume-title":"Coloured Petri Nets: Modelling and Validation of Concurrent Systems","author":"K Jensen","year":"2009","unstructured":"Jensen, K., Kristensen, L.M.: Coloured Petri Nets: Modelling and Validation of Concurrent Systems. Springer, NewYork (2009)"},{"key":"517_CR34","unstructured":"Jones, C.B.: Systematic software development using VDM, vol. 2, 2nd edn. Prentice Hall Englewood Cliffs, NJ (1986)"},{"issue":"2","key":"517_CR35","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1016\/j.infsof.2008.01.005","volume":"51","author":"P Katsaros","year":"2009","unstructured":"Katsaros, P.: A roadmap to electronic payment transaction guarantees and a colored Petri net model checking approach. Inf. Softw. Technol. 51(2), 235\u2013257 (2009)","journal-title":"Inf. Softw. Technol."},{"key":"517_CR36","doi-asserted-by":"crossref","unstructured":"Khomenko, V.: Model Checking Based on Prefixes of Petri Net Unfoldings. Ph.D. thesis, University of Newcastle upon Tyne, UK (2003)","DOI":"10.1007\/3-540-45657-0_49"},{"issue":"1","key":"517_CR37","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1007\/BF01384314","volume":"6","author":"KL McMillan","year":"1995","unstructured":"McMillan, K.L.: A technique of state space search based on unfolding. Form. Methods Syst. Des. 6(1), 45\u201365 (1995)","journal-title":"Form. Methods Syst. Des."},{"key":"517_CR38","doi-asserted-by":"crossref","unstructured":"Kr\u00fcger, I., Grosu, R., Scholz, P., Broy, M.: From MSCs to statecharts. Distributed and Parallel Embedded Systems, pp. 61\u201371. Springer (1999)","DOI":"10.1007\/978-0-387-35570-2_5"},{"key":"517_CR39","first-page":"281","volume":"2002","author":"K Lautenbach","year":"2002","unstructured":"Lautenbach, K.: Reproducibility of the empty marking. Appl. Theory Petri Nets 2002, 281\u2013300 (2002)","journal-title":"Appl. Theory Petri Nets"},{"key":"517_CR40","unstructured":"Lecomte, T., Servat, T., Pouzaucre, G.: Formal methods in safety-critical railway systems. In: Proc. Brazilian Symposium on Formal Methods: SMBF (2007)"},{"key":"517_CR41","first-page":"57","volume":"3","author":"A Mirabadi","year":"2009","unstructured":"Mirabadi, A., Yazdi, M.B.: Automatic generation and verification of railway interlocking control tables using FSM and NuSMV. Signal+Draht 3, 57\u201363 (2009)","journal-title":"Signal+Draht"},{"key":"517_CR42","doi-asserted-by":"crossref","unstructured":"Mortensen, K.H.: Automatic code generation from coloured Petri nets for an access control system. In: Second Workshop on Practical Use of Coloured Petri Nets and Design\/CPN, Aarhus, Denmark, pp. 41\u201358. Citeseer (1999)","DOI":"10.7146\/dpb.v28i541.7075"},{"issue":"4","key":"517_CR43","doi-asserted-by":"crossref","first-page":"541","DOI":"10.1109\/5.24143","volume":"77","author":"T Murata","year":"1989","unstructured":"Murata, T.: Petri nets: properties, analysis and applications. Proc. IEEE 77(4), 541\u2013580 (1989)","journal-title":"Proc. IEEE"},{"issue":"1","key":"517_CR44","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/BF01887199","volume":"1","author":"M Nielsen","year":"1989","unstructured":"Nielsen, M., Havelund, K., Wagner, K.R., George, C.: The RAISE language, method and tools. Form. Asp. Comput. 1(1), 85\u2013114 (1989)","journal-title":"Form. Asp. Comput."},{"key":"517_CR45","unstructured":"Object Management Group: Unified Modeling Language. http:\/\/www.uml.org\/ (2013)"},{"key":"517_CR46","unstructured":"Object Management Group: Object Constraint Language: Version 2.4. http:\/\/www.omg.org\/spec\/OCL\/2.4\/PDF\/ (2014)"},{"key":"517_CR47","unstructured":"Object Management Group: OMG Unified Modeling Language (OMG UML), Superstructure: Version 2.2. http:\/\/www.omg.org\/spec\/UML\/2.2\/Superstructure (2009)"},{"issue":"1","key":"517_CR48","first-page":"3","volume":"5","author":"J Padberg","year":"2001","unstructured":"Padberg, J., Jansen, L., SchniedeR, E., Ehrig, H., Heckel, R.: Cooperability in train control systems: specification of scenarios using open nets. J. Integr. Des. Process Sci. 5(1), 3\u201321 (2001)","journal-title":"J. Integr. Des. Process Sci."},{"issue":"10","key":"517_CR49","doi-asserted-by":"crossref","first-page":"1444","DOI":"10.1016\/j.jss.2005.12.022","volume":"79","author":"S Philippi","year":"2006","unstructured":"Philippi, S.: Automatic code generation from high-level Petri-nets for model driven systems engineering. J. Syst. Softw. 79(10), 1444\u20131455 (2006)","journal-title":"J. Syst. Softw."},{"key":"517_CR50","unstructured":"Pope, M., Drewes, J., May, J.: Generic hazard list for railway systems. In: 7th World Congress on Railway Research\u2014WCRR 2006. Montr\u00e9al and Canada (2006)"},{"key":"517_CR51","doi-asserted-by":"crossref","unstructured":"R\u00e1sto\u010dn\u00fd, K., Janota, A., Zahradn\u00edk, J.: The use of UML for development of a railway interlocking system. In: Integration of Software Specification Techniques for Applications in Engineering, Lecture Notes in Computer Science, vol. 3147, pp. 174\u2013198. Springer (2004)","DOI":"10.1007\/978-3-540-27863-4_11"},{"key":"517_CR52","doi-asserted-by":"crossref","unstructured":"Ross, D.T.: Structured analysis (SA): a language for communicating ideas. IEEE Trans. Softw. Eng. (1), 16\u201334 (1977)","DOI":"10.1109\/TSE.1977.229900"},{"key":"517_CR53","unstructured":"Stadlmann, B.: Systematic UML-design used in the development of a basic train control system for regional branch lines. In: FORMS\/FORMAT 2004, pp. 71\u201378. Beyrich DigitalService, Germany (2004)"},{"key":"517_CR54","first-page":"28","volume":"5","author":"B Stadlmann","year":"2012","unstructured":"Stadlmann, B., Kaiser, F., Maihofer, S.: Rechnergest\u00fctztes Zugleitsystem f\u00fcr die Pinzgauer Lokalbahn. Signal+Draht 5, 28\u201333 (2012)","journal-title":"Signal+Draht"},{"key":"517_CR55","doi-asserted-by":"crossref","unstructured":"Tretmans, J.: Model Based Testing with Labelled Transition Systems, Lecture Notes in Computer Science, vol. 4949. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-78917-8_1"},{"issue":"2","key":"517_CR56","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1109\/TSE.2003.1178048","volume":"29","author":"S Uchitel","year":"2003","unstructured":"Uchitel, S., Kramer, J., Magee, J.: Synthesis of behavioral models from scenarios. IEEE Trans. Softw. Eng. 29(2), 99\u2013115 (2003)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"3","key":"517_CR57","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1656250.1656252","volume":"19","author":"J Whittle","year":"2010","unstructured":"Whittle, J., Jayaraman, P.K.: Synthesizing hierarchical state machines from expressive scenario descriptions. ACM Trans. Softw. Eng. Methodol. 19(3), 1\u201345 (2010)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"517_CR58","doi-asserted-by":"crossref","unstructured":"Whittle, J., Schumann, J.: Generating statechart designs from scenarios. In: Proceedings of the 2000 International Conference on Software Engineering, pp. 314\u2013323 (2000)","DOI":"10.1145\/337180.337217"},{"key":"517_CR59","unstructured":"Winter, K., Robinson, N.J.: Modelling large railway interlockings and model checking small ones. In: Proceedings of the 26th Australasian Computer Science Conference. Vol. 16, pp. 309\u2013316 (2003)"},{"key":"517_CR60","unstructured":"Wu, D.: Verifiable Design of a Satellite-based Train Control System with Petri Nets. Ph.D. thesis, Technische Universit\u00e4t Braunschweig, Braunschweig and Germany (2014)"},{"key":"517_CR61","doi-asserted-by":"crossref","unstructured":"Wu, D., SchniedeR, E., Lu, D., Manz, H.: Realistic modelling of train control system with coloured Petri nets. In: Proceedings of 13th IFAC Symposium on Control in Transportation Systems (CTS 2012), vol. 13, pp. 19\u201323. Sofia and Bulgaria (2012)","DOI":"10.3182\/20120912-3-BG-2031.00004"},{"issue":"6","key":"517_CR62","doi-asserted-by":"crossref","first-page":"567","DOI":"10.1109\/41.334574","volume":"41","author":"R Zurawski","year":"1994","unstructured":"Zurawski, R., Zhou, M.: Petri nets and industrial applications: a tutorial. IEEE Trans. Ind. Electron. 41(6), 567\u2013583 (1994)","journal-title":"IEEE Trans. Ind. Electron."}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-016-0517-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-016-0517-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-016-0517-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-016-0517-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T09:09:06Z","timestamp":1748768946000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-016-0517-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,2,4]]},"references-count":62,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2018,2]]}},"alternative-id":["517"],"URL":"https:\/\/doi.org\/10.1007\/s10270-016-0517-1","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,2,4]]}}}