Part of WP 3a aka WP7.
Available models:
- model/Why3-MERCE/ model attempt made with Why3 0.80 tool (http://why3.lri.fr)
- model/B-Systerel/Classical_B model attempt made with Atelier B tool(http://www.atelierb.eu)
- model/B-Systerel/Event_B model attempt made with Rodin in Event-B (http://www.event-b.org/)
- model/EA-SysML model attempt made with Enterprise Architect
- model/GNATprove-MERCE/ model attempt made with GNATprove tool (http://www.open-do.org/projects/hi-lite/gnatprove/)
- model/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 model/ERTMSFormalSpecs)
- model/SCADE_Siemens: SCADE model, generated C code and documentation made with SCADE Suite (http://www.esterel-technologies.com/)