Validation coverage for a component-based SDL model of a railway signaling system
Banci M, Becucci M, Fantechi A, Spinicci E
Computer Science(all) Railway signaling Program Verification MSC scenario Theoretical Computer Science General Computer Science Software validation Component-based SDL model
In this paper we present an application of formal verification techniques to a component-based SDL model of a railway signalling system lent by General Electric Transportation Systems. A MSC-driven validation technique has been applied to verify the multiple-configuration features of the system. This work addresses the problem of validating a component-oriented designed SDL model, with a partial reuse of previously verified MSC scenarios if a new component is introducing or modified: some possible solutions based on the coverage metrics and information provided by the adopted tools are discussed.
Publisher: Elsevier B.V.
[2] ITU-T, Recommendation Z.120 - Message Sequence Charts (MSC). Geneva, 1999.
[3] D. Harel, Statecharts: A visual formalism for complex systems. Science of Computer Programming, Vol. 8, pages 231-274, 1987.
[4] S. Bacherini, S. Bianchi, L. Capecchi, C. Becheri, A. Felleca, A. Fantechi, E. Spinicci, Modelling a railway signalling system using SDL. Proceedings of FORMS 2003 International Symposium on Formal Methods for Railway Operation and Control Systems, Budapest, May 2003.
[5] A. Fantechi, E. Spinicci, Modelling and Validating a Multiple-configuration railway signalling system using SDL. Proceedings of TACoS 2003 International Workshop on Test and Analysis of Component Based Systems, Warsaw, April 2003.
[6] J. Bohn, W. Damm, H. Wittke, J. Klose, A. Moik, Modeling and Validating Train System Applications Using Statemate and Live Sequence Charts. Integrated Design and Process Technology, IDPT-2002, United States of America, June 2002.
[7] A. Cimatti, P. Pieraccini, R. Sebastiani, P. Traverso, A. Villafiorita, Formal specification and validation of a vital protocol. Proceedings of FM'99, Toulouse, France, September 1999. LNCS 1709, Springer-Verlag.
[8] Telelogic TAU 4.4 User's manual, Telelogic AB, www.telelogic.com.
[9] G. J. Holzmann Design and Validation of Computer Protocols. Prentice-Hall, 1990.
[10] G. J. Holzmann Validating SDL Specification: an Experiment. Proceedings of the 9th International Workshop on Protocol Specification, Testing and Verification, Twente University, The Netherlands, June 1989.
Metrics
Back to previous page
@inproceedings{oai:it.cnr:prodotti:91269,
title = {Validation coverage for a component-based SDL model of a railway signaling system},
author = {Banci M and Becucci M and Fantechi A and Spinicci E},
publisher = {Elsevier B.V.},
doi = {10.1016/j.entcs.2004.02.083},
year = {2005}
}
0000-0002-4648-4667