{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,8]],"date-time":"2025-11-08T22:41:32Z","timestamp":1762641692177,"version":"3.40.4"},"reference-count":48,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2014,5,27]],"date-time":"2014-05-27T00:00:00Z","timestamp":1401148800000},"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":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2014,8]]},"DOI":"10.1007\/s10009-014-0318-1","type":"journal-article","created":{"date-parts":[[2014,5,26]],"date-time":"2014-05-26T18:26:51Z","timestamp":1401128811000},"page":"339-361","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Formal verification and simulation for platform screen doors and collision avoidance in subway control systems"],"prefix":"10.1007","volume":"16","author":[{"given":"Huixing","family":"Fang","sequence":"first","affiliation":[]},{"given":"Jianqi","family":"Shi","sequence":"additional","affiliation":[]},{"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[]},{"given":"Jian","family":"Guo","sequence":"additional","affiliation":[]},{"given":"Kim Guldstrand","family":"Larsen","sequence":"additional","affiliation":[]},{"given":"Alexandre","family":"David","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,5,27]]},"reference":[{"key":"318_CR1","volume-title":"The B-book: Assigning Programs to Meanings","author":"J-R Abrial","year":"2005","unstructured":"Abrial, J.-R.: The B-book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)"},{"key":"318_CR2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"J-R Abrial","year":"2010","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)"},{"key":"318_CR3","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R., Lee, M., Neilson, D., Scharbach, P., S\u00c3rensen, I.: The b-method. In: Proceedings of VDM, LNCS, vol. 552, pp. 398\u2013405. Springer-Verlag, Berlin (1991)","DOI":"10.1007\/BFb0020001"},{"key":"318_CR4","unstructured":"Accellera Orgnization: Property specification language reference. http:\/\/www.eda.org\/vfv\/docs\/psl_lrm-1.01.pdf (2003). Accessed 25 Apr 2003"},{"key":"318_CR5","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1016\/j.entcs.2004.02.055","volume":"109","author":"A Agrawal","year":"2004","unstructured":"Agrawal, A., Simon, G., Karsai, G.: Semantic translation of simulink\/stateflow models to hybrid automata using graph transformations. Electron. Notes. Theor. Comput. Sci. 109, 43\u201356 (2004)","journal-title":"Electron. Notes. Theor. Comput. Sci."},{"key":"318_CR6","doi-asserted-by":"crossref","unstructured":"Alur, R., Courcoubetis, C., Henzinger, T., Ho, P.: Hybrid automata: an algorithmic approach to the specification and analysis of hybrid systems. In: Hybrid Systems, LNCS, vol. 736, pp. 209\u2013229. Springer-Verlag, Berlin (1993)","DOI":"10.1007\/3-540-57318-6_30"},{"issue":"3","key":"318_CR7","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1109\/32.489079","volume":"22","author":"R Alur","year":"1996","unstructured":"Alur, R., Henzinger, T., Ho, P.: Automatic symbolic verification of embedded systems. IEEE Trans. Softw. Eng. 22(3), 181\u2013201 (1996)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"318_CR8","doi-asserted-by":"crossref","unstructured":"Asarin, E., Bournez, O., Dang, T., Maler, O.: Approximate reachability analysis of piecewise-linear dynamical systems. In: Proceedings of HSCC, LNCS, vol. 1790, pp. 20\u201331. Springer-Verlag, Berlin (2000)","DOI":"10.1007\/3-540-46430-1_6"},{"key":"318_CR9","doi-asserted-by":"crossref","unstructured":"Asarin, E., Dang, T., Maler, O., Testylier, R.: Using redundant constraints for refinement. In: Proceedings of ATVA, LNCS, vol. 6252, pp. 37\u201351. Springer-Verlag, Berlin (2010)","DOI":"10.1007\/978-3-642-15643-4_5"},{"key":"318_CR10","doi-asserted-by":"crossref","unstructured":"Bagnara, R., Ricci, E., Zaffanella, E., Hill, P.: Possibly not closed convex polyhedra and the parma polyhedra library. In: Proceedings of SAS, LNCS, vol. 2477, pp. 299\u2013315. Springer-Verlag, Berlin (2002)","DOI":"10.1007\/3-540-45789-5_17"},{"key":"318_CR11","doi-asserted-by":"crossref","unstructured":"Bloem, R., Cimatti, A., Greimel, K., Hofferek, G., K\u00f6nighofer, R., Roveri, M., Schuppan, V., Seeber, R.: Ratsy-a new requirements analysis tool with synthesis. In: Proceedings of CAV, pp. 425\u2013429. Springer-Verlag, Berlin (2010)","DOI":"10.1007\/978-3-642-14295-6_37"},{"key":"318_CR12","doi-asserted-by":"crossref","DOI":"10.1142\/p373","volume-title":"Practical Railway Engineering","author":"C Bonnett","year":"2005","unstructured":"Bonnett, C.: Practical Railway Engineering. Imperial College Press, London (2005)"},{"key":"318_CR13","unstructured":"ClearSy: http:\/\/www.clearsy.com\/en\/ (2011\u20132013). Accessed 1 July 2013"},{"key":"318_CR14","unstructured":"ClearSy: COPPILOT System. http:\/\/www.coppilot.fr\/en\/coppilot\/ (2011\u20132013). Accessed 1 July 2013"},{"key":"318_CR15","unstructured":"ClearSy: Tools and applications at ClearSy. http:\/\/www.tools.clearsy.com (2011\u20132013). Accessed 21 Aug 2013"},{"key":"318_CR16","doi-asserted-by":"crossref","unstructured":"Doyen, L., Henzinger, T., Raskin, J.: Automatic rectangular refinement of affine hybrid systems. In: Proceedings of FORMATS, LNCS, vol. 3829, pp. 144\u2013161. Springer-Verlag, Berlin (2005)","DOI":"10.1007\/11603009_13"},{"issue":"7","key":"318_CR17","doi-asserted-by":"crossref","first-page":"828","DOI":"10.1016\/j.scico.2012.04.003","volume":"78","author":"A Ferrari","year":"2012","unstructured":"Ferrari, A., Fantechi, A., Magnani, G., Grasso, D., Tempestini, M.: The metr\u00f4 rio case study. Sci. Comput. Program. 78(7), 828\u2013842 (2012)","journal-title":"Sci. Comput. Program."},{"key":"318_CR18","doi-asserted-by":"crossref","unstructured":"Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. In: Proceedings of HSCC, LNCS, vol. 3414, pp. 258\u2013273. Springer-Verlag, Berlin (2005)","DOI":"10.1007\/978-3-540-31954-2_17"},{"key":"318_CR19","unstructured":"Frehse, G.: Language Overview for PHAVer version 0.35. http:\/\/www.cs.ru.nl\/~goranf\/ (2006). Accessed 22 June 2006"},{"issue":"3","key":"318_CR20","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/s10009-007-0062-x","volume":"10","author":"G Frehse","year":"2008","unstructured":"Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. Int. J. Softw. Tools. Technol. Transf. 10(3), 263\u2013279 (2008)","journal-title":"Int. J. Softw. Tools. Technol. Transf."},{"key":"318_CR21","doi-asserted-by":"crossref","unstructured":"Frehse, G., Le Guernic, C., Donz\u00e9, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: scalable verification of hybrid systems. In: Proceedings of CAV, LNCS, vol. 6806, pp. 379\u2013395. Springer-Verlag, Berlin (2011)","DOI":"10.1007\/978-3-642-22110-1_30"},{"key":"318_CR22","doi-asserted-by":"crossref","unstructured":"Girard, A., Le Guernic, C.: Zonotope\/hyperplane intersection for hybrid systems reachability analysis. In: Proceedings of HSCC, LNCS, vol. 4981, pp. 215\u2013228. Springer-Verlag, Berlin (2008)","DOI":"10.1007\/978-3-540-78929-1_16"},{"key":"318_CR23","unstructured":"Granlund, T., Ryde, K.: The GNU Multiple Precision Arithmetic Library Version 4 (2001)"},{"key":"318_CR24","doi-asserted-by":"crossref","unstructured":"Halbwachs, N., Proy, Y., Raymond, P.: Verification of linear hybrid systems by means of convex approximations. In: Proceedings of SAS, LNCS, vol. 864, pp. 223\u2013237. Springer-Verlag, Berlin (1994)","DOI":"10.1007\/3-540-58485-4_43"},{"key":"318_CR25","doi-asserted-by":"crossref","unstructured":"Hamon, G.: A denotational semantics for stateflow. In: Proceedings of EMSOFT, pp. 164\u2013172. ACM, New York (2005)","DOI":"10.1145\/1086228.1086260"},{"issue":"5\u20136","key":"318_CR26","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1007\/s10009-007-0049-7","volume":"9","author":"G Hamon","year":"2007","unstructured":"Hamon, G., Rushby, J.: An operational semantics for stateflow. Int. J. Softw. Tools. Technol. Transf. 9(5\u20136), 447\u2013456 (2007)","journal-title":"Int. J. Softw. Tools. Technol. Transf."},{"issue":"3","key":"318_CR27","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."},{"issue":"4","key":"318_CR28","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/235321.235322","volume":"5","author":"D Harel","year":"1996","unstructured":"Harel, D., Naamad, A.: The statemate semantics of statecharts. ACM Trans. Softw. Eng. Methodol. 5(4), 293\u2013333 (1996)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"issue":"1\u20132","key":"318_CR29","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"T Henzinger","year":"1997","unstructured":"Henzinger, T., Ho, P., Wong-Toi, H.: Hytech: a model checker for hybrid systems. Int. J. Softw. Tools. Technol. Transf. 1(1\u20132), 110\u2013122 (1997)","journal-title":"Int. J. Softw. Tools. Technol. Transf."},{"issue":"1","key":"318_CR30","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1006\/jcss.1998.1581","volume":"57","author":"T Henzinger","year":"1998","unstructured":"Henzinger, T., Kopke, P., Puri, A., Varaiya, P.: What\u2019s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94\u2013124 (1998)","journal-title":"J. Comput. Syst. Sci."},{"key":"318_CR31","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: Proceedings of LICS, pp. 278\u2013292. IEEE Computer Society, Washington, D.C. (1996)","DOI":"10.1109\/LICS.1996.561342"},{"key":"318_CR32","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511574924","volume-title":"The Way of Z: Practical Programming with Formal Methods","author":"J Jacky","year":"1996","unstructured":"Jacky, J.: The Way of Z: Practical Programming with Formal Methods. Cambridge University Press, Cambridge (1996)"},{"key":"318_CR33","unstructured":"Jo H.-J., Hwang J.-G., Yong Y.-K.: Development of formal method application for ensuring safety in train control system. http:\/\/www.railway-research.org\/IMG\/pdf\/o.3.4.2.3.pdf (2008)"},{"key":"318_CR34","doi-asserted-by":"crossref","unstructured":"Kurzhanski, A.B., Varaiya, P.: Ellipsoidal techniques for reachability analysis. In: Proceedings of HSCC, LNCS, vol. 1790, pp. 202\u2013214. Springer-Verlag, Berlin (2000)","DOI":"10.1007\/3-540-46430-1_19"},{"issue":"2","key":"318_CR35","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1016\/j.nahs.2009.03.002","volume":"4","author":"C Guernic Le","year":"2010","unstructured":"Le Guernic, C., Girard, A.: Reachability analysis of linear systems using support functions. Nonlinear Anal. Hybrid Syst. 4(2), 250\u2013262 (2010)","journal-title":"Nonlinear Anal. Hybrid Syst."},{"key":"318_CR36","doi-asserted-by":"crossref","unstructured":"Lecomte, T.: Safe and reliable metro platform screen doors control\/command systems. In: Proceedings of FM, LNCS, vol. 5014, pp. 430\u2013434. Springer-Verlag, Berlin (2008)","DOI":"10.1007\/978-3-540-68237-0_32"},{"key":"318_CR37","doi-asserted-by":"crossref","unstructured":"Lecomte, T.: Applying a formal method in industry: a 15-year trajectory. In: Proceedings of FMICS, LNCS, vol. 5825, pp. 26\u201334. Springer-Verlag, Berlin (2009)","DOI":"10.1007\/978-3-642-04570-7_3"},{"issue":"1","key":"318_CR38","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1996.0060","volume":"128","author":"NA Lynch","year":"1996","unstructured":"Lynch, N.A., Vaandrager, F.W.: Forward and backward simulations, ii: timing-based systems. Inf. Comput. 128(1), 1\u201325 (1996)","journal-title":"Inf. Comput."},{"key":"318_CR39","doi-asserted-by":"crossref","unstructured":"Marrone, S., Nardone, R., Orazzo, A., Petrone, I., Velardi, L.: Improving verification process in driverless metro systems: the mbat project. In: Proceedings of ISoLA, LNCS, vol. 7610, pp. 231\u2013245. Springer-Verlag, Berlin (2012)","DOI":"10.1007\/978-3-642-34032-1_23"},{"key":"318_CR40","unstructured":"MBAT Consortium: ARTEMIS Project MBAT. http:\/\/www.mbat-artemis.eu (2011\u20132014). Accessed 1 July 2013"},{"key":"318_CR41","unstructured":"National Institute of Standards and Technology (NIST): Fire dynamics simulator and smokeview code. http:\/\/code.google.com\/p\/fds-smv\/ (2012\u20132013). Accessed 5 Mar 2014"},{"key":"318_CR42","doi-asserted-by":"crossref","unstructured":"Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: An approach to the description and analysis of hybrid systems. In: Proceedings of Hybrid Systems, LNCS, vol. 736, pp. 149\u2013178. Springer-Verlag, Berlin (1993)","DOI":"10.1007\/3-540-57318-6_28"},{"issue":"2","key":"318_CR43","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1007\/s10009-005-0205-x","volume":"8","author":"I Ober","year":"2006","unstructured":"Ober, I., Graf, S., Ober, I.: Validating timed uml models by simulation and verification. Int. J. Softw. Tools. Technol. Transf. 8(2), 128\u2013145 (2006)","journal-title":"Int. J. Softw. Tools. Technol. Transf."},{"key":"318_CR44","first-page":"526","volume":"3414","author":"A Pinto","year":"2005","unstructured":"Pinto, A., Sangiovanni-Vincentelli, A.L., Carloni, L.P., Passerone, R.: Interchange formats for hybrid systems: review and proposal. Proc. HSCC LNCS 3414, 526\u2013541 (2005)","journal-title":"Proc. HSCC LNCS"},{"key":"318_CR45","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.tust.2011.09.003","volume":"30","author":"L Qu","year":"2012","unstructured":"Qu, L., Chow, W.: Platform screen doors on emergency evacuation in underground railway stations. Tunn. Undergr. Space Technol. 30, 1\u20139 (2012)","journal-title":"Tunn. Undergr. Space Technol."},{"issue":"4","key":"318_CR46","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1016\/j.tust.2008.12.003","volume":"24","author":"JS Roh","year":"2009","unstructured":"Roh, J.S., Ryou, H.S., Park, W.H., Jang, Y.J.: Cfd simulation and assessment of life safety in a subway train fire. Tunn. Undergr. Space Technol. 24(4), 447\u2013453 (2009)","journal-title":"Tunn. Undergr. Space Technol."},{"key":"318_CR47","doi-asserted-by":"crossref","unstructured":"Su, W., Abrial, J.-R., Zhu, H.: Complementary methodologies for developing hybrid systems with event-b. In: Proceedings of ICFEM, LNCS, vol. 7635. Springer-Verlag, Berlin (2012)","DOI":"10.1007\/978-3-642-34281-3_18"},{"issue":"3","key":"318_CR48","first-page":"915","volume":"9","author":"L Zhao","year":"2013","unstructured":"Zhao, L., Tang, T., Cheng, R., He, L.: Property based requirements analysis for train control system. J. Comput. Inf. Syst. 9(3), 915\u2013922 (2013)","journal-title":"J. Comput. Inf. Syst."}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0318-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-014-0318-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0318-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T03:25:14Z","timestamp":1746242714000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-014-0318-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,5,27]]},"references-count":48,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2014,8]]}},"alternative-id":["318"],"URL":"https:\/\/doi.org\/10.1007\/s10009-014-0318-1","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2014,5,27]]}}}