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