Part of WP 3a aka WP7. (task T7.1)
Available models:
- Why3-MERCE/ model attempt made with Why3 0.80 tool (http://why3.lri.fr)
- B-Systerel/Classical_B model attempt made with Atelier B tool(http://www.atelierb.eu)
- B-Systerel/Event_B model attempt made with Rodin in Event-B (http://www.event-b.org/)
- EA-SysML model attempt made with Enterprise Architect
- GNATprove-MERCE/ model attempt made with GNATprove tool (http://www.open-do.org/projects/hi-lite/gnatprove/)
- CORE-All4tec model attempt made with CORE Workstation (http://www.vitechcorp.com/products/core.shtml)
- ERTMSFormalSpec https://github.com/openETCS/ERTMSFormalSpecs (TODO: add a README file in ERTMSFormalSpecs)
- SCADE_Siemens: SCADE model, generated C code and documentation made with SCADE Suite (http://www.esterel-technologies.com/)