We present the EuRailCheck tool, which supports the formalization and the validation of requirements, based on the use of formal methods. The tool allows the user first to analyze the requirements in natural language, categorizing and structuring them; second, to formalize the requirements into a subset of UML with a formal semantics, and enriched with static and temporal constraints; third, to apply model checking techniques specialized for the validation of formal requirements. The tool has been developed and validated within a project funded by the European Railway Agency for the validation of the European Train Control System specification. By now, the tool has been successfully used by almost thirty railway experts of different companies.

Supporting Requirements Validation: The EuRailCheck Tool

Cavada, Roberto;Cimatti, Alessandro;Mariotti, Alessandro;Mattarei, Cristian;Micheli, Andrea;Mover, Sergio;Pensallorto, Marco;Roveri, Marco;Susi, Angelo;Tonetta, Stefano
2009

Abstract

We present the EuRailCheck tool, which supports the formalization and the validation of requirements, based on the use of formal methods. The tool allows the user first to analyze the requirements in natural language, categorizing and structuring them; second, to formalize the requirements into a subset of UML with a formal semantics, and enriched with static and temporal constraints; third, to apply model checking techniques specialized for the validation of formal requirements. The tool has been developed and validated within a project funded by the European Railway Agency for the validation of the European Train Control System specification. By now, the tool has been successfully used by almost thirty railway experts of different companies.
9780769538914
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/11582/5003
 Attenzione

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

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