In this work, we present a results from case study ontesting a highly configurable, safety-critical system from therailway domain using model-based risk-oriented testing. Inthe construction of the system and test models, we face thefollowing problems: (i) A domain expert will usually not beknowledgeable in the construction of system models, but hasvery detailed knowledge which configurations of the systemwill be especially critical (e.g., prone to head-on collisions).Thus, a method for the construction of system and testmodels from domain-specific descriptions is necessary. (ii)The system model shall be validatable against the system’srequirements. (iii) The verification of the system modelagainst safety requirements should be possible. We willdemonstrate an approach based on DSLs, compositionalconstruction of Mealy machines and a proof technique asa solution to these three problems.