Validation coverage for a component-based SDL model of a railway signaling system

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.