A Deductive Proof System for Multithreaded Java with Exceptions

• Autorzy: Ábrahám E. , de Boer F.S. , de Roever W-P. , Steffen M.
• Języki publikacji: EN

Abstrakty

EN

Besides the features of a class-based object-oriented language, Java integrates concurrency via its thread-classes, allowing for a multithreaded flow of control. Besides that, the language offers a flexible exception mechanism for handling errors or exceptional program conditions. To reason about safety-properties of Java-programs and extending previous work on the proof theory for monitor synchronization, we introduce in this paper an assertional proof method for JavaMT ("Multi-Threaded Java"), a small concurrent sublanguage of Java, covering concurrency and especially exception handling. We show soundness and relative completeness of the proof method.

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 82, nr 4
• Strony: 391--463
• Opis fizyczny: bibliogr. 57 poz.

Twórcy

autor

Ábrahám E.

autor

de Boer F.S.

autor

de Roever W-P.

autor

Steffen M.

• Albert-Ludwigs-University Freiburg, Fahnenbergplatz 79085, Freiburg,Germany,

Bibliografia

• [1] Ábrahám, E.: An Assertional Proof System forMultithreaded Java-Theory and Tool Support, Ph.D. Thesis, University of Leiden, 2004, Defended 20.1.2005.
• [2] Ábrahám, E., de Boer, F. S., de Roever,W.-P., Steffen,M.: Inductive Proof-Outlines forMonitors in Java, in: Najm et al. [34], 155-169, A longer version appeared as technical report TR-ST-03-1, April 2003.
• [3] Ábrahám, E., de Boer, F. S., de Roever, W.-P., Steffen, M.: Inductive Proof Outlines for Multithreaded Java with Exceptions, Technical Report 0313, Institut f¨ur Informatik und Praktische Mathematik, Christian-Albrechts-Universit¨at zu Kiel, December 2003.
• [4] Ábrahám, E., de Boer, F. S., de Roever, W.-P., Steffen, M.: A Compositional Operational Semantics for JavaMT, International Symposium on Verification (Theory and Practice), July 2003 (N. Derschowitz, Ed.), 2772, Springer-Verlag, 2004, A preliminary version appeared as Technical Report TR-ST-02-2, May 2002.
• [5] Ábrahám, E., de Boer, F. S., de Roever, W.-P., Steffen, M.: An Assertion-Based Proof System for Multithreaded Java, Theoretical Computer Science, 331, 2005.
• [6] Ábrahám -Mumm, E., de Boer, F. S.: Proof-Outlines for Threads in Java, Proceedings of CONCUR 2000 (C. Palamidessi, Ed.), 1877, Springer-Verlag, August 2000.
• [7] Ábrahám -Mumm, E., de Boer, F. S., de Roever, W.-P., Steffen, M.: A Tool-Supported Proof System for Monitors in Java, in: Bonsangue et al. [20], 1-32.
• [8] Ábrahám -Mumm, E., de Boer, F. S., de Roever, W.-P., Steffen, M.: Verification for Java's Reentrant Multithreading Concept, Proceedings of FoSSaCS 2002 (M. Nielsen, U. H. Engberg, Eds.), 2303, Springer-Verlag, April 2002, A longer version, including the proofs for soundness and completeness, appeared as Technical Report TR-ST-02-1,March 2002.
• [9] Alves-Foss, J., Ed.: Formal Syntax and Semantics of Java, vol. 1523 of Lecture Notes in Computer Science State-of-the-Art-Survey, Springer-Verlag, 1999.
• [10] Andrews, G. R.: Foundations of Multithreaded, Parallel, and Distributed Programming, Addison-Wesley, 2000.
• [11] Apt, K. R.: Ten Years of Hoare's Logic: A Survey - Part I, ACM Transactions on Programming Languages and Systems, 3(4), October 1981, 431-483.
• [12] Apt, K. R., Francez, N., de Roever, W.-P.: A Proof System for Communicating Sequential Processes, ACM Transactions on Programming Languages and Systems, 2, 1980, 359-385.
• [13] The Project Bali, http://isabelle.in.tum.de/Bali/, 2003.
• [14] van den Berg, J., Huisman, M., Jacobs, B., Poll, E.: A Type-Theoretic Memory Model for Verification of Sequential Java Programs, Recent Trends in Algebraic Development Techniques (D. Bert, C. Choppy, P. Mosses, Eds.), 1827, Springer-Verlag, 2000, An earlier version appeared as Computer Science Institute, University of Nijmegen, Technical Report CSI-R9926, 1999.
• [15] van den Berg, J., Jacobs, B.: The Loop Compiler for Java and JML, Tools and Algorithms for the Construction and Analysis of Systems(TACAS '02) (T. Margaria,W. Yi, Eds.), 2031, Springer-Verlag, 2002.
• [16] van den Berg, J., Jacobs, B., Poll, E.: Formal Specification and Verification of JavaCard's Application Identifier Class, Java on Smart Cards: Programming and Security. Revised Papers, Java Card 2000, International Workshop, Cannes, France (I. Attali, T. Jensen, Eds.), 2001.
• [17] de Boer, F. S.: A WP-Calculus for OO, Proceedings of FoSSaCS '99 (W. Thomas, Ed.), 1578, Springer-Verlag, 1999.
• [18] de Boer, F. S., Pierik, C.: Computer-Aided Specification and Verification of Annotated Object-Oriented Programs, Proceedings of the Fifth International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 2002) (B. Jacobs, A. Rensink, Eds.), 209, Kluwer, 2002.
• [19] de Boer, F. S., Pierik, C.: Towards an Environment for the Verification of Annotated Object-Oriented Programs, Technical report UU-CS-2003-002, Institute of Information and Computing Sciences, University of Utrecht, January 2003.
• [20] Bonsangue, M. M., de Boer, F. S., de Roever, W.-P., Graf, S., Eds.: Proceedings of the First International Symposium on Formal Methods for Components and Objects (FMCO 2002), Leiden, vol. 2852 of Lecture Notes in Computer Science, Springer-Verlag, 2003.
• [21] Cenciarelli, P., Knapp, A., Reus, B., Wirsing, M.: An Event-Based Structural Operational Semantics of Multi-Threaded Java, in: Alves-Foss [9], 157-200.
• [22] Floyd, R. W.: Assigning Meanings to Programs, Proc. Symposia in Applied Mathematics: Mathematical Apsecs of Computer Science (J. T. Schwartz, Ed.), 1967.
• [23] Hoare, C. A. R.: An Axiomatic Basis for Computer Programming, Communications of the ACM, 12(10), 1969, 576-580.
• [24] Huisman, M.: Java Program Verification in Higher-Order Logic with PVS and Isabelle, Ph.D. Thesis, University of Nijmegen, 2001.
• [25] Huisman, M., Jacobs, B.: Inheritance in Higher Order Logic: Modeling and Reasoning, Theorem Proving in Higher Order Logics (TPHOL 2000) (M. Aagaard, J. Harrison, Eds.), 1869, An earlier version appeared as Technical Report CSI-R0004 Computing Science Institute, University of Nijmegen., 2000.
• [26] Huisman, M., Jacobs, B., van den Berg, J.: A Case Study in Class Library Verification: Java's Vector Class, Software Tools for Technology Transfer, 3(3), 2001, 332-352.
• [27] Jacobs, B.: A Formalisation of Java's Exception Mechanism, Proceedings of ESOP 2001 (D. Sands, Ed.), 2028, Springer-Verlag, 2001.
• [28] Jacobs, B., van den Berg, J., Huisman,M., van Barkum,M., Hensel, U., Tews, H.: Reasoning about Classes in Java (Preliminary Report), Object Oriented Programming: Systems, Languages, and Applications (OOPSLA) '98 (Vancouver, Canada), ACM, 1998, In SIGPLAN Notices 30(10).
• [29] Jacobs, B., Kiniry, J.,Warnier,M.: Java ProgramVerification Challenges, in: Bonsangue et al. [20], 202-219.
• [30] Jacobs, B., Poll, E.: A Logic for the Java Modelling Language JML, Fundamental Approaches to Software Engineering (H. Hussmann, Ed.), 2029, Springer-Verlag, 2001.
• [31] Leavens, G. T., Leino, K. R. M., M¨uller, P.: Specification and Verification Challenges for Sequential Object-Oriented Programs, Formal Aspects of Computing, 2007, To appear.
• [32] Levin, G., Gries, D.: A Proof Technique for Communicating Sequential Processes, Acta Informatica, 15(3), 1981, 281-302.
• [33] The LOOP project: Formal methods for object-oriented systems, http://www.cs.kun.nl/_bart/LOOP/, 2001.
• [34] Najm, E., Nestmann, U., Stevens, P., Eds.: Proceedings of the 6th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS '03), Paris, vol. 2884 of Lecture Notes in Computer Science, Springer-Verlag, November 2003.
• [35] Nipkow, T.: Hoare Logics in Isabelle/HOL, Proof and System-Reliability (H. Schwichtenberg, R. Steinbrüggen, Eds.), Kluwer, 2002.
• [36] Nipkow, T., von Oheimb, D.: Java-light is Type-Safe-Definitely, Proceedings of POPL '98, ACM, 1998.
• [37] Nipkow, T., von Oheimb, D., Pusch, C.: μJava: Embedding a Programming Language in a Theorem Prover, Foundations of Secure Computation. Proc. Int. Summer School Marktoberdorf 1999 (F. L. Bauer, R. Steinbr¨uggen, Eds.), IOS Press, 2000.
• [38] von Oheimb, D.: Axiomatic Semantics for Javalight , in: Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications European Conference on Object-Oriented Programming (OOPSLA) (ECOOP), 2000.
• [39] von Oheimb, D.: Axiomatic Sematics for Javalight in Isabelle/HOL, Technical Report CSE 00-008, Oregon Graduate Institute, 2000.
• [40] von Oheimb, D.: Hoare Logic for Java in Isabelle/HOL, Concurrency and Computation: Practice and Experience, 13(13), 2001, 1173-1214.
• [41] von Oheimb, D., Nipkow, T.: Machine-Checking the Java Specification: Proving Type-Safety, in: Alves-Foss [9].
• [42] von Oheimb, D., Nipkow, T.: Hoare Logic for NanoJava: Auxiliary Variables, Side Effects and Virtual Methods revisited, Proceedings of Formal Methods Europe: Formal Methods - Getting IT Right (FME'02) (L.-H. Eriksson, P. A. Lindsay, Eds.), 2391, Springer-Verlag, 2002.
• [43] Owicki, S., Gries, D.: An Axiomatic Proof Technique for Parallel Programs, Acta Informatica, 6(4), 1976, 319-340.
• [44] Owre, S., Rushby, J. M., Shankar, N.: PVS: A Prototype Verification System, Automated Deduction (CADE-11) (D. Kapur, Ed.), 607, Springer-Verlag, 1992.
• [45] Paulson, L. C.: The Isabelle Reference Manual, Technical Report 283, University of Cambridge, Computer Laboratory, 1993.
• [46] Pierik, C.: Validation Techniques for Object-Oriented Proof Outlines, Ph.D. Thesis, Universiteit Utrecht, May 2006.
• [47] Pierik, C., de Boer, F. S.: A Syntax-Directed Hoare Logic for Object-Oriented Programming Concepts, in: Najm et al. [34], 64-78, An extended version appeared as University of Utrecht Technical Report UU-CS-2003-010.
• [48] Poetzsch-Heffter, A.: A Logic for the Verification of Object-Oriented Programs, Proceedings of Programming Languages and Fundamentals of Programming (R. Berghammer, F. Simon, Eds.), Institut f¨ur Informatik und Praktische Mathematik, Christian-Albrechts-Universit¨at zu Kiel, November 1997, Bericht Nr. 9717.
• [49] Poetzsch-Heffter, A.: Specification and Verification of Object-Oriented Programs, Technische Universität München, January 1997, Habilitationsschrift.
• [50] Poetzsch-Heffter, A., M¨uller, P.: Logical Foundations for Typed Object-Oriented Languages, Proceedings of PROCOMET '98 (D. Gries, W.-P. de Roever, Eds.), International Federation for Information Processing (IFIP), Chapman & Hall, 1998.
• [51] Poetzsch-Heffter, A., M¨uller, P.: A Programming Logic for Sequential Java, Programming Languages and Systems (S. Swierstra, Ed.), 1576, Springer, 1999.
• [52] Poll, E., van den Berg, J., Jacobs, B.: Specification of the JavaCard API in JML, Fourth Smart Card Research and Advanced Application Conference (CARDIS'2000) (J. Domingo-Ferrer, D. Chan, A. Watson, Eds.), Kluwer Acad. Publ., 2000.
• [53] Poll, E., van den Berg, J., Jacobs, B.: Formal specification of the Java Card API in JML: the APDU class, Computer Networks, 36(4), 2001, 407-421.
• [54] Stärk, R., Schmid, J., Börger, E.: Java and the Java Virtual Machine: Definition, Verification, Validation, Springer-Verlag, 2001.
• [55] Steffen, M.: Object-Connectivity and Observability for Class-Based, Object-Oriented Languages, Habilitation thesis, Technische Faktult¨at der Christian-Albrechts-Universit¨at zu Kiel, 2006, Submitted 4th. July, accepted 7. February 2007.
• [56] Tucker, J. V., Zucker, J. I.: Program Correctness over Abstract Data Types, with Error-State Semantics, vol. 6 of CWI Monograph Series, North-Holland, 1988.
• [57] Warmer, J. B., Kleppe, A. G.: The Object Constraint Language: Precise Modeling With UML, Object Technology Series, Addison-Wesley, 1999.