Secondary tools for Verification and Validation - openETCS/model-evaluation GitHub Wiki
This page concerns activities of WP7 T7.2 and is dedicated to the evaluation of tools for VnV activities.
Planning is available on the main page.
Activities covered by means and tools
The following activities have been proposed initially (in the DoW) to be covered by the Verification & Validation tools :
- Static Analysis
- Test Case handling
- Testing
- Simulation
- Formal proof
- Model checking/ Contract based Analysis
- Documentation
Means and tools proposed for Verification or Validation
The following table contents the proposed means and tools to evaluate for this benchmark :
| Contact | Formalism / Tool | Link with primary means or tools | Verification | Validation | 1c) VnV SSRS | 2c) VnV SubSystem Model | 3d) VnV SW model | 3e) VnV Sw code |
|---|---|---|---|---|---|---|---|---|
| Marielle Petit-Doche (Systerel) | AtelierB | Classical B | X | X | X | X | X | |
| Uwe Steinke (SIEMENS) | SCADE Suite | SCADE | X | X | ? | ? | ? | ? |
| Stefan Rieger (TWT) | UPPAAL | system C | X | X | ? | ? | ? | ? |
| Stefan Rieger (TWT) | System C | SysML/ C | X | X | ? | ? | ? | ? |
| Matthias Güdemann (Systerel) | Rodin + pluggins (ProR, ProB, SMT solvers, IUML,...) | Event B | X | X | X | X | ||
| Jan Welte (TU-BS) | CPN-Tools & SPENAT | Coloured PN | X | X | ? | ? | ? | ? |
| Alexandre Ginisty (All4tec) | MaTeLo (Model Based Testing tool based on Markov Chains) | UML/SysML (Papyrus) | X | X | ? | ? | ? | ? |
| Cécile Braunstein (Uni. Bremen) | [RT-tester] (https://github.com/openETCS/model-evaluation/wiki/RT-Tester-description) | [EA-SysML] (https://github.com/openETCS/model-evaluation/wiki/EA-Enterprise-Architect-description)/[SCADE](https://github.com/openETCS/model-evaluation/wiki/SCADE-Description) | X | X | ? | ? | ? | ? |
| Silvano Dal Zilio (LAAS-CNRS) | Fiacre and Tina, model-checking toolbox for Time Petri Nets | UML/SysML (Papyrus) | X | ? | ? | ? | ? | |
| Virgile Prevosto (CEA LIST) | Frama-C | X | X | X | X | |||
| Christophe Gaston (CEA LIST) | Diversity | UML/SysML (Papyrus) | X | |||||
Who is volunteer to propose means and tools to evaluate ?
Criteria for Verification
- Model verification
- Techniques
- Traceability
- Correctness
- Completeness
- ...
Criteria for Validation
- Functional
- Real-Time
- Safety
- ...
Case studies and Criteria
These tools are strongly linked to those of the primary benchmark. We propose to start with the same example as described in D2.5 from Subset 026:
- §3.5.3: Establish a communication session
- §5.9: Procedure on Sight
- §4.6.2: Transitions table
- parts of §3.13: Braking curves
A first set of criteria is in discussion with WP4, see [https://github.com/openETCS/validation/blob/master/VerificationAndValidationPlan/WP41a-PreliminaryEvaluationCriteriaOnVAndV.pdf](this document)
Other ideas ?
An open repository to store the models is available: VnV means and tools