[moca] Paper: Formal Analysis of a Distributed Object-Oriented Language and Runtime

[Alex Ahern <aja@xxxxxxxxxxxx>]

Dear all,

We would like to announce the following paper

 Formal Analysis of a Distributed Object-Oriented Language and Runtime

We have extended a core sequential Java for distribution,
including RMI, class downloading, serialisation and code mobility.
One of the interesting points for the moca-readers would be
that we model hidden concerns as runtime expressions
based on study in the pi-calculus.

It can be downloaded from:

http://www.doc.ic.ac.uk/~aja/dcbl.html

We hope you find it interesting, and we welcome any comments.

Best wishes,

Alex Ahern
(aja@xxxxxxxxxxxx)

============================================

[Title]

Formal Analysis of a Distributed Object-Oriented Language and Runtime

[Author]

Alexander Ahern and Nobuko Yoshida

[Abstract]

Distributed language features form an important part of modern
object-oriented programming.  In spite of their prominence in today's
computing environments, the formal semantics of distributed primitives
for object-oriented languages have not been well-understood, in
contrast to their sequential part.  This makes it difficult to perform
rigorous analysis of their behaviour and develop formally founded
safety methodologies.  As a first step to rectify this situation, we
present an operational semantics and typing system for a Java-like
core language with primitives for distribution. The language captures
the crucial but often hidden concerns involved in distributed objects,
including object serialisation, dynamic class downloading and remote
method invocation. We propose several invariant properties that
describe important correctness conditions for distributed runtime
behaviour.  These invariants also play a fundamental role in
establishing type safety, and help bound the design space for
extensions to the language. The semantics of the language are
constructed modularly, allowing straightforward extension, and this is
exploited by adding primitives for direct code distribution to the
language: thunk passing. Typing rules for the new primitives are
developed using the invariants as an analysis tool, with type
soundness ensuring that their inclusion does not violate safety
guarantees.

[/Abstract]

--
Alex Ahern <http://www.doc.ic.ac.uk/~aja/>
 
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html