Skip to content

ERTMSFormalSpecs Project proposal

Jump to bottom
BerndHekele edited this page Mar 12, 2013 · 3 revisions

##Proposal The ERTMSFormalSpecs project is a proposed open source project under the OpenETCS Container Project (WP3).

This proposal is in the Project Proposal Phase (as defined in the OpenETCS Development Process) and is written to declare its intent and scope. We solicit additional participation and input from the OpenETCS community. Please send all feedback to this mailing list [email protected].

Background

The European Railway Traffic Management System (ERTMS) defines standards for interoperability between the onboard train protection systems (ETCS) and the railway infrastructure. The ERTMS specifications are of significant size, and as of today, specified in plain English only. ERTMSFormalSpecs (EFS) is a project based on a domain-specific language, designed to express the ERTMS specification in a concise and verifiable formal representation. It aims at being understandable by domain specialists while retaining the ability to be interpreted or translated to efficient executable representations by fully automated means.

For a full description of ERTMSFormalSpecs, see the white paper presented at the WCRR2011 conference: http://www.ertmssolutions.com/files/ERTMSFormalSpecs_WCRR2011.pdf

Scope

The scope of ERTMSFormalSpecs is to model only the onboard ERTMS subsystem, not the complete ERTMS system (i.e. not including RBC, Eurobalise, Loop, RIU, etc).

Moreover the scope is restricted only to the applicative functions of the onboard ERTMS (EVC), specified in Subset-026. All peripherals and FFFIS interfaces are not included in the scope (i.e. DMI, BTM, JRU, FFFIS STM, FIS Euroradio, ...).

ERTMSFormalSpecs scope includes three components:

  • A formal language
  • A toolchain enabling to browse specs, model, trace, test and debug
  • Subset-026 model and tests

Description

The ERTMSFormalSpecs (EFS) product is made up of two components:

1/ The model includes the requirements expressed in Subset-026, the complete data description, sub-system decomposition and business logic of an EVC, specified in UNISIG Subset-026 specifications, expressed in the EFS language, and the tests from Subset-076 tests as well as additional tests needed to cover the Subset-076 holes.

2/ The workbench is a graphical tool designed to develop, maintain, and document model-based development for the Subset-026. It is a desktop application, running on Microsoft Windows platform.

The EFS language is a domain specific language, developed by ERTMS Solutions for the sole purpose of modelling the ERTMS specifications. It is thus not clobbered by history of irrelevant application domains, nor by universal features that are commonly included in general purpose formalizations. This language design is driven by two opposite constraints:

• Constraint 1: To be as close as possible to the artifacts used in the UNISIG Subset-026 specifications (e.g. plain English, state diagrams, tables) to demonstrate the equivalence between specification and implementation

• Constraint 2: To be formal to allow interpretation, inferences and deduce system properties.

Why OpenETCS?

ERTMSFormalSpecs is 100% inline with the goals of the OpenETCS project, which are expressed in OpenETCS FPP:

The purpose of the OpenETCS project is to develop an integrated modelling, development, validation and testing framework for leveraging the cost-efficient and reliable implementation of ETCS. The framework will provide a holistic tool chain across the whole development process of ETCS software. The tool chain will support the formal specification and verification of the ETCS system requirements, the automatic and ETCS compliant code generation and validation, and the model-based test case generation and execution. OpenETCS will utilize "Open Standards" on all levels, including hardware and software specification, interface definition, design tools, verification and validation procedures and last but not least embedded control software.

What will be the benefits for the OpenETCS project?

The OpenETCS project shall be able to reuse the complete work done in the scope of ERTMSFormalSpecs (as of today, a complete toolchain plus 33% of Subset-026 including braking curves already modelled).

Reusing this work shall provide a headstart for the WP3a and WP3 work packages.

Also, the existing community involvement in ERTMSFormalSpecs shall boost community involvement of OpenETCS, bringing greater resources to both open-source projects.

What will be the benefits for the ERTMSFormalSpecs project?

ERTMSFormalSpecs shall benefit from the large OpenETCS consortium resources that could collaborate with existing ERTMSFormalSpecs committers to further develop the ERTMSFormalSpecs product.

Initial Contribution

As of today, 100% of ERTMSFormalSpecs source code and documentation has been placed under EUPL license, as a public repository on GitHub https://github.com/stanpinte/ERTMSFormalSpecs.

Legal Issues

100% of ERTMSFormalSpecs source code and documentation has been placed under EUPL license. IP is completely owned by ERTMS Solutions , as all source code and documentation has been developed by individuals working for ERTMS Solutions as employees, therefore ensuring ERTMS Solutions has the full IP and authority to apply EUPL license to all ERTMSFormalSpecs artifacts.

Additionally, ERTMSFormalSpecs depends on the following third-party components:

All components that have a license compatible with the EUPL license http://joinup.ec.europa.eu/software/page/eupl/eupl-compatible-open-source-licences#section-2 are included in the ERTMSFormalSpecs repository.

Components that are incompatible with EUPL can be downloaded separately by the users (as tracked in issue https://github.com/stanpinte/ERTMSFormalSpecs/issues/10), and shall not be included in the ERTMSFormalSpecs repository.

  • XML Persistence. Persistence of the ERTMSFormalSpec Workbench is performed using XML which garantees the openness of the model. However, we have used XMLBooster, available at http://www.xmlbooster.com to generate the data structure, parsers and unparsers used to store the model. XMLBooster C# runtime license ONGOING EUPL MIGRATION
  • Reporting is performed through PdfSharp, publicly available at http://www.pdfsharp.net, published under the MIT license, COMPATIBLE WITH EUPL
  • Speed decelaration graphs are created using Gnuplot, available at http://www.gnuplot.info/, published under the GNUPlot license COMPATIBILITY WITH EUPL UNDER CHECK
  • Logging is performed using Log4Net, available at http://logging.apache.org/log4net/, published under the Apache license v2.0 COMPATIBLE WITH EUPL
  • Installer files are created using Inno installer 5.0, available at http://www.jrsoftware.org/isinfo.php, published under the INNO Setup license COMPATIBILITY WITH EUPL UNDER CHECK

Project Leads

Stanislas Pinte, ERTMS Solutions

Committers

The following individuals are the initial committers to the GitHub project:

Laurent Ferier, ERTMS Solutions Svitlana Lukicheva, ERTMS Solutions Juan Diez Perez, ERTMS Solutions

We welcome additional committers and contributions.

Mentors

The following Architecture Council members will mentor this project:

  • Jonas Helming
  • Klaus-Ruediger Hase

Interested Parties

The following individuals, organisations, companies and projects have expressed interest in this project:

Project Scheduling

All bugs and enhancements are listed on https://github.com/stanpinte/ERTMSFormalSpecs/issues

As of today, all committers are working on the following issues:

  • Support for Subset-026 v3.3.0
  • Verification of Braking Curves implementation with the ERA braking curve spreadsheet

This work shall be ongoing in November and December 2012.

Clone this wiki locally