Skip to main content
SpringerLink
Log in

The Approach: Integrating Object Oriented Design and Formal Verification

  • Conference paper
  • First Online:
Logics in Artificial Intelligence (JELIA 2000)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1919))

Included in the following conference series:

Abstract

This paper reports on the ongoing KeY project aimed at bridging the gap between (a) object-oriented software engineering methods and tools and (b) deductive verification. A distinctive feature of our approach is the use of a commercial CASE tool enhanced with functionality for formal specification and deductive verification.

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight 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. J.-R. Abrial. The B Book — Assigning Programs to Meanings. Cambridge University Press, Aug. 1996.

    Google Scholar 

  2. K. R. Apt. Ten years of Hoare logic: A survey — part I. ACM Transactions on Programming Languages and Systems, 1981.

    Google Scholar 

  3. T. Baar. Experiences with the UML/OCL-approach to precise software modeling: A report from practice. Submitted, see http://i12www.ira.uka.de/~key, 2000.

  4. T. Baar, R. Hähnle, T. Sattler, and P. H. Schmitt. Entwurfsmustergesteuerte Erzeugung von OCL-Constraints. In G. Snelting, editor, Softwaretechnik-Trends, Informatik Aktuell. Springer, 2000.

    Google Scholar 

  5. B. Beckert. A dynamic logic for Java Card. In Proc. 2nd ECOOP Workshop on Formal Techniques for Java Programs, Cannes, France, 2000. See http://i12www.ira.uka.de/~key/doc/2000/beckert00.pdf.gz.

  6. E. Börger and W. Schulte. A programmer friendly modular definition of the semantics of Java. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, LNCS 1523, pages 353–404. Springer, 1999.

    Chapter  Google Scholar 

  7. R. Breu, R. Grosu, F. Huber, B. Rumpe, and W. Schwerin. Towards a precise semantics for object-oriented modeling techniques. In H. Kilov and B. Rumpe, editors, Proc Workshop on Precise Semantics for Object-Oriented Modeling Techniques at ECOOP’97. Techn. Univ. of Munich, Tech. Rep. TUM-I9725, 1997.

    Google Scholar 

  8. E. Clarke and J. M. Wing. Formal methods: State of the art and future directions. ACM Computing Surveys, 28(4):626–643, 1996.

    Article  Google Scholar 

  9. D. L. Dill and J. Rushby. Acceptance of formal methods: Lessons from hardware design. IEEE Computer, 29(4):23–24, 1996. Part of: Hossein Saiedian (ed.). An Invitation to Formal Methods. Pages 16–30.

    Google Scholar 

  10. R. B. France, J.-M. Bruel, M. M. Larrondo-Petrie, and E. Grant. Rigorous objectoriented modeling: Integrating formal and informal notations. In M. Johnson, editor, Proc. Algebraic Methodology and Software Technology (AMAST), Berlin, Germany, LNCS 1349. Springer, 1997.

    Google Scholar 

  11. E. Gamma, R. Helm, R. Johnson, and J. Vlissides. Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, 1995.

    Google Scholar 

  12. M. Giese. Integriertes automatisches und interaktives Beweisen: Die Kalkülebene. Diploma Thesis, Fakultät für Informatik, Universität Karlsruhe, June 1998.

    Google Scholar 

  13. M. Giese. A first-order simplification rule with constraints. In Proc. Int. Workshop on First-Order Theorem Proving, St. Andrews, Scotland, 2000. See http://i12www.ira.uka.de/~key/doc/2000/giese00a.ps.gz.

  14. M. Grand. Patterns in Java, volume 2. John Wiley & Sons, 1999.

    Google Scholar 

  15. S. B. Guthery. Java Card: Internet computing on a smart card. IEEE Internet Computing, 1(1):57–59, 1997.

    Article  Google Scholar 

  16. E. Habermalz. Interactive theorem proving with schematic theory specific rules. Technical Report 19/00, Fakultät für Informatik, Universität Karlsruhe, 2000. See http://12www.ira.uka.de/~key/doc/2000/stsr.ps.gz.

  17. U. Hansmann, M. S. Nicklous, T. Schäck, and F. Seliger. Smart Card Application Development Using Java. Springer, 2000.

    Google Scholar 

  18. M. G. Hinchey and J. P. Bowen, editors. Applications of Formal Methods. Prentice Hall, 1995.

    Google Scholar 

  19. I. Jacobson, G. Booch, and J. Rumbaugh. The Unified Software Development Process. Object Technology Series. Addison-Wesley, 1999.

    Google Scholar 

  20. D. Kozen and J. Tiuryn. Logic of programs. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, chapter 14, pages 789–840. Elsevier, Amsterdam, 1990.

    Google Scholar 

  21. K. Lano. The B Language and Method: A guide to Practical Formal Development. Springer Verlag London Ltd., 1996.

    Google Scholar 

  22. J. Martin and J. J. Odell. Object-Oriented Methods: A Foundation, UML Edition. Prentice-Hall, 1997.

    Google Scholar 

  23. T. Nipkow and D. von Oheimb. Machine-checking the Java specification: Proving type safety. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, LNCS 1523, pages 119–156. Springer, 1999.

    Google Scholar 

  24. Object Management Group, Inc., Framingham/MA, USA, http://www.omg.org. OMG Unified Modeling Language Specification, Version 1.3, June 1999.

  25. L. C. Paulson. Isabelle: A Generic Theorem Prover. Springer, Berlin, 1994.

    MATH  Google Scholar 

  26. A. Poetzsch-Heffter and P. Müller. A programming logic for sequential Java. In S. D. Swierstra, editor, Proc. Programming Languages and Systems (ESOP), Amsterdam, The Netherlands, LNCS 1576, pages 162–176. Springer, 1999.

    Google Scholar 

  27. W. Reif. The KIV-approach to software verification. In M. Broy and S. Jähnichen, editors, KORSO: Methods, Languages, and Tools for the Construction of Correct Software — Final Report, LNCS 1009. Springer, 1995.

    Chapter  Google Scholar 

  28. O. Slotosch. Overview over the project QUEST. In Applied Formal Methods, Proc. FM-Trends 98, Boppard, Germany, LNCS 1641, pages 346–350. Springer, 1999.

    Google Scholar 

  29. Sun Microsystems, Inc., Palo Alto/CA, USA. Java Card 2.1 Application Programming Interfaces, Draft 2, Release 1.3, 1998.

    Google Scholar 

  30. O. Traynor, D. Hazel, P. Kearney, A. Martin, R. Nickson, and L. Wildman. The Cogito development system. In M. Johnson, editor, Proc. Algebraic Methodology and Software Technology, Berlin, LNCS 1349, pages 586–591. Springer, 1997.

    Google Scholar 

  31. J. Warmer and A. Kleppe. The Object Constraint Language: Precise Modelling with UML. Object Technology Series. Addison-Wesley, 1999.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Complexity and Deduction Systems, University of Karlsruhe, Institute for Logic, D-76128, Karlsruhe, Germany

    Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Wolfram Menzel & Peter H. Schmitt

  2. Department of Computing Science, Chalmers University of Technology, S-41296, Gothenburg

    Reiner Hähnle

