Skip to main content
SpringerLink
Log in
Book cover

Embedded Systems – Modeling, Technology, and Applications pp 21–32Cite as

Efficient Construction and Verification of Embedded Software

  • Conference paper

  • 706 Accesses

This is a preview of subscription content, 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   129.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD   169.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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [BG04] Jan Olaf Blech and Sabine Glesner. A Formal Correctness Proof for Code Generation from SSA Form in Isabelle/HOL. In Informatik 2004 -Informatik verbindet, 34. Jahrestagung der Gesellschaft für Informatik (GI), Band 2, pages 449-558, 2004. Lecture Notes in Informatics (LNI).

    Google Scholar 

  2. [BGG05] Jan Olaf Blech, Lars Gesellensetter, and Sabine Glesner. Formal Verification of Dead Code Elimination in Isabelle/HOL. In Proc. 3rd IEEE International Conference on Software Engineering and Formal Methods, Koblenz, Germany, September 2005. IEEE Computer Society Press.

    Google Scholar 

  3. [BGL05] Jan Olaf Blech, Sabine Glesner, and Johannes Leitner. Formal Verification of Java Code Generation from UML Models. In Proceedings of the 3rd International Fujaba Days 2005: MDD in Practice. Technical Report, University of Paderborn, September 2005.

    Google Scholar 

  4. [BGLM05] Jan Olaf Blech, Sabine Glesner, Johannes Leitner, and Steffen Mülling. Optimizing Code Generation from SSA Form: A Comparison Between Two Formal Correctness Proofs in Isabelle/HOL. In Proc. Workshop Compiler Optimization meets Compiler Verification (COCV 2005), 8th Europ. Conf. on Theory and Practice of Software (ETAPS 2005), pages 1-18, 2005. Elsevier, Electronic Notes in Theor. Comp. Sc. (ENTCS).

    Google Scholar 

  5. Manuel Blum and Sampath Kannan. Designing Programs that Check Their Work. Journal of the ACM, 42(1):269-291, 1995.

    Article  MATH  Google Scholar 

  6. R. Cytron, J. Ferrante, B. K. Rosen, M. N. Wegman, and F. K. Zadeck. Efficiently Computing Static Single Assignment Form and the Control Dependence Graph. ACM TOPLAS, 13(4):451-490, October 1991.

    Article  Google Scholar 

  7. Laurian M. Chirica and David F. Martin. Toward Compiler Imple-mentation Correctness Proofs. ACM TOPLAS, 8(2):185-214, April 1986.

    Article  MATH  Google Scholar 

  8. Axel Dold, Friedrich W. von Henke, and Wolfgang Goerigk. A Completely Verified Realistic Bootstrap Compiler. International Journal of Foundations of Computer Science, 14(4):659-680, 2003.

    Article  MATH  MathSciNet  Google Scholar 

  9. Daniel Große and Rolf Drechsler. Checkers for SystemC Designs. In Proc. Second ACM & IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'2004), pages 171-178, 2004.

    Google Scholar 

  10. [GFJ04] Sabine Glesner, Simone Forster, and Matthias Jäger. A Program Result Checker for the Lexical Analysis of the GNU C Compiler. In Proc. Workshop Compiler Optimization meets Compiler Verification (COCV 2004), 7th Europ. Conf. on Theory and Practice of Software (ETAPS 2004), pages 1-16, 2004. Elsevier, Electronic Notes in Theor. Comp. Science.

    Google Scholar 

  11. [GG06] Lars Gesellensetter and Sabine Glesner. Only the Best Can Make It: Optimal Component Selection. In Workshop Formal Foundations of Embedded Software and Component-Based Software Architectures (FESCA 2006), 9th Europ. Conf. on Theory and Practice of Software (ETAPS 2006), 2006. Elsevier, Electr. Notes in Theor. Comp. Sc. (ENTCS).

    Google Scholar 

  12. [GGZ98] Wolfgang Goerigk, Thilo Gaul, and Wolf Zimmermann. Correct Programs without Proof? On Checker-Based Program Verification. In Tool Support for System Specification and Verification, ATOOLS 98, pages 108-123, 1998. Springer Series Advances in Computing Science.

    Google Scholar 

  13. S. Glesner, G. Goos, W. Zimmermann. Verifix: Konstruktion und Architektur verifizierender Übersetzer(Verifix: Construction and Architecture of Verifying Compilers). It-information Technology, 46:265-276, 2004.

    Article  Google Scholar 

  14. [GKC01] Thilo Gaul, Antonio Kung, and Jerome Charousset. AJACS: Applying Java to Automotive Control Systems. In Conf. Proc. of Embedded Intelligence 2001, Nürnberg, pages 425-434. Design & Elektronik, 2001.

    Google Scholar 

  15. [Gle03a] Sabine Glesner. Program Checking with Certificates: Separating Correctness-Critical Code. In Proc. 12th Int l FME Symposium (Formal Methods Europe), pages 758-777, 2003. Springer Verlag, LNCS Vol. 2805.

    Google Scholar 

  16. Sabine Glesner. Using Program Checking to Ensure the Correctness of Compiler Implementations. Journal of Universal Computer Science (J. UCS), 9(3):191-222, March 2003.

    Google Scholar 

  17. [HGG+99] A. Heberle, T. Gaul, W. Goerigk, G. Goos, and W. Zimmermann. Construction of Verified Compiler Front-Ends with Program-Checking. Perspectives of System Informatics, PSI 99, 1999. Springer LNCS Vol. 1755.

    Google Scholar 

  18. Gerwin Klein and Tobias Nipkow. Verified Bytecode Verifiers. Theoretical Computer Science, 298:583-626, 2003.

    Article  MATH  MathSciNet  Google Scholar 

  19. [MN98] Kurt Mehlhorn and Stefan Näher. From Algorithms to Working Programs: On the Use of Program Checking in LEDA. 23rd Int l Symp. on Math. Found. of Comp. Sc. (MFCS 98), 1998. Springer LNCS Vol. 1450.

    Google Scholar 

  20. J. S. Moore. A Mechanically Verified Language Implementation. Journal of Automated Reasoning, 5(4):461-492, 1989.

    Google Scholar 

  21. [MP67] John McCarthy and J. Painter. Correctness of a Compiler for Arithmetic Expressions. In Mathem. Aspects of Computer Science, Proc. Symposia in Applied Mathematics, pages 33-41. American Mathem. Society, 1967.

    Google Scholar 

  22. [Nec97] George C. Necula. Proof-Carrying Code. In Proc. 24th ACM SIGPLAN-SIGACT Symp. on Principles of Progr. Languages (POPL 97), 1997.

    Google Scholar 

  23. A. Nymeyer and J. -P. Katoen. Code generation based on formal BURS theory and heuristic search. Acta Informatica 34, pages 597-635, 1997.

    Article  MathSciNet  Google Scholar 

  24. [NPW02] Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer LNCS Vol. 2283, 2002.

    Google Scholar 

  25. C. H. Papadimitriou. Computational Complexity. Addison-Wesley, 1994.

    MATH  Google Scholar 

  26. [Pol81] Wolfgang Polak. Compiler Specification and Verification. Springer Verlag, Lecture Notes in Computer Science, Vol. 124, 1981.

    Google Scholar 

  27. [PSS98] A. Pnueli, M. Siegel, E. Singerman. Translation validation. In Tools and Algor. for the Constr. and Anal. of Systems, 1998. Springer LNCS 1384.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Software Engineering for Embedded Systems, Technische Universität Berlin, Germany

    Sabine Glesner

Authors
  1. Sabine Glesner
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Real-Time Systems and Robotics, Technische Universität Berlin, Berlin, Germany

    Günter Hommel

  2. Intelligent Computer-Human Interface, Shanghai Jiao Tong University, Shanghai, China

    Sheng Huanye

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer

About this paper

Cite this paper

Glesner, S. (2006). Efficient Construction and Verification of Embedded Software. In: Hommel, G., Huanye, S. (eds) Embedded Systems – Modeling, Technology, and Applications. Springer, Dordrecht. https://doi.org/10.1007/1-4020-4933-1_3

Download citation

  • DOI: https://doi.org/10.1007/1-4020-4933-1_3

  • Publisher Name: Springer, Dordrecht

  • Print ISBN: 978-1-4020-4932-3

  • Online ISBN: 978-1-4020-4933-0

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation