Tool for Translating Simulink Models into Input Language of a Model Checker
Model Based Development (MBD) using Mathworks tools like Simulink, Stateflow etc. is being pursued in Honeywell for the development of safety critical avionics software. Formal verification techniques are well-known to identify design errors of safety critical systems reducing development cost and time. As of now, formal verification of Simulink design models is being carried out manually resulting in excessive time consumption during the design phase. We present a tool that automatically translates certain Simulink models into input language of a suitable model checker. Formal verification of safety critical avionics components becomes faster and less error prone with this tool. Support is also provided for reverse translation of traces violating requirements (as given by the model checker) into Simulink notation for playback.
Unable to display preview. Download preview PDF.
- 1.DO-178B guidelines. Available from: http://www.rtca.org/
- 2.Simulink web page: http://www.mathworks.com/products/simulink/
- 3.Stateflow web page: http://www.mathworks.com/products/stateflow/
- 4.NuSMV web page: http://nusmv.irst.itc.it/
- 5.Embedded Validator web page: http://www.dspaceinc.com/ww/en/inc/home/products/sw/pcgs/automatic_model_validation.cfm
- 6.Checkmate web page: http://www.ece.cmu.edu/~webk/checkmate/
- 8.Camus, J.-L., Dion, B.: Efficient development of airborne software with scade-suite. Technical report, Esterel Technologies (2003)Google Scholar