This folder contains the deliverables related to the use of the FORMOSE approach (SysML/KAOS goal and domain modeling) on the ABZ2018 case study : specification of the hybrid ERTMS/ETCS Level 3 Standard (https://www.southampton.ac.uk/abz2018/information/case-study.page).
  
  # ABZ2018-_ERTMS_Case_Study.pdf
  This file represents a  paper describing the application of the FORMOSE approach on the ABZ2018 case study.
  
  # ABZ2018-_ERTMS_Case_Study_old_full_version.pdf
  This file represents a rough paper describing, with more details and explanations, the application of the FORMOSE approach on the ABZ2018 case study.
  
  # ABZ2018CaseStudy_eventb_proofs_scope.zip
  This archive contains the Rodin components related to the Event-B specification of the hybrid ERTMS/ETCS Level 3 Standard (here we take into account Event-B requirements not relevant for the FORMOSE approach).
  
  # ABZ2018CaseStudy_restricted_sysmlkaos_proofs_scope.zip
  This archive contains the Rodin components related to the Event-B specification of the hybrid ERTMS/ETCS Level 3 Standard with a strict application of the FORMOSE approach (for example, we are not interested here in Event-B proof obligations that are not relevant for the approach).