Modeling of Railway Logics for Reverse Engineering, Verification and Refactoring

Modeling of Railway Logics for Reverse Engineering, Verification and Refactoring

F. Flammini A. Lazzaro N. Mazzocca 

ANSALDO STS, RAMS Unit, Via Nuova delle Brecce 260, Naples 80147, Italy

University of Naples “Federico II”, Dipartimento di Informatica e Sistemistica, Via Claudio 21, Naples 80125, Italy

31 March 2011
| Citation



Model-based approaches are widespread both in functional and non-functional verification activities of critical computer-based systems. Reverse engineering can also be used to support checks for correctness of system implementation against its requirements. In this paper, we show how a model-based technique, using the Unified Modeling language (UMl), suits the reverse engineering of complex control logics. UMl is usually exploited to drive the development of software systems, using an object-oriented and bottom-up approach; however, it can be also used to model legacy non-object-oriented logic processes featuring a clear distinction between data structures and related operations. Our case-study consists in the most important component of the European Railway Traffic Management System/European Train control System: the Radio Block center (RBc). The model we obtained from the logic code of the RBc significantly facilitated both structural and behavioral analyses, giving a valuable contribution to the static verification and refactoring of the software under test.


control software, modeling, railways, refactoring, reverse engineering, verification


[1] Heath, W.S., Real-time Software Techniques, Van Nostrand Reinhold: New York, 1991.

[2] CENELEC: EN 50126 Railways Applications – The specification and demonstration of Reliability, Maintainability and Safety (RAMS), 2001.

[3] De Nicola, G., di Tommaso, P., Esposito, R., Flammini, F., Marmo, P. & Orazzo, A., A grey box approach to the functional testing of complex automatic train protection systems. LNCS, 3463, pp. 305–317, 2005.

[4] Fowler, M. et al., Refactoring: Improving the Design of Existing Code, 1st edn, Addison-Wesley Professional, 1999.

[5] Chikofsky, E.J. & Cross, J.H., Reverse engineering and design recovery: a taxonomy. IEEE Software, 7(1), 1990. doi:10.1109/52.43044

[6] Cimatti, A., Giunchiglia, F., Mongardi, G., Romano, D., Torielli, F. & Traverso, P., Formal verification of a railway interlocking system using model checking. Formal Aspects of Computing, 10(4), pp. 361–380, 1998. doi:10.1007/s001650050022

[7] UNISIG ERTMS/ETCS – Class 1 Issue 2.2.2 Subset 026, 2001.

[8] OMG Unified Modeling Language:

[9] Rational Corporation:

[10] Bondavalli, A., Fantechi, A., Latella, D. & Simoncini, L., Design validation of embedded dependable systems. IEEE Micro, 21(5), pp. 52–62, 2001. doi:10.1109/40.958699

[11] Mirandola, R. & Cortellessa, V., UML Based Performance Modeling of Distributed Systems. Proceedings of UML, pp. 178–193, 2000.

[12] Briand, L. & Labiche, Y., A UML-based approach to system testing. In Journal of Software and Systems Modeling, 1(1), pp. 10–42, 2002.

[13] Astels, D., Refactoring with UML. Proc. of the 3rd International Conference on eXtreme Programming and Flexible Processes in Software Engineering, pp. 67–70, 2002.

[14] Tonella, P., Torchiano, M., Du Bois, B. & Systä, T., Empirical studies in reverse engineering: state of the art and future trends. Empirical Software Engineering, 12(5), 2007, DOI 10.1007/s10664-007-9037-5, doi:10.1007/s10664-007-9037-5

[15] Visual Paradigm Code Reverse:

[16] Interactive Objects ArchStyler:

[17] Cung, A. & Lee, Y.S., Reverse Software Engineering with UML for website maintenance. IEEE Proceedings of Working Conference in Reverse Engineering’00, pp. 100–111, 2000.

[18] Riva, C., Selonen, P., Systa, T. & Xu, J., UML-based reverse engineering and model analysis approaches for software architecture maintenance. Proceedings of the 20th IEEE International Conference on Software Maintenance (ICSM’04).

[19] Briand, L., Labiche, Y. & Leduc, J., Toward the reverse engineering of UML sequence diagrams for distributed Java software. IEEE Transactions on Software Engineering, 32(9), pp. 642–663, 2006. doi:10.1109/TSE.2006.96

[20] Rady de Almeida Jr, J., Batista Camargo Jr, J., Abrantes Basseto, B. & Paz, P., Best practices in code inspection for safety-critical software. IEEE Software, 20(3), pp. 56–63, 2003. doi:10.1109/MS.2003.1196322

[21] Verimag IF:

[22] Telelogic Logiscope:

[23] Bernardeschi, C., Fantechi, A., Gnesi, S., Mongardi, G. & Romano, D., A formal verification environment for railway signaling system design. Formal Methods in System Design, 12, pp. 139–161. 1998. doi:10.1023/A:1008645826258

[24] Gnesi, S., Latella, D., Lenzini, G., Abbaneo, C., Amendola, A. & Marmo, P., An automatic SPIN validation of a safety critical railway control system. IEEE International Conference on Dependable Systems & Networks, pp. 119–124, 2000.

[25] Dong, W., Wang, J., Qi, X. & Qi, Z.-C., Model checking UML statecharts. Eighth Asia-Pacific Software Engineering Conference (APSEC 2001), pp. 363–370, 2001. doi:10.1109/APSEC.2001.991503

[26] Gnesi, S., Latella, D. & Massink, M., Model checking UML statechart diagrams using JACK. The 4th IEEE International Symposium on High-Assurance Systems Engineering, pp. 46–55, 1999.

[27] Havelund, K., Lowry, M. & Penix, J., Formal analysis of a space-craft controller using SPIN. IEEE Transactions on Software Engineering, 27(8), pp. 749–765, 2001. doi:10.1109/32.940728

[28] Abbaneo, C., Flammini, F., Lazzaro, A., Marmo, P., Mazzocca, N. & Sanseviero, A., UML Based Reverse Engineering for the Verification of Railway Control Logics. IEEE Proceedings of Dependability of Computer Systems (DepCoS’96), Szklarska Poręba: Poland, pp. 3–10, May 25–27, 2006.

[29] Source Dynamics Source Insight:

[30] Agile Modeling:

[31] Egyed, N., Medvidovic: Consistent Architectural Refinement and Evolution using the Unified Modeling Language. Proceedings of ICSE 2001, Toronto, 3463, pp. 305–317, 2005.

[32] OMG Model Driven Architecture: