Pessoa: MATLAB Toolbox for the synthesis of correct-by-design embedded control software.

This is a Toolbox developed at UCLA's CyPhyLab (Paulo Tabuada's group).
It is based on the recent notion of approximate bisimulation that allows one to replace differential equations, describing a physical system, by an equivalent finite-state machine. Controller design problems can then be solved by using efficient synthesis algorithms operating over the equivalent finite-state machine models. The resulting controllers are also finite-state, are guaranteed to enforce the control specifications on the original physical system, and can be readily transformed into bug-free code for any desired digital platform.
This toolbox lets you:
1.construct effortlessly finite-state models of linear and switched linear control systems
2.use these finite-state models to synthesize controllers for safety and reachability specifications
3.simulate the resulting controllers in Simulink.