OPEN ACCESS
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: http://www.omg.org/uml
[9] Rational Corporation: http://www.rational.com
[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, http://www.springerlink.com/content/30881032523123r2 doi:10.1007/s10664-007-9037-5
[15] Visual Paradigm Code Reverse: http://www.visual-paradigm.com/VPGallery/codeengine/CodeReverse.html
[16] Interactive Objects ArchStyler: http://www.interactive-objects.com/products/arcstyler
[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: http://www-verimag.imag.fr/~async/IF/index.html
[22] Telelogic Logiscope: http://www.telelogic.com/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: http://www.sourceinsight.com/
[30] Agile Modeling: http://www.agilemodeling.com/
[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: http://www.omg.org/mda/