-
Notifications
You must be signed in to change notification settings - Fork 17
Evaluationproposal
##Proposal The modelevaluation project is a proposed open source project under the toolchain Container Project (WP3a).
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].
The goal of this project is to identify the modelling languages that could fit the requirements associated to the specific needs of ETCS design and railway norms. Those needs will be defined by the requirements project. Depending on recommendations, several languages may be necessary to handle the different levels of abstraction of the whole design process. For each candidate, a small subset of the ERTMS specification will be modelled. The languages may have to be adapted in the process. The identification and definition will distinguish between wide-spectrum modelling languages suitable for a wide variety of modelling domains such as UML, SysML, B, and domain-specific languages (DSL) designed and optimised for application in a specific application domain only. For wide-spectrum languages their metamodels will be analysed with respect to their expressive power and resulting adequateness for designing ERTMS models. For DSL candidates the associated meta-metamodels will be analysed with respect to their capabilities to support language extensions that may become necessary for novel releases of the ERTMS specification the in the future. Since no language is universal (i.e. able to address all aspects of design needs) the proposed approach is likely to involve several modelling languages supporting different viewpoints and working at different levels of abstractions. With this kind of approach, we will need to check the compatibility of the semantics of the modelling languages that address overlapping viewpoints. There are two problems here. First, when dealing with a heterogeneous specification, we need a common semantical basis to check the compatibility of the models. More pragmatically, when we deal with two models (expressed in a different language) that describe the same part of the system, we need to show that they are consistent with each other. Candidate languages will be subsequently evaluated against the requirements from WP2. If a suitable language is identified, but no partner steps up to model the prototype, it will not be considered.
The experience with the tools will be recorded, and the tools will be evaluated against the requirements from WP2. In particular, the compliance of the candidate tools with respect to EN50128 constraints will be investigated.
The selection of model languages is a core requirement of the openETCS projects.
| Contact | Formalism / Tool | Subset used | Started? | Notes |
|---|---|---|---|---|
| Uwe Steinke (Siemens) | SCADE 6.3.1 | SUBSET-026-3, ISSUE : 3.3.0, 3.5 Management of Radio Communication" | yes | Results presented at WP2 meeting, Nov. 2012 |
| Stan Pinte (ERTMS Solutions) | ERTMSFormalSpecs | Version 0.9, Subset-026 v3.2.0 | yes | 33% of Subset-026 formalized as of november 2012. Workshop on 17.-18. Dec. |
| Cyril Cornu (All4Tec) | CORE Workstation 5.1 | SUBSET 026 ISSUE 3.3.0 | yes | |
| Marielle Petit-doche and Matthias Gudermann (Systerel) | Event-B / Rodin 2.7 with ProR, ProB or AnimB and toolkit of provers (AtelierB, SAT,...) | Subset 26 v3.3.0 | yes | Will combine with ProR for requirements traceability. |
| Marielle Petit-doche and Matthias Gudermann (Systerel) | ClassicalB / AtelierB 4.0.2 | Subset 26 v3.3.0 | no | |
| David Mentré (MERCE) | Why3 0.80 | Subset-026 v3.3.0 | yes | Trying various small parts of subset-026 |
| Cecile Braunstein (Uni. Bremen) | SysML/EA, RT-Tester | SUBSET-026-3, ISSUE : 3.0.0, 3.5 Management of Radio Communication" | yes | |
| Johannes Feuser (Uni. Bremen) | GOPRR (GOPPRR) meta meta model / MetaEdit+ | {Subset-026 (Issue 2.3.0)/Levels: 0, 1/ETCS Modes: NP/SB/SF/IS/TR/PT/UN/SR/FS | yes (finished) | Not all functionality modelled. To be published in Ph.D. thesis approximately February 2013 and in J. Feuser and J. Peleska, “Dependability in Open Proof Software with Hardware Virtualization – The Railway Control Systems perspective,” 2012, under revision for Special Issue of Science of Computer Programming. |
- Classical B model and Event-B model: no legal issue. New code under EUPL v.1.1 developed for the project
- Why3 model: no legal issue. All code is licensed under EUPL v.1.1 and owned by MERCE
- ERTMSFormalSpecs model: No issue, as full code is under EUPL v.1.1
- SysML/EA model : no legal issue. All code is licensed under EUPL v.1.1 and owned by Braunstein.
David Mentre
- Michael Jastram, Formal Mind
- Uwe Steinke, Siemens, GitHub: UweSteinkeFromSiemens
- Stanislas Pinte, ERTMS Solution
- Cyril Cornu, ALL4TEC
- Marielle Petit-Doche, Systerel, GitHub: MariellePetitDoche
- Matthias Gudemann, Systerel, GitHub: MGudemann
- David Mentré, Mitsubishi Electric R&D Centre, MERCEmentre on GitHub
- Cecile Braunstein, Uni. Bremen, GitHub: cecilebraun
- Johannes Feuser, Uni. Bremen
We welcome additional committers and contributions.
The following members will mentor this project:
- Klaus-Ruediger Hase (Deutsche Bahn)
- Jonas Helming (EclipseSource München)
- Michael Jastram (Formal Mind)
Are there anymore interested parties?
- Milestone 1 (Apr-13): Report on the candidate languages (sample model, evaluation against requirements and evolution needed)
- Milestone 2 (May-13): Report on the final language choice(s)