Bu makale, ABZ2018 için önerilen vaka çalışması çerçevesinde hibrid ERTMS / ETCS seviye 3 standardının bir spesifikasyonunu sunmaktadır. Spesifikasyon, ANR FORMOSE projesinde geliştirilen, kritik ve karmaşık sistem gereksinimlerinin modellenmesi ve resmi olarak doğrulanması için yöntem ve araçlara dayanmaktadır. Gereksinimler SysML / KAOS hedef diyagramları ile belirtilir ve resmi şartnamenin mimarisini elde etmek için otomatik olarak B Sistem spesifikasyonlarına çevrilir. Etki alanı özellikleri, OWL ve PLIB tabanlı SysML / KAOS etki alanı modelleme dili ile ontolojiler tarafından belirtilir. Otomatik çevirileri resmi şartnamenin yapısal bölümünü tamamlar. Spesifikasyonun manuel olarak tamamlanması gereken tek bölüm olayların gövdesidir. İnşaat, ilgili yöntemler dahilinde mevcut olan iyileştirme mekanizmalarına dayalı olarak artımlıdır. Vaka çalışması ile ilgili olarak, resmi şartname yedi iyileştirme seviyesi içerir ve tüm kanıtlar Rodin platformu altında tahliye edilmiştir.