乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T09:18:36Z","timestamp":1725527916973},"reference-count":72,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2018,3,8]],"date-time":"2018-03-08T00:00:00Z","timestamp":1520467200000},"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":[[2018,6]]},"DOI":"10.1007\/s10009-018-0488-3","type":"journal-article","created":{"date-parts":[[2018,3,8]],"date-time":"2018-03-08T12:45:32Z","timestamp":1520513132000},"page":"263-288","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":27,"title":["Towards formal methods diversity in railways: an experience report with seven frameworks"],"prefix":"10.1007","volume":"20","author":[{"given":"Franco","family":"Mazzanti","sequence":"first","affiliation":[]},{"given":"Alessio","family":"Ferrari","sequence":"additional","affiliation":[]},{"given":"Giorgio O.","family":"Spagnolo","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,3,8]]},"reference":[{"key":"488_CR1","unstructured":"1850-2010\u2014IEEE Standard for Property Specification Language (PSL). http:\/\/ieeexplore.ieee.org\/servlet\/opac?punumber=5445949 . Accessed 7 Mar 2018"},{"key":"488_CR2","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":"488_CR3","doi-asserted-by":"crossref","unstructured":"Amrani, M., Lucio, L., Selim, G., Combemale, B., Dingel, J., Vangheluwe, H., Le Traon, Y., Cordy, J.R.: A tridimensional approach for studying the formal verification of model transformations. In: 2012 IEEE Fifth International Conference on Software Testing, Verification and Validation (ICST), pp. 921\u2013928. IEEE (2012)","DOI":"10.1109\/ICST.2012.197"},{"key":"488_CR4","doi-asserted-by":"crossref","unstructured":"Antoni, M., Ammad, N.: Formal validation method and tools for French computerized railway interlocking systems. In: IET Conference Proceedings\u20144th IET International Conference on Railway Condition Monitoring (RCM 2008), pp. 6\u20136(10) (2008)","DOI":"10.1049\/ic:20080313"},{"key":"488_CR5","unstructured":"Arnold, A., Gaudel, M.C., Marre, B.: An experiment on the validation of a specification by heterogeneous formal means: the transit node. In: 5th IFIP Working Conference on Dependable Computing for Critical Applications (DCCA5), pp. 24\u201334 (1995)"},{"key":"488_CR6","doi-asserted-by":"publisher","first-page":"1491","DOI":"10.1109\/TSE.1985.231893","volume":"12","author":"A Avizienis","year":"1985","unstructured":"Avizienis, A.: The N-version approach to fault-tolerant software. IEEE Trans. Softw. Eng. 12, 1491\u20131501 (1985)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"488_CR7","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., Havel, V., Havl\u00ed\u010dek, J., Kriho, J., Len\u010do, M., Ro\u010dkai, P., \u0160till, V., Weiser, J.: DiVinE 3.0\u2014an explicit-state model checker for multithreaded C & C++ programs. In: International Conference on Computer Aided Verification, pp. 863\u2013868. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_60"},{"key":"488_CR8","doi-asserted-by":"crossref","unstructured":"Behm, P., Benoit, P., Faivre, A., Meynadier, J.M.: METEOR: a successful application of B in a large project. In: International Symposium on Formal Methods, pp. 369\u2013387. Springer (1999)","DOI":"10.1007\/3-540-48119-2_22"},{"key":"488_CR9","doi-asserted-by":"crossref","unstructured":"Benaissa, N., Bonvoisin, D., Feliachi, A., Ordioni, J.: The PERF approach for formal verification. In: International Conference on Reliability, Safety and Security of Railway Systems, pp. 203\u2013214. Springer (2016)","DOI":"10.1007\/978-3-319-33951-1_15"},{"key":"488_CR10","doi-asserted-by":"crossref","unstructured":"BBlom, S., van de Pol, J., Weber, M.: LTSmin: distributed and symbolic reachability. In: International Conference on Computer Aided Verification, pp. 354\u2013359. Springer (2010)","DOI":"10.1007\/978-3-642-14295-6_31"},{"key":"488_CR11","doi-asserted-by":"crossref","unstructured":"Bonacchi, A., Fantechi, A., Bacherini, S., Tempestini, M., Cipriani, L.: Validation of railway interlocking systems by formal verification, a case study. In: International Conference on Software Engineering and Formal Methods, pp. 237\u2013252. Springer (2013)","DOI":"10.1007\/978-3-319-05032-4_18"},{"issue":"2","key":"488_CR12","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1109\/32.44387","volume":"16","author":"SS Brilliant","year":"1990","unstructured":"Brilliant, S.S., Knight, J.C., Leveson, N.G.: Analysis of faults in an n-version software experiment. IEEE Trans. Softw. Eng. 16(2), 238\u2013247 (1990)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"488_CR13","unstructured":"CENELEC. EN 50128:2011: Railway Applications\u2014Communication, Signalling and Processing Systems\u2014Software for Railway Control and Protection Systems. Technical Report (2011)"},{"key":"488_CR14","doi-asserted-by":"crossref","unstructured":"Chiappini, A., Cimatti, A., Macchi, L., Rebollo, O., Roveri, M., Susi, A., Tonetta, S., Vittorini, B.: Formalization and validation of a subset of the European train control system. In: 2010 ACM\/IEEE 32nd International Conference on Software Engineering, vol.\u00a02, pp. 109\u2013118. IEEE (2010)","DOI":"10.1145\/1810295.1810312"},{"key":"488_CR15","unstructured":"Cho, C.H., Choi, D.H., Quan, Z.H., Choi, S.A., Park, G.S., Ryou, M.S.: Modeling of CBTC carborne ATO functions using SCADE. In: 2011 11th International Conference on Control, Automation and Systems (ICCAS), pp. 1089\u20131093. IEEE (2011)"},{"key":"488_CR16","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: Nusmv 2: an opensource tool for symbolic model checking. In: International Conference on Computer Aided Verification, pp. 359\u2013364. Springer (2002)","DOI":"10.1007\/3-540-45657-0_29"},{"key":"488_CR17","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"488_CR18","unstructured":"DaSilva, C., Dehbonei, B., Mejia, F.: Formal specification in the development of industrial applications: subway speed control system. In: Proceedings of the IFIP TC6\/WG6. 1 Fifth International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols: Formal Description Techniques, V, pp. 199\u2013213. North-Holland Publishing Co. (1992)"},{"issue":"1\u20132","key":"488_CR19","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/0304-3975(84)90113-0","volume":"34","author":"R Nicola De","year":"1984","unstructured":"De Nicola, R., Hennessy, M.C.B.: Testing equivalences for processes. Theor. Comput. Sci. 34(1\u20132), 83\u2013133 (1984)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"488_CR20","doi-asserted-by":"publisher","first-page":"458","DOI":"10.1145\/201019.201032","volume":"42","author":"R Nicola De","year":"1995","unstructured":"De Nicola, R., Vaandrager, F.: Three logics for branching bisimulation. J. ACM (JACM) 42(2), 458\u2013487 (1995)","journal-title":"J. ACM (JACM)"},{"key":"488_CR21","doi-asserted-by":"crossref","unstructured":"Dong, J., Chen, S., Jeng, J-J.: Event-based blackboard architecture for multi-agent systems. In: International Conference on Information Technology: Coding and Computing, 2005. ITCC 2005, vol.\u00a02, pp. 379\u2013384. IEEE (2005)","DOI":"10.1109\/ITCC.2005.149"},{"key":"488_CR22","unstructured":"Dormoy, F.-X.: Scade 6: a model based solution for safety critical software development. In: Proceedings of the 4th European Congress on Embedded Real Time Software (ERTS08), pp. 1\u20139 (2008)"},{"key":"488_CR23","doi-asserted-by":"crossref","unstructured":"D\u2019silva, Vijay, Kroening, Daniel, Weissenbacher, Georg: A survey of automated techniques for formal software verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 27(7), 1165\u20131178, (2008)","DOI":"10.1109\/TCAD.2008.923410"},{"key":"488_CR24","doi-asserted-by":"crossref","unstructured":"Fantechi, Alessandro: Twenty-five years of formal methods and railways: what next? In International Conference on Software Engineering and Formal Methods, pp. 167\u2013183. Springer, (2013)","DOI":"10.1007\/978-3-319-05032-4_13"},{"issue":"3","key":"488_CR25","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1145\/2211616.2211619","volume":"21","author":"A Fantechi","year":"2012","unstructured":"Fantechi, A., Gnesi, S., Lapadula, A., Mazzanti, F., Pugliese, R., Tiezzi, F.: A logical verification methodology for service-oriented computing. ACM Transactions on Software Engineering and Methodology (TOSEM) 21(3), 16 (2012)","journal-title":"ACM Transactions on Software Engineering and Methodology (TOSEM)"},{"key":"488_CR26","doi-asserted-by":"crossref","unstructured":"Ferrari, A., Fantechi, A., Gnesi, S.: Lessons learnt from the adoption of formal model-based development. In: Goodloe, A.E., Person, S. (eds.) NASA Formal Methods Symposium (NFM 2012). Lecture Notes in Computer Science, vol 7226. Springer, Berlin, pp. 24\u201338 (2012)","DOI":"10.1007\/978-3-642-28891-3_5"},{"issue":"3","key":"488_CR27","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1109\/MS.2013.44","volume":"30","author":"A Ferrari","year":"2013","unstructured":"Ferrari, A., Fantechi, A., Gnesi, S., Magnani, G.: Model-based development and formal methods in the railway industry. IEEE Softw. 30(3), 28\u201334 (2013)","journal-title":"IEEE Softw."},{"issue":"7","key":"488_CR28","doi-asserted-by":"publisher","first-page":"828","DOI":"10.1016\/j.scico.2012.04.003","volume":"78","author":"A Ferrari","year":"2013","unstructured":"Ferrari, A., Fantechi, A., Magnani, G., Grasso, D., Tempestini, M.: The metr\u00f4 rio case study. Sci. Comput. Program. 78(7), 828\u2013842 (2013)","journal-title":"Sci. Comput. Program."},{"key":"488_CR29","doi-asserted-by":"crossref","unstructured":"Ferrari, A., Magnani, G., Grasso, D., Fantechi, A.: Model checking interlocking control tables. In: FORMS\/FORMAT 2010, pp. 107\u2013115. Springer, (2011)","DOI":"10.1007\/978-3-642-14261-1_11"},{"issue":"6","key":"488_CR30","doi-asserted-by":"publisher","first-page":"647","DOI":"10.1007\/s10009-013-0298-6","volume":"16","author":"A Ferrari","year":"2014","unstructured":"Ferrari, A., Spagnolo, G.O., Martelli, G., Menabeni, S.: From commercial documents to system requirements: an approach for the engineering of novel CBTC solutions. Int. J. Softw. Tools Technol. Transf. 16(6), 647\u2013667 (2014)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"488_CR31","doi-asserted-by":"crossref","unstructured":"Fitzgerald, J., Larsen, P.G.: Balancing insight and effort: the industrial uptake of formal methods. In: Formal Methods and Hybrid Real-Time Systems, pp. 237\u2013254. Springer (2007)","DOI":"10.1007\/978-3-540-75221-9_10"},{"key":"488_CR32","doi-asserted-by":"crossref","unstructured":"Frappier, M., Fraikin, B., Chossart, R., Chane-Yack-Fa, R., Ouenzar, M.: Comparison of model checking tools for information systems. In: International Conference on Formal Engineering Methods, pp. 581\u2013596. Springer (2010)","DOI":"10.1007\/978-3-642-16901-4_38"},{"issue":"2","key":"488_CR33","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/s10009-012-0244-z","volume":"15","author":"H Garavel","year":"2013","unstructured":"Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. STTT 15(2), 89\u2013107 (2013)","journal-title":"STTT"},{"key":"488_CR34","doi-asserted-by":"crossref","unstructured":"Garavel, H., Lang, F., Serwe, W.: From LOTOS to LNT. In: ModelEd, TestEd, TrustEd\u2014Essays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday, volume 10500 of Lecture Notes in Computer Science, pp. 3\u201326. Springer (2017)","DOI":"10.1007\/978-3-319-68270-9_1"},{"key":"488_CR35","doi-asserted-by":"crossref","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3A modern refinement checker for CSP. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 187\u2013201. Springer (2014)","DOI":"10.1007\/978-3-642-54862-8_13"},{"key":"488_CR36","doi-asserted-by":"publisher","DOI":"10.1002\/9781118459898","volume-title":"Formal Methods for Industrial Critical Systems: A Survey of Applications","author":"S Gnesi","year":"2012","unstructured":"Gnesi, S., Margaria, T.: Formal Methods for Industrial Critical Systems: A Survey of Applications. Wiley, Hoboken (2012)"},{"key":"488_CR37","doi-asserted-by":"crossref","unstructured":"Gnesi, S., Mazzanti, F.: An abstract, on the fly framework for the verification of service-oriented systems. In: Rigorous Software Engineering for Service-Oriented Systems, volume 6582 of LNCS, pp. 390\u2013407. Springer (2011)","DOI":"10.1007\/978-3-642-20401-2_18"},{"key":"488_CR38","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/9946.001.0001","volume-title":"Modeling and Analysis of Communicating Systems","author":"JF Groote","year":"2014","unstructured":"Groote, J.F., Mousavi, M.R.: Modeling and Analysis of Communicating Systems. MIT Press, Cambridge (2014)"},{"key":"488_CR39","doi-asserted-by":"crossref","unstructured":"Gruner, S., Kumar, A., Maibaum, T.: Towards a body of knowledge in formal methods for the railway domain: identification of settled knowledge. In: International Workshop on Formal Techniques for Safety-Critical Systems, pp. 87\u2013102. Springer (2015)","DOI":"10.1007\/978-3-319-29510-7_5"},{"issue":"3","key":"488_CR40","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1109\/52.896248","volume":"17","author":"CA Gunter","year":"2000","unstructured":"Gunter, C.A., Gunter, E.L., Jackson, M., Zave, P.: A reference model for requirements and specifications. IEEE Softw. 17(3), 37\u201343 (2000)","journal-title":"IEEE Softw."},{"issue":"9","key":"488_CR41","doi-asserted-by":"publisher","first-page":"1305","DOI":"10.1109\/5.97300","volume":"79","author":"N Halbwachs","year":"1991","unstructured":"Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous data flow programming language LUSTRE. Proc. IEEE 79(9), 1305\u20131320 (1991)","journal-title":"Proc. IEEE"},{"key":"488_CR42","unstructured":"Hamon, G., Dutertre, B., Erkok, L., Matthews, J., Sheridan, D., Cok, D., Rushby, J., Bokor, P., Shukla, S., Pataricza, A., et\u00a0al.: Simulink design verifier-applying automated formal methods to simulink and stateflow. In: AFM08: Third Workshop on Automated Formal Methods, 14 July 2008, Princeton, New Jersey (2008)"},{"issue":"4","key":"488_CR43","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K Havelund","year":"2000","unstructured":"Havelund, K., Pressburger, T.: Model checking java programs using java pathfinder. Int. J. Softw. Tools Technol. Transf. (STTT) 2(4), 366\u2013381 (2000)","journal-title":"Int. J. Softw. Tools Technol. Transf. (STTT)"},{"issue":"6","key":"488_CR44","doi-asserted-by":"publisher","first-page":"713","DOI":"10.1007\/s10009-013-0295-9","volume":"16","author":"AE Haxthausen","year":"2014","unstructured":"Haxthausen, A.E.: Automated generation of formal safety conditions from railway interlocking tables. Int. J. Softw. Tools Technol. Transf. 16(6), 713\u2013726 (2014)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"488_CR45","doi-asserted-by":"publisher","unstructured":"Hoare, C.A.R.: Communicating sequential processes. In: Hansen, P.B. (ed.) The Origin of Concurrent Programming. Springer, New York, NY (1978). https:\/\/doi.org\/10.1007\/978-1-4757-3472-0_16","DOI":"10.1007\/978-1-4757-3472-0_16"},{"key":"488_CR46","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"G Holzmann","year":"2003","unstructured":"Holzmann, G.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley Professional, Boston (2003)"},{"key":"488_CR47","doi-asserted-by":"crossref","unstructured":"Hordvik, S., \u00d8seth, K., Blech, J.O., Herrmann, P.: A methodology for model-based development and safety analysis of transport systems. In: 11th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE) (2016)","DOI":"10.1007\/978-3-319-56390-9_3"},{"key":"488_CR48","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"D Jackson","year":"2012","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2012)"},{"key":"488_CR49","doi-asserted-by":"crossref","unstructured":"James, P., Lawrence, A., Moller, F., Roggenbach, M., Seisenberger, M., Setzer, A., Kanso, K., Chadwick, S.: Verification of solid state interlocking programs. In: International Conference on Software Engineering and Formal Methods, pp. 253\u2013268. Springer (2013)","DOI":"10.1007\/978-3-319-05032-4_19"},{"key":"488_CR50","unstructured":"Jansen, L., Meyer Zu Horste, M., Schnieder, 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 Desgin\/CPN, pp. 103\u2013115. Aarhus University (1998). https:\/\/pdfs.semanticscholar.org\/8fcd\/1cfb8fb098fa75205f51ab00a6700e4db0e7.pdf . Accessed 7 Mar 2018"},{"key":"488_CR51","doi-asserted-by":"publisher","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, Berlin (2009)"},{"issue":"3","key":"488_CR52","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1109\/TR.2004.832819","volume":"53","author":"G Latif-Shabgahi","year":"2004","unstructured":"Latif-Shabgahi, G., Bass, J.M., Bennett, S.: A taxonomy for software voting algorithms used in safety-critical systems. IEEE Trans. Reliab. 53(3), 319\u2013328 (2004)","journal-title":"IEEE Trans. Reliab."},{"key":"488_CR53","doi-asserted-by":"crossref","unstructured":"Magree, J.: Behavioral analysis of software architectures using LTSA. In: Proceedings of the 1999 International Conference on Software Engineering, 1999, pp. 634\u2013637. IEEE (1999)","DOI":"10.1145\/302405.302726"},{"key":"488_CR54","doi-asserted-by":"crossref","unstructured":"Mateescu, R., Thivolle, D.: A model checking language for concurrent value-passing systems. In: FM 2008: Formal Methods, 15th International Symposium on Formal Methods, Turku, Finland, May 26\u201330, 2008, Proceedings, volume 5014 of Lecture Notes in Computer Science, pp. 148\u2013164. Springer (2008)","DOI":"10.1007\/978-3-540-68237-0_12"},{"key":"488_CR55","doi-asserted-by":"crossref","unstructured":"Mazzanti, F.: An experience in Ada multicore programming: parallelisation of a model checking engine. In: Ada-Europe International Conference on Reliable Software Technologies, volume 9695 of LNCS, pp. 94\u2013109. Springer (2016)","DOI":"10.1007\/978-3-319-39083-3_7"},{"key":"488_CR56","doi-asserted-by":"crossref","unstructured":"Mazzanti, F., Ferrari, A., Spagnolo, G.O.: Experiments in formal modelling of a deadlock avoidance algorithm for a CBTC system. In: International Symposium on Leveraging Applications of Formal Methods, pp. 297\u2013314. Springer (2016)","DOI":"10.1007\/978-3-319-47169-3_22"},{"key":"488_CR57","doi-asserted-by":"crossref","unstructured":"Mazzanti, F., Spagnolo, G.O., Della Longa, S., Ferrari, A.: Deadlock avoidance in train scheduling: a model checking approach. In: International Workshop on Formal Methods for Industrial Critical Systems, volume 8718 of LNCS, pp. 109\u2013123. Springer (2014)","DOI":"10.1007\/978-3-319-10702-8_8"},{"key":"488_CR58","doi-asserted-by":"crossref","unstructured":"Mazzanti, F., Spagnolo, G.O., Ferrari, A.: Designing a deadlock-free train scheduler: a model checking approach. In: NASA Formal Methods Symposium, volume 8430 of LNCS, pp. 264\u2013269. Springer (2014)","DOI":"10.1007\/978-3-319-06200-6_22"},{"key":"488_CR59","unstructured":"Mazzanti, F., Spagnolo, G.O., Ferrari, A.: Formal Tool Diversity\u2014Experiments Data Repository (2017). https:\/\/github.com\/ISTI-FMT\/TrainSchedulingModels , http:\/\/fmt.isti.cnr.it\/WEBPAPER\/TrainSchedulingModels-master.zip . Accessed 7 Mar 2018"},{"issue":"2","key":"488_CR60","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1145\/1646353.1646372","volume":"53","author":"SP Miller","year":"2010","unstructured":"Miller, S.P., Whalen, M.W., Cofer, D.D.: Software model checking takes off. Commun. ACM 53(2), 58\u201364 (2010)","journal-title":"Commun. ACM"},{"key":"488_CR61","doi-asserted-by":"crossref","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: International Conference on Automated Deduction, pp. 748\u2013752. Springer (1992)","DOI":"10.1007\/3-540-55602-8_217"},{"issue":"6","key":"488_CR62","doi-asserted-by":"publisher","first-page":"580","DOI":"10.1109\/71.774908","volume":"10","author":"D Powell","year":"1999","unstructured":"Powell, D., Arlat, J., Beus-Dukic, L., Bondavalli, A., Coppola, P., Fantechi, A., Jenn, E., Rab\u00e9jac, C., Wellings, A.: Guards: a generic upgradable architecture for real-time dependable systems. IEEE Trans. Parallel Distrib. Syst. 10(6), 580\u2013599 (1999)","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"key":"488_CR63","doi-asserted-by":"crossref","unstructured":"Qian, J., Liu, J., Chen, X., Sun, J.: Modeling and verification of zone controller: the scade experience in China\u2019s railway systems. In: 2015 IEEE\/ACM 1st International Workshop on Complex Faults and Failures in Large Software Systems (COUFLESS), pp. 48\u201354. IEEE (2015)","DOI":"10.1109\/COUFLESS.2015.15"},{"key":"488_CR64","unstructured":"RTCA. DO-178C Software Considerations in Airborne Systems and Equipment Certification (2012)"},{"issue":"2","key":"488_CR65","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/j.scico.2010.07.002","volume":"76","author":"MH Beek ter","year":"2011","unstructured":"ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: A state\/event-based model-checking approach for the analysis of abstract system properties. Sci. Comput. Program. 76(2), 119\u2013135 (2011)","journal-title":"Sci. Comput. Program."},{"key":"488_CR66","doi-asserted-by":"crossref","unstructured":"ter Beek, M.H., Gnesi, S., Mazzanti, F.: From EU projects to a family of model checkers. In: Software, Services, and Systems, volume 8950 of LNCS, pp. 312\u2013328. Springer (2015)","DOI":"10.1007\/978-3-319-15545-6_20"},{"key":"488_CR67","doi-asserted-by":"crossref","unstructured":"Vanit-Anunchai, S.: Application of coloured petri nets in modelling and simulating a railway signalling system. In: International Workshop on Formal Methods for Industrial Critical Systems, pp. 214\u2013230. Springer (2016)","DOI":"10.1007\/978-3-319-45943-1_15"},{"key":"488_CR68","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/j.scico.2016.05.010","volume":"133","author":"LH Vu","year":"2017","unstructured":"Vu, L.H., Haxthausen, A.E., Peleska, J.: Formal modelling and verification of interlocking systems featuring sequential release. Sci. Comput. Program. 133, 91\u2013115 (2017)","journal-title":"Sci. Comput. Program."},{"key":"488_CR69","doi-asserted-by":"crossref","unstructured":"Whalen, M., Cofer, D., Miller, S., Krogh, B.H., Storm, W.: Integration of formal analysis into a model-based software development process. In: International Workshop on Formal Methods for Industrial Critical Systems, pp. 68\u201384. Springer (2007)","DOI":"10.1007\/978-3-540-79707-4_7"},{"key":"488_CR70","unstructured":"Winter, K., Johnston, W., Robinson, P., Strooper, P., Van Den Berg, L.: Tool support for checking railway interlocking designs. In: Proceedings of the 10th Australian Workshop on Safety Critical Systems and Software, vol. 55, pp. 101\u2013107. Australian Computer Society, Inc. (2006)"},{"issue":"4","key":"488_CR71","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1145\/1592434.1592436","volume":"41","author":"J Woodcock","year":"2009","unstructured":"Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal methods: Practice and experience. ACM Comput. Surv. (CSUR) 41(4), 19 (2009)","journal-title":"ACM Comput. Surv. (CSUR)"},{"issue":"2","key":"488_CR72","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/s00165-014-0302-2","volume":"27","author":"P Zave","year":"2015","unstructured":"Zave, P.: A practical comparison of alloy and spin. Formal Aspects Comput. 27(2), 239 (2015)","journal-title":"Formal Aspects Comput."}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-018-0488-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-018-0488-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-018-0488-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T14:10:50Z","timestamp":1693577450000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-018-0488-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,3,8]]},"references-count":72,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2018,6]]}},"alternative-id":["488"],"URL":"https:\/\/doi.org\/10.1007\/s10009-018-0488-3","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,3,8]]},"assertion":[{"value":"8 March 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}