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
 Heath, W.S., Real-time Software Techniques, Van Nostrand Reinhold: New York, 1991.
 CENELEC: EN 50126 Railways Applications – The specification and demonstration of Reliability, Maintainability and Safety (RAMS), 2001.
 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.
 Fowler, M. et al., Refactoring: Improving the Design of Existing Code, 1st edn, Addison-Wesley Professional, 1999.
 Chikofsky, E.J. & Cross, J.H., Reverse engineering and design recovery: a taxonomy. IEEE Software, 7(1), 1990. doi:10.1109/52.43044
 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
 UNISIG ERTMS/ETCS – Class 1 Issue 2.2.2 Subset 026, 2001.
 OMG Unified Modeling Language: http://www.omg.org/uml
 Rational Corporation: http://www.rational.com
 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
 Mirandola, R. & Cortellessa, V., UML Based Performance Modeling of Distributed Systems. Proceedings of UML, pp. 178–193, 2000.
 Briand, L. & Labiche, Y., A UML-based approach to system testing. In Journal of Software and Systems Modeling, 1(1), pp. 10–42, 2002.
 Astels, D., Refactoring with UML. Proc. of the 3rd International Conference on eXtreme Programming and Flexible Processes in Software Engineering, pp. 67–70, 2002.
 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, http://www.springerlink.com/content/30881032523123r2 doi:10.1007/s10664-007-9037-5
 Visual Paradigm Code Reverse: http://www.visual-paradigm.com/VPGallery/codeengine/CodeReverse.html
 Interactive Objects ArchStyler: http://www.interactive-objects.com/products/arcstyler
 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.
 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).
 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
 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
 Verimag IF: http://www-verimag.imag.fr/~async/IF/index.html
 Telelogic Logiscope: http://www.telelogic.com/logiscope/
 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
 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.
 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
 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.
 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
 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.
 Source Dynamics Source Insight: http://www.sourceinsight.com/
 Agile Modeling: http://www.agilemodeling.com/
 Egyed, N., Medvidovic: Consistent Architectural Refinement and Evolution using the Unified Modeling Language. Proceedings of ICSE 2001, Toronto, 3463, pp. 305–317, 2005.
 OMG Model Driven Architecture: http://www.omg.org/mda/