Skip to main content
SpringerLink
Log in

A Case for Certifying Compilers in Industrial Automation

  • Chapter
  • First Online:
Principled Software Development

  • 498 Accesses

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 109.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. B. Fernandez Adiego et al. “Applying Model Checking to Industrial-Sized PLC Programs”. In: IEEE Trans. Industrial Informatics. IEEE, 2015.

    Google Scholar 

  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. 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. 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.

    Chapter  Google Scholar 

  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. 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. 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. 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. 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. 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. 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. 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. M. A. Dave. “Compiler Verification: A Bibliography”. In: ACM SIGSOFT Software Engineering Notes ACM, 2003.

    Article  Google Scholar 

  14. Drossopoulou et al. “Formal Techniques for Java-like Programs”. In: European Conference on Object-Oriented Programming Springer, 2002.

    Google Scholar 

  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. 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. 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. 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. 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. 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. 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. 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. 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. G. C. Necula. “Translation Validation for an Optimizing Compiler”. In: ACM sigplan notices. Vol. 35. No. 5. ACM, 2000.

    Google Scholar 

  25. G. C. Necula and P Lee. “The Design and Implementation of a Certifying Compiler”. In: ACM SIGPLAN Notices. ACM, 1998.

    Google Scholar 

  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. 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. A. Poetzsch-Heffter and M. Gawkowski. “Towards Proof Generating Compilers”. In: Electronic Notes in Theoretical Computer Science. Elsevier, 2005.

    Google Scholar 

  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. 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. 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. A. Zoitl and R. Lewis, eds. Modelling Control Systems using IEC 61499. IET, 2014. ISBN: 978-1-84919-760-1.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Altran, Munich, Germany

    Jan Olaf Blech

Authors
  1. Jan Olaf Blech
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, ETH Zürich, Zürich, Switzerland

    Peter Müller

  2. Institut für Softwaretechnik und Fahrzeuginformatik, Technische Universität Braunschweig, Braunschweig, Germany

    Ina Schaefer

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Blech, J.O. (2018). A Case for Certifying Compilers in Industrial Automation. In: Müller, P., Schaefer, I. (eds) Principled Software Development. Springer, Cham. https://doi.org/10.1007/978-3-319-98047-8_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-98047-8_5

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-98046-1

  • Online ISBN: 978-3-319-98047-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation