Advertisement

Abstract Interpretation of MATLAB Code with Interval Sets

  • Christian DernehlEmail author
  • Norman Hansen
  • Stefan Kowalewski
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9933)

Abstract

In this paper we present how formal methods can be applied to MATLAB programs. We apply a static analysis based on abstract interpretation to derive reachable values and identify potential programming faults fully automatically. Our verification is built on a formalization and abstraction of matrices, structures and data types, such as integers and IEEE-754 floats. Combined with previously presented static analysis for Simulink, our tool can verify block diagrams with embedded MATLAB code. We show the feasibility of our tool and compare our solutions against a commercial tool, using real world applications.

Keywords

Abstract Interpretation Valuation Function Cell Array Abstract Domain Array Access 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Notes

Acknowledgements

This project was funded within the Priority Programme “Cooperatively Interacting Automobiles” of the German Science Foundation DFG (SPP 1835). The authors acknowledge the fruitful collaboration with the project partners.

References

  1. 1.
    Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model forstatic analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1977, New York, NY, USA (1977)Google Scholar
  2. 2.
    Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Rival, X.: Why does Astrée scale up? Formal Methods Syst. Des. 35(3), 229–264 (2009)CrossRefzbMATHGoogle Scholar
  3. 3.
    Dernehl, C., Hansen, N., Gerlitz, T., Kowalewski, S.: Static value range analysis for MATLAB/simulink-models. In: INFORMATIK 2015 (2015)Google Scholar
  4. 4.
    Dernehl, C., Hansen, N., Kowalewski, S.: Combining abstract interpretation with symbolic execution for a static value range analysis of block diagrams. In: De Nicola, R., Kühn, E. (eds.) SEFM 2016. LNCS, vol. 9763, pp. 137–152. Springer, Heidelberg (2016). doi: 10.1007/978-3-319-41591-8_10 CrossRefGoogle Scholar
  5. 5.
    Doherty, J., Hendren, L., Radpour, S.: Kind analysis for MATLAB. ACM SIGPLAN Not. 46(10), 99–118 (2011)CrossRefGoogle Scholar
  6. 6.
    Elphick, D., Leuschel, M., Cox, S.: Partial evaluation of MATLAB. In: Pfenning, F., Macko, M. (eds.) GPCE 2003. LNCS, vol. 2830, pp. 344–363. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  7. 7.
    Feret, J.: Static analysis of digital filters. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 33–48. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  8. 8.
    Gerlitz, T., Minh Tran, Q., Dziobek, C.: Detection and handling of model smells for MATLAB/simulink models. In: Proceedings of the International Workshop on Modelling in Automotive Software Engineering. CEUR (2015)Google Scholar
  9. 9.
    Granger, P.: Static analysis of arithmetical congruences. Int. J. Comput. Math. 30, 165–190 (1989)CrossRefzbMATHGoogle Scholar
  10. 10.
    Hickey, T., Ju, Q., Van Emden, M.H.: Interval arithmetic: from principles to implementation. J. ACM (JACM) 48, 1038–1068 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Kim, S.J., Koh, K., Boyd, S., Gorinevsky, D.: l1 trend filtering. SIAM Rev. 51, 339–360 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Lu, Z., Mukhopadhyay, S.: Model-based static code analysis for MATLAB models. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part I. LNCS, vol. 7609, pp. 474–487. Springer, Heidelberg (2012)Google Scholar
  13. 13.
    Miné, A.: Relational abstract domains for the detection of floating-point run-time errors. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 3–17. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  14. 14.
    Miné, A.: The octagon abstract domain. High.-Order Symb. Comput. 19, 31–100 (2006)CrossRefzbMATHGoogle Scholar
  15. 15.
    Rohn, J.: Interval linear programming. In: Rohn, J. (ed.) Linear Optimization Problems with Inexact Data, pp. 79–100. Springer US, Boston (2006)CrossRefGoogle Scholar
  16. 16.
    Rümmer, P., Wahl, T.: An SMT-LIB theory of binary floating-point arithmetic. In: International Workshop on Satisfiability Modulo Theories (SMT) (2010)Google Scholar
  17. 17.
    Stattelmann, S., Biallas, S., Schlich, B., Kowalewski, S.: Applying static code analysis on industrial controller code. In: 19th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA). IEEE (2014)Google Scholar

Copyright information

© Springer International Publishing AG 2016

Authors and Affiliations

  • Christian Dernehl
    • 1
    Email author
  • Norman Hansen
    • 1
  • Stefan Kowalewski
    • 1
  1. 1.Lehrstuhl Informatik 11 - Embedded SoftwareRWTH Aachen UniversityAachenGermany

Personalised recommendations