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-01-01
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
