Embedded systems toolchain
An integrated toolchain for embedded systems, grounded end to end in a single deterministic model of computation: MIMOS. Modelling, simulation, verification, schedulability analysis, and code synthesis — all on the same semantics, so properties proven at the model level carry through to the deployed system.
Toolchain
Five stages share the same MIMOS model of computation, so what you simulate is what you verify — and what you verify is what runs.
Describe the system as a MIMOS network: real-time tasks connected by asynchronous FIFO and register channels.
Execute the model step by step to get a deterministic trajectory — every run is reproducible bit-for-bit.
Check deadlock- and overflow-freedom by static analysis. Verify functional properties by exhaustive state-space exploration.
Map verified components to real-time tasks; check multicore schedulability and worst-case end-to-end latency.
Synthesize multicore deployment code that preserves the model's semantics and the timing constraints verified earlier.
License
MIMOS-Tools is free to use for research, teaching, and evaluation under the PolyForm Noncommercial License 1.0.0. Commercial use requires a separate license — get in touch.
Contact
Questions or licensing: wang.yi@it.uu.se. For bug reports and feature requests, open an issue on GitHub.