ETCS (European Train Control System) er en standard som skal sørge for at togene går sikkert og effektivt. En forenklet versjon av ETCS blir for øyeblikket modellert i omskrivningslogikk i Swansea. HybridSynchAADL er en variant og utvidelse av AADL (en industriell modellsstandard for flysystemer) for å modellere "synkrone" distribuerte systemer med "continuous dynamics". HybridSynchAADL utvikles av Kyungmin Bae i Korea (delvis sammen med Ölveczky).
I denne oppgaven skal vi prøve å modellere en forenklet versjon av ETCS i HybridSynchAADL. Vi skal så bruke HybridSynchAADL til å simulere et system med noen tog og sjekke hvorvidt de kommer seg frem sikkert og effektivt. Man skal så bruke HybridSynchAADL's analysemetoder til å verifisere/modell-sjekke at systemet er trygt og effektivt.
En Maude-modell av det forenklede systemet er under utarbeidelse i Swansea.