The Matlab/Simulink language has become the standard formalism for modeling
and implementing control software in areas like avionics, automotive,
railway, and process automation.  Such software is often safety critical,
and bugs have potentially disastrous consequences for people and material
involved.  We define a verification methodology to assess the correctness of
Simulink programs by means of automated test-case generation.  In the style
of fault- and mutation-based testing, the coverage of a Simulink program by
a test suite is defined in terms of the detection of injected faults.  Using
bounded model checking techniques, we are able to effectively and
automatically compute test suites for given fault models.  Several
optimisations are discussed to make the approach practical for realistic
Simulink programs and fault models, and to obtain accurate coverage
measures.