Dynamic state machines for modelling railway control systems

Science of Computer Programming - Tập 133 - Trang 116-153 - 2017
M. Benerecetti1, R. De Guglielmo2, U. Gentile1, S. Marrone3, N. Mazzocca1, R. Nardone1, A. Peron1, L. Velardi2, V. Vittorini1
1Department of Electrical Engineering and Information Technology, University of Naples Federico II, Naples, Italy
2Ansaldo STS, Naples, Italy
3Department of Mathematics and Physics, Second University of Naples, Naples, Italy

Tài liệu tham khảo

Alur, 1999, Communicating hierarchical state machines, vol. 1644, 169 Amalfitano, 2014, Improving code coverage in android apps testing by exploiting patterns and automatic test case generation, 29 Anand, 2013, An orchestrated survey of methodologies for automated software test case generation, J. Syst. Softw., 86, 1978, 10.1016/j.jss.2013.02.061 Artho, 2013, Modbat: a model-based API tester for event-driven systems, vol. 8244, 112 Barberio, 2014, An interoperable testing environment for ERTMS/ETCS control systems, vol. 8696, 147 Benerecetti, 2010, Analysis of timed recursive state machines, 61 Benerecetti, 2016, Timed recursive state machines: expressiveness and complexity, Theor. Comput. Sci., 625, 85, 10.1016/j.tcs.2016.02.021 Bernardi, 2013, Enabling the usage of UML in the verification of railway systems: the dam-rail approach, Reliab. Eng. Syst. Saf., 120, 112, 10.1016/j.ress.2013.06.032 D. Bjørner, New results and trends in formal techniques and tools for the development of software for transportation systems: a review, in: Proceedings 4th Symposium on Formal Methods for Railway Operation and Control Systems, FORMS03, LHarmattan Hongrie, Budapest, 2003. Braunstein, 2014, Complete model-based equivalence class testing for the ETCS ceiling speed monitor, 380 CENELEC, 2003 CENELEC, 2011 Cimatti, 2000, NuSMV: a new symbolic model checker, Int. J. Softw. Tools Technol. Transf., 2, 2000, 10.1007/s100090050046 Gentile, 2014, Test specification patterns for automatic generation of test sequences, 170 M. Glinz, Statecharts for requirements specification—as simple as possible, as rich as needed, in: Proceedings of the ICSE 2002 International Workshop on Scenarios and State Machines: Models, Algorithms and Tools, Orlando, Florida, USA. Hamon, 2005, A denotational semantics for stateflow, 164 Hamon, 2007, An operational semantics for stateflow, Int. J. Softw. Tools Technol. Transf., 9, 447, 10.1007/s10009-007-0049-7 Harel, 1987, Statecharts: a visual formalism for complex systems, Sci. Comput. Program., 8, 231, 10.1016/0167-6423(87)90035-9 Harel, 1996, The statemate semantics of statecharts, ACM Trans. Softw. Eng. Methodol., 5, 293, 10.1145/235321.235322 Haxthausen, 2015, Model checking and model-based testing in the railway domain, 82 Hierons, 2009, Using formal specifications to support testing, ACM Comput. Surv., 41, 9, 10.1145/1459352.1459354 Holzmann, 2003 Jouault, 2008, ATL: a model transformation tool, Sci. Comput. Program., 72, 31, 10.1016/j.scico.2007.08.002 Lanotte, 2002, Dynamic hierarchical machines, Fundam. Inform., 54, 237 Leveson, 1994, Requirements specification for process-control systems, IEEE Trans. Softw. Eng., 20, 684, 10.1109/32.317428 Maggiolo-Schettini, 2003, A comparison of statecharts step semantics, Theor. Comput. Sci., 290, 465, 10.1016/S0304-3975(01)00381-4 Marrone, 2014, Towards model-driven V&V assessment of railway control systems, Int. J. Softw. Tools Technol. Transf., 16, 669, 10.1007/s10009-014-0320-7 Marrone, 2013, Vulnerability modeling and analysis for critical infrastructure protection applications, Int. J. Crit. Infrastruct. Prot., 6, 217, 10.1016/j.ijcip.2013.10.001 Marrone, 2015, On synergies of cyber and physical security modelling in vulnerability assessment of railway systems, Comput. Electr. Eng., 47, 275, 10.1016/j.compeleceng.2015.07.011 Nardone, 2016, Modeling railway control systems in Promela, vol. 596, 121 Nardone, 2014, Dynamic state machines for formalizing railway control system specifications, 93 OMG-UML2, Unified Modeling Language: Infrastructure and Superstructure, OMG, 2011, Version 2.4.1 formal/11-08-05. Peleska, 2013, Industrial-strength model-based testing—state of the art and current challenges, Electron. Proc. Theor. Comput. Sci., 111, 3, 10.4204/EPTCS.111.1 Petrenko, 2012, Model-based testing of software and systems: recent advances and challenges, Int. J. Softw. Tools Technol. Transf., 14, 383, 10.1007/s10009-012-0240-3 Pflügl, 2013, CRYSTAL, critical system engineering acceleration, a truly European dimension, ARTEMIS Mag., 14, 12 Schmidt, 2006, Guest editor's introduction: model-driven engineering, Computer, 39, 25, 10.1109/MC.2006.58 UIC, 2002 Utting, 2007