Advertisement

A Case for Certifying Compilers in Industrial Automation

  • Jan Olaf Blech
Chapter

Abstract

Certifying Compilers are compilers that (1) compile programs from a source language into a target language, and (2) check their results for each compilation run by using a separate dedicated checker. In many cases, certifying compilers can guarantee compilation correctness for individual compilation runs, i.e., they guarantee that target code is a correct translation of given source code. This paper advocates the use of certifying compilers in industrial automation: It describes basic principles, potential benefits and future research directions: it connects work on certifying compilers, compiler correctness, and verification approaches in the area of industrial automation.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    B. Fernandez Adiego et al. “Applying Model Checking to Industrial-Sized PLC Programs”. In: IEEE Trans. Industrial Informatics. IEEE, 2015.Google Scholar
  2. 2.
    B. Fernandez Adiego et al “Model-based Automated Testing of Critical PLC Programs”. In: Model-based Automated Testing of Critical PLC Programs. Industrial Informatics (INDIN). IEEE, 2013.Google Scholar
  3. 3.
    R. Wilhelm et al. “The Worst-case Execution-time Problem—overview of Methods and Survey of Tools”. In: ACM Transactions on Embedded Computing Systems (TECS). ACM, 2008.Google Scholar
  4. 4.
    N. Bauer et al. “Verification of PLC Programs given as Sequential Function Charts”. In: Integration of software specification techniques for applications in Engineering. Springer Berlin Heidelberg, 2004.CrossRefGoogle Scholar
  5. 5.
    S. Biallas, J. Brauer, and S. Kowalewski. “PLC: A Verification Platform for Programmable Logic Controllers”. In: 27th IEEE/ACM International Conference on Automated Software Engineering. ACM, 2012.Google Scholar
  6. 6.
    J. O. Blech and A. Poetzsch-Heffter. “A Certifying Code Generation Phase”. In: Compiler Optimization meets Compiler Verification (COCV 2007), Braga, Portugal. Elsevier ENTCS, 2007.Google Scholar
  7. 7.
    J. O. Blech and B. Grégoire. “Certifying Code Generation Runs with Coq: A Tool Description”. In: Compiler Optimization meets Compiler Verification (COCV 2008), Budapest, Hungary. 2008.Google Scholar
  8. 8.
    J. O. Blech and B. Grégoire. “Certifying Code Generation with Coq”. In: Compiler Optimization meets Compiler Verification (COCV 2008), Budapest, Hungary. 2008.Google Scholar
  9. 9.
    J. O. Blech and B. Grégoire. “Using Checker Predicates in Certifying Code Generation.” In: Compiler Optimization meets Compiler Verification (COCV 2009), York, UK. 2009.Google Scholar
  10. 10.
    J. O. Blech and S. Ould Biha. “Verification of PLC Properties Based on Formal Semantics in Coq”. In: 9th International Conference on Software Engineering and Formal Methods (SEFM). LNCS, Springer, 2011.Google Scholar
  11. 11.
    J. O. Blech, I. Schaefer, and A. Poetzsch-Heffter. “Translation Validation for System Abstractions”. In: Runtime Verification (RV’07), Vancouver, Canada. LCNS, Springer Verlag, 2007.Google Scholar
  12. 12.
    J. O. Blech, P. Lindgren, D. Pereira, V. Vyatkin and A. Zoitl. “A Comparison of Formal Verification Approaches for IEC 61499”. In: Emerging Technologies and Factory Automation (ETFA). IEEE, 2016.Google Scholar
  13. 13.
    M. A. Dave. “Compiler Verification: A Bibliography”. In: ACM SIGSOFT Software Engineering Notes ACM, 2003.CrossRefGoogle Scholar
  14. 14.
    Drossopoulou et al. “Formal Techniques for Java-like Programs”. In: European Conference on Object-Oriented Programming Springer, 2002.Google Scholar
  15. 15.
    G. Frey and L. Litz. “Formal Methods in PLC Programming”. In: IEEE International Conference on Systems, Man, and Cybernetics IEEE, 2000.Google Scholar
  16. 16.
    M. J. Gawkowski, J. O. Blech, and A. Poetzsch-Heffter. “Certifying Compilers based on Formal Translation Contracts”. In: Technical Report 355–06. University of Kaiserslautern, 2006.Google Scholar
  17. 17.
    H–M. Hanisch et al. “One Decade of IEC 61499 Modeling and Verification-results and Open Issues”. In: Reprints of the 13th IFAC Symposium on Information Control Problems in Manufacturing. 2009.Google Scholar
  18. 18.
    J. O. Blech and B. Grégoire. “Certifying Compilers Using Higher Order Theorem Provers as Certificate Checkers”. In: Formal Methods in System Design. Springer-Verlag, 2010.Google Scholar
  19. 19.
    J. O. Blech and M. Périn. “Generating Invariant-based Certificates for Embedded Systems”. In: Transactions on Embedded Computing Systems (TECS). ACM, 2012.Google Scholar
  20. 20.
    H. Kagermann, W. Wahlster, and J. Helbig. Recommendations for Implementing the Strategic Initiative INDUSTRIE 4.0 – Final Report of the Industrie 4.0 Working Group. 2013.Google Scholar
  21. 21.
    G. T Leavens, K. R. M. Leino, and P. Müller. “Specification and Verification Challenges for Sequential Object-oriented Programs”. In: Formal Aspects of Computing. Springer, 2007.Google Scholar
  22. 22.
    J. McCarthy and J. Painter. “Correctness Of A Compiler For Arithmetic Expression”. In: Proceedings Symposium in Applied Mathematics, Vol 19. Mathematical Aspects of Computer Science, 1967.Google Scholar
  23. 23.
    P. Müller and M. Nordio. “Proof-transforming Compilation of Programs with Abrupt Termination”. In: Proceedings of the 2007 conference on Specification and verification of component-based systems: 6th Joint Meeting of the European Conference on Software Engineering and the ACM SIGSOFT Symposium on the Foundations of Software Engineering. ACM, 2007.Google Scholar
  24. 24.
    G. C. Necula. “Translation Validation for an Optimizing Compiler”. In: ACM sigplan notices. Vol. 35. No. 5. ACM, 2000.Google Scholar
  25. 25.
    G. C. Necula and P Lee. “The Design and Implementation of a Certifying Compiler”. In: ACM SIGPLAN Notices. ACM, 1998.Google Scholar
  26. 26.
    I. D. Peake and J. O. Blech. “A Candidate Architecture for Cloud-based Monitoring in Industrial Automation”. In: 2017 IEEE International Conference on Software Quality Reliability and Security Companion (QRS-C). IEEE, 2017.Google Scholar
  27. 27.
    A. Pnueli, M. Siegel, and E. Singerman. “Translation Validation”. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 1998.Google Scholar
  28. 28.
    A. Poetzsch-Heffter and M. Gawkowski. “Towards Proof Generating Compilers”. In: Electronic Notes in Theoretical Computer Science. Elsevier, 2005.Google Scholar
  29. 29.
    B. Schlich, J. Brauer, and S. Kowalewski. “Application of Static Analyses for State-space Reduction to the Microcontroller Binary Code”. In: Science of Computer Programming Elsevier, 2011.Google Scholar
  30. 30.
    M. Wenger et al. “Remote Monitoring Infrastructure for IEC 61499 Based Control Software”. In: 8th International Congress on Ultra Modern Telecommunications and Control Systems. IEEE, 2016.Google Scholar
  31. 31.
    J. Yoo et al. “PLC-Based Safety Critical Software Development for Nuclear Power Plants”. In: In International Conference on Computer Safety, Reliability, and Security. Springer, 2004.Google Scholar
  32. 32.
    A. Zoitl and R. Lewis, eds. Modelling Control Systems using IEC 61499. IET, 2014. ISBN: 978-1-84919-760-1.Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Jan Olaf Blech
    • 1
  1. 1.AltranMunichGermany

Personalised recommendations