Authors
  1. Wolfgang Ahrendt
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Thomas Baar
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Bernhard Beckert
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Martin Giese
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Elmar Habermalz
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Reiner Hähnle
    View author publications

    You can also search for this author in PubMed Google Scholar

  7. Wolfram Menzel
    View author publications

    You can also search for this author in PubMed Google Scholar

  8. Peter H. Schmitt
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Applied Mathematics, E.T.S.I. Informática, University of Málaga, 29071, Málaga, Spain

    Manuel Ojeda-Aciego  & Inma P. de Guzmán  & 

  2. Intelligent Systems Department, Computer Science Institute, University of Leipzig, Augustusplatz 10-11, 04109, Leipzig, Germany

    Gerhard Brewka

  3. Center for Artificial Intelligence, Department of Computer Science, University of Lisbon, 2825-114, Caparica, Portugal

    LuĂ­s Moniz Pereira

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ahrendt, W. et al. (2000). The Approach: Integrating Object Oriented Design and Formal Verification. In: Ojeda-Aciego, M., de Guzmán, I.P., Brewka, G., Moniz Pereira, L. (eds) Logics in Artificial Intelligence. JELIA 2000. Lecture Notes in Computer Science(), vol 1919. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-40006-0_3

Download citation

  • DOI: https://doi.org/10.1007/3-540-40006-0_3

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-41131-4

  • Online ISBN: 978-3-540-40006-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation