Advertisement

Tool for Translating Simulink Models into Input Language of a Model Checker

  • B. Meenakshi
  • Abhishek Bhatnagar
  • Sudeepa Roy
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4260)

Abstract

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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    DO-178B guidelines. Available from: http://www.rtca.org/
  2. 2.
  3. 3.
  4. 4.
    NuSMV web page: http://nusmv.irst.itc.it/
  5. 5.
  6. 6.
  7. 7.
    Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers 35(8), 677–691 (1986)zbMATHCrossRefGoogle Scholar
  8. 8.
    Camus, J.-L., Dion, B.: Efficient development of airborne software with scade-suite. Technical report, Esterel Technologies (2003)Google Scholar
  9. 9.
    Clarke, E.M., Wing, J.M.: Formal methods: state of the art and future directions. ACM Computing Surveys 28(4), 626–643 (1996)CrossRefGoogle Scholar
  10. 10.
    Dajani-Brown, S., Cofer, D., Hartman, G., Pratt, S.: Formal modeling and analysis of an avionics triplex sensor voter. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 34–48. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  11. 11.
    Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: Ardis, M. (ed.) Proc. 2nd Workshop on Formal Methods in Software Practice (FMSP 1998), pp. 7–15. ACM Press, New York (1998)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • B. Meenakshi
    • 1
  • Abhishek Bhatnagar
    • 1
  • Sudeepa Roy
    • 1
  1. 1.Honeywell Technology Solutions LabBangaloreIndia

Personalised recommendations