In this paper, the authors explain a formal method adopted to model the system requirements specification of the ERTMS/ETCS trackside-subsystem (Radio Block Center) implemented on the high speed/high capacity Italian railways. The logical behaviour is represented by Statechart diagrams using the Statemate™ Magnum Tool. The model pointed out permits to describe the specification in scalable way, giving both a high level of abstraction and a more detailed level of description. The proposed methodology has been applied to represent the Bologna-Firenze and Milano-Bologna ETCS lines. The process has concerned the following steps: I) analysis of all the documents (UNISIG, RFI SRS), II) chose of the Formal Language Model (Statecharts), III) rules definition for Statechart Models (state conditions, state transitions), IV) develompment of the Statechart Model for the ETCS Trackside Subsystem, V) testing of the Model by Specific Tools: i) Statemate Magnum Certifier for logical tests implemented by the user, ii) Automatic evaluation of the model through Real Datalog files.

Use of formal languages to represent the ERTMS/ETCS system requirements specifications

PICCOLO, Antonio;GALDI, Vincenzo;MALANGONE, RAFFAELE
2015-01-01

Abstract

In this paper, the authors explain a formal method adopted to model the system requirements specification of the ERTMS/ETCS trackside-subsystem (Radio Block Center) implemented on the high speed/high capacity Italian railways. The logical behaviour is represented by Statechart diagrams using the Statemate™ Magnum Tool. The model pointed out permits to describe the specification in scalable way, giving both a high level of abstraction and a more detailed level of description. The proposed methodology has been applied to represent the Bologna-Firenze and Milano-Bologna ETCS lines. The process has concerned the following steps: I) analysis of all the documents (UNISIG, RFI SRS), II) chose of the Formal Language Model (Statecharts), III) rules definition for Statechart Models (state conditions, state transitions), IV) develompment of the Statechart Model for the ETCS Trackside Subsystem, V) testing of the Model by Specific Tools: i) Statemate Magnum Certifier for logical tests implemented by the user, ii) Automatic evaluation of the model through Real Datalog files.
2015
9781479974009
9781479974009
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11386/4670416
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 6
  • ???jsp.display-item.citation.isi??? ND
social impact