UseCases¶
Our tool is a compiler translating Simulink models with observers to Lustre code with observers.
In order to express the synchronous observers on a Simulink model, we provide an Observer block. This block is a masked sub-system with one parameter named parameterType.
Here is the Simulink graphical block:
And the parameter definition window:
The Simulink source file containing this block is provided here: ObserverBlock.mdl.
Counter use-case¶
The first use case is the model of a counter. The counter will activate its output every four tick and start activating its output after the three first ticks.
Here is the graphical view of its Simulink model:
Simulink source model is provided in Counter.mdl
Generated Lustre code and C code are provided in Counter.tar.gz.
Voter use-case¶
The first use case is the model of a simplified voter. Such a voter take as inputs the outputs of three sensors measuring the same parameter, the interval of legal input values (maximum and minimum) and a delta tallying with the maximum acceptable uncertainty of measurement. Its purpose is to compute a valid input for the controller from its three input values and to report occasional measurement errors.
A graphical view of the Simulink model is provided in simple_voter_obs.png. In this picture, system model elements are depicted in black whereas verification related architecture (observers) is displayed in red.
Simulink source model is provided in TriplexVoter.mdl
Generated Lustre code and C code are provided in TriplexVoter.tar.gz