Assertional methods for mobile asynchronous channels in Java

Project code: Moby-J Research group: Research group: Formal methods for coordination languages (SEN3.2)Start: 2001-10-01End: 2004-09-30Project coordinator: Dr. M.M. Bonsangue

Project code: Moby-J
Research group: Research group: Formal methods for coordination languages (SEN3.2)

Start: 2001-10-01
End: 2004-09-30

Project coordinator: Dr. M.M. Bonsangue

The project aims at the development of a programming environment which supports component-based design and verification of Java programs. We define an extension of the Java language called MobiJ with a notion of component which allows for the encapsulation of its internal data-processing and composition by means of mobile asynchronous channels. The programming environment for MobiJ will include tools for specification and verification based on assertional methods. These assertional methods extend and generalize the Object Constraint Language (OCL) used in the Unified Modeling Language.

This is a project previous to the Moby-J project Formal methods for components and objects

Members

Prof.dr. F. Arbab, Prof.dr. F.S. de Boer, Dr. M.M. Bonsangue, Drs. J.V. Guillen Scholten,
Drs. J.F. Jacob

Key publications

  • Farhad Arbab, Abstract Behavior types: a foundation model for components and their composition. In Proceedings of FMCO'02, Leiden, LNCS 2582 Springer-Verlag, 2003.
  • Erika Abraham, Marcello M. Bonsangue, Frank S. de Boer, Martin Steffen, A Structural Operational Semantics for a Concurrent Class Calculus. In CAU technical report 0307, August 2003. PDF-file (197 KB) (16 pages)
  • Erika Abraham, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen, A Compositional Operational Sematics for JavaMT. In Proceedings of the International Symposium on Verification (Theory and Practice), Celebrating Zohar Manna's 64th Birthday, LNCS 2003, Springer-Verlag
  • Erika Abraham, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen, A Tool-supported Proof System for Multithreaded Java. In Proceedings of FMCO'02, Leiden, LNCS 2582 Springer-Verlag, 2003.
  • J. Guillen-Scholten, F. Arbab, F.S. de Boer, and M.M. Bonsangue, A channel-based Coordination Model for Components. In A. Brogi and J.M. Jacquet, editors, Proceedings of the 1st International Workshop on Foundations of Coordination Languages and Software Architectures (FoCLaSA 02), ENTCS 68(3), Elsevier Science, 2002.
  • J. Guillen-Scholten, F. Arbab, F.S. de Boer, and M.M. Bonsangue, MoCha: a Middleware Based on Mobile Channels. In Proceedings of 26th Internation Conference on Computer Software and Application Conference (COMPSAC 02), IEEE Computer Society Press, 2002.

Project reports

Publications in CWI reports

Cooperation

  • University of Kiel
  • LIACS - University of Leiden

Mobi-J is a project founded by a bilateral research program of The Netherlands Organization for Scientic Research (NWO) and the Central Public Funding Organization for Academic Research in Germany (DFG).