Formal validation & verification of software for railway control and protection systems: experimental applications in ANSALDO