MIMOS-Tools

Case studies

Exercised on real control systems

Three systems from three domains, each taken through the full MIMOS-Tools flow — modeled, simulated, verified, scheduled — and bundled as runnable examples in every release.

Avionics

ROSACE flight controller

A 13-task, four-rate longitudinal flight controller from industrial avionics.

Railway

Train crossing controller

A classic infinite-state formal-verification benchmark. Exhaustive state-space exploration reduces it to a 158-state automaton and turns up a real liveness bug: a stopped train that can wait forever for a green signal.

Automotive

Autonomous-driving perception pipeline

A six-task object-detection pipeline with a dual-path structure — a high-priority region-of-interest path feeding control, and a lower-rate full-scene path for context.