Tool for translating simulink models into input language of a model checker

Journal Article (Journal Article)

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. © Springer-Verlag Berlin Heidelberg 2006.

Full Text

Duke Authors

Cited Authors

  • Meenakshi, B; Bhatnagar, A; Roy, S

Published Date

  • January 1, 2006

Published In

Volume / Issue

  • 4260 LNCS /

Start / End Page

  • 606 - 620

Electronic International Standard Serial Number (EISSN)

  • 1611-3349

International Standard Serial Number (ISSN)

  • 0302-9743

Digital Object Identifier (DOI)

  • 10.1007/11901433_33

Citation Source

  • Scopus