Student zvolí systém (např. robot, síťový protokol) a modeluje ho ve vhodném formalizmu (např. časované automaty, hybridní systémy). Pak analyzuje vlastnosti tohoto systému ve vhodném softwarovém balíku (např. UPPAAL, HSolver).