I am looking for tools to design hybrid systems, involving image
processing components and
feedback control components.
Our goal is to verify the design formally to avoid tests using system
and guarantee functional models results and real-time performances.
I already looked at the following tools used at UC Berkeley :
SHIFT seems to target design and simulation of hybrid systems with a
number of components.
Hytech seems to target formal verification of hybrid systems. The
systems are modeled with timed automata and timing properties are
expressed with the CTL temp*Logic.
I am not sure, but it seems that PtolemyII will cover SHIFT and Hytech
Any idea or explanation ?