On the Semantics of JavaSpaces
Roberto Gorrieri, University of Bologna, Italy
joint work with Nadia Busi and Gianluigi Zavattaro
Abstract:
JavaSpaces is a coordination middleware for distributed Java programming
recently proposed by Sun Microsystems. It is inspired by the Linda
coordination model: processes interact via the emission (out),
consumption (in), test for presence (rd) and the test
for absence (inp) of data inside a shared repository.
Three are the most interesting new features
introduced by JavaSpaces. The first one is an event notification
mechanism (notify): a process can register interest in the incoming
arrivals of a particular kind of data, and then receive communication of the
occurrence of these events. The second feature is the so-called
distributed leasing: at the moment a client outputs a tuple, it also
declares its required lifetime (that the server may satisfy only
partially). The third feature is a timeout on the blocking operation
of input: if no instance is found before the timeout expires, then the
operation fails and terminates. We present a structured operational
semantics for a process algebra featuring these coordination
primitives. This abstract semantics is used to clarify possible ambiguities
of the informal definitions of JavaSpaces, to discuss possible
implementation choices and to compare the expressive power of the new
primitives. Interestingly enough, many subtle phenomena occur, some of which
might lead to reconsider the actual choice of primitives.
Rewriting Logic and Maude:
a Wide-spectrum Semantic Framework for Open
Object-based Distributed Systems
Jose Meseguer, SRI International
Abstract:
Rewriting logic is ideally suited as a semantic framework for open
object-based distributed systems. Both the distributed states and the local
concurrent transitions of such systems can be naturally specified by rewrite
theories in which such local concurrent transitions are described by rewrite
rules. Maude is a high-performance rewriting logic language and system
developed at SRI International that supports executable specification and
programming, and a flexible variety of formal analyses.
Rewriting logic is a wide-spectrum semantic framework well suited to span the gap between high-level architectural designs and distributed or mobile system implementations. Rewriting logic has been used to give a precise semantics to a number of architectural notations and concepts, and to obtain partially- or fully-defined formal executable specifications from such notations. Using Maude, such executable specifications can then be analyzed in a variety of ways, including symbolic simulation and debugging, and flexible forms of model checking analysis. Furthermore, using model checkig analysis and formal proofs, formal properties of such specifications expressed in nonexecutable formalisms such as temporal and modal logics can be verified. Since under quite reasonable assuptions rewriting logic specifications can be directly implemented with competitive performance as distributed and mobile systems, it is in fact possible to span the gap from high-level designs to implementations without leaving the formal framework.
All this is quite ambitious, and has not yet been fully realized. However, thanks to the efforts of several research teams, a substantial body of encouraging experience at all levels of this project already exists. This paper introduces rewriting logic and Maude, and surveys the experience gained so far in applying them to open object-based distributed systems.
Object-Oriented Programming for Wide-Area Computing
Jayadev Misra, University of Texas at Austin
Abstract:
Object-based sequential programming has had a major impact on software
engineering. However, object-based concurrent programming remains
elusive as an effective programming tool. The class of applications
that will be implemented on future high-bandwidth networks of
processors will be significantly more ambitious than the current
applications (which are mostly involved with transmissions of digital
data and images), and object-based concurrent programming has the
potential to simplify designs of such applications. Many of the
programming concepts developed for databases, object-oriented
programming and designs of reactive systems can be unified into a
compact model of concurrent programs that can serve as the foundation
for designing these future applications.
There are several key questions in developing a model of concurrent-objects for wide-area computing. Foremost among the concerns is the difficulty associated with managing concurrent interactions, particularly when a multitude of machines interact. This is the main topic of this research. Additionally, issues of security and fault-tolerance are central to wide-area computing. How can a secure computation be carried out if the data and procedure reside at different machines? If a computation involves several thousand machines -- as would be expected for a computation on the world-wide web -- is it realistic to allow an unknown party to have exclusive access to a resource? That party may crash requiring a major roll-back effort. Is it reasonable to queue a caller for access to a resource when the resource manager could possibly fail, causing the caller to block? In this case, it may be more efficient to reject the call if the resource is not readily available. We seek a model that allows us to experiment with a variety of questions of this nature.
High Confidence Adaptive and Reflective Middleware: Fact or Fiction?
Doug Schmidt (DARPA ISO)
Abstract:
E-speak: the Technology for Ubiquitous E-services
Alan H. Karp, Hewlett-Packard Laboratories
Abstract:
Today, setting up a service to be used over the Internet is difficult,
special-case work. Part of the difficulty is that each provider of
such a service addresses a common set of problems in a proprietary
way. E-speak solves the problems of naming, describing, managing, and
controlling access in a manner that makes it easier and safer to allow
remote access. With e-speak, we can think of all applications as
e-services that we can enlist to solve our problems.
E-speak is the open-source software platform for creating, composing, mediating, managing, and accessing Internet-based e-services. With e-speak we can more easily build a world of universal e-services that can be accessed intuitively using a wide array of devices and platforms, from personal digital assistants, to PCs, information appliances, and supercomputers. With e-speak these e-services can interact with each other in order to advertise capabilities, discover other e-services, and ally with each other to offer new functionality, even negotiate to broker, bill, manage, and monitor each other - all in a dynamic, ad hoc, yet secure manner.
This talk will describe the requirements that led to the various features of the e-speak architecture as well as its key abstractions and innovations.
Behavioural Subtyping and Property Preservation
by Heike Wehrheim
Abstract:
Inheritance is one of the key features in object-oriented design and
analysis. It especially supports an incremental
development by allowing to stepwise add new functionality to an
existing system design.
When using a subclass which is a specialisation of a
certain superclass, the question arises which of the superclass'
properties still hold for the subclass. We investigate this topic
for three behavioural subtyping relations, which formalise the
subtyp - supertyp relationship among classes
on the basis of process algebra correctness relations. According to the
degree of change allowed by the subtyping relations, safety and
liveness properties of the superclass are preserved up to different
extents.
Requirements Level Semantics for UML Statecharts
by Rik Eshuis, Roel Wieringa
Abstract:
We propose a formal semantics for UML statecharts aimed at the
requirements level. A requirements level model assumes perfect
technology and has a considerably simpler semantics than an
implementation level model. Our semantics is an adaptation of
the STATEMATE statechart semantics, with local variables,
identifier addressing, point-to-point communication, synchronous
communication and dynamic object creation and deletion. We start
with an informal comparison of STATEMATE and UML statechart
semantics and then give a formalisation of our semantics in
terms of labelled transition systems.
A Step Toward Automatic Distribution of Java Programs
by Isabelle Attali, Denis Caromel, Romain Guider
Abstract:
This article investigates the automatic distribution and
parallelization of object-oriented programs.
We formally define a set of properties that allow to turn standard
objects into active objects to be distributed.
We first explain a principle of seamless sequential, multi-threaded
and distributed programming using Java, that enhances code reuse
and code distribution. We exhibit conditions on the graph of objects
to detect activable objects and transform a sequential program into
a distributed or parallel program using active objects.
Finally, we explain how these properties were implemented in order to
check them statically on a given Java program.
A Practical Approach to Incremental Specification
by Charles Lakos, Glenn Lewis
Abstract:
The object-oriented specification of concurrent and distributed
systems has tended to emphasise the aspect of substitutability at the
expense of code reuse. A variety of constraints has been imposed in order
to guarantee substitutability in one form or another. This paper argues
that the incremental development of software specifications needs to
consider substitutability in the context of code reuse. Further, the common
approach of starting with an abstract specification and then progressively
refining it (in some general way) means that many existing substitutability
constraints are too strong. In the context of Coloured Petri Nets, we
advocate the use of three specific forms of refinement type refinement,
subnet refinement, and node refinement. These have weaker demands for
substitutability, namely that every (complete) refined behaviour has a
corresponding abstract behaviour, but not necessarily vice versa. An
examination of case studies in the literature suggests that this approach is
applicable in practice.
Fail-Stop Components by Pattern Matching
by Tomasz Janowski, Wojciech Mostowski
Abstract:
We describe an approach to formally specify object-based software
components, in order to be able to automatically check their
behaviour at run-time. The specification is a regular expression
built from the propositions about the states (or pairs of states) of
a component. Checking is done by a specification-generated wrapper,
which produces a fail-stop component from a component which fails in
an arbitrary way. The wrapper-generator is implemented for a subset
of Java classes. We argue that specification-based error-detection
is particularly suitable for the components of open, object-based
distributed systems.
Behavior Expression and OMDD: A new methodology for ream-time distributed systems
by Yunming WANG, Albert BENVENISTE, Jean-Pierre TALPIN, Paul LE GUERNIC
Abstract:
In this paper, we will take advantage of UML and synchronous model
to propose a new methodology for the development of real-time
distributed systems. We will first propose a new language called
Behavior Expression, then will we provide its semantics and
compilation mechanism. We will also present OMDD as intermediate code
for compilation. Determinism and composability can be checked
directly by analyzing OMDDs, consequently, it allows partial
compilation. Furthermore, endochrony and isochrony can also be
verified by OMDDs, which ensure correct distribution of synchronous
system on asynchronous networks. Based on these benefits, we propose
a new methodology of development for real-time distributed systems by
integrating behavior expression into UML.
Refinement of objects and operations in Object-Z
by John Derrick, Eerke Boiten
Abstract:
In this paper we describe how we can refine both objects and operations in an
Object-Z specification. In particular, we will be concerned with changes of
granularity of both objects and operations. Objects in that we wish to
change the structure of objects in a specification. Operations in that we
wish to provide explicit support for action refinement in this language.
There are clear advantages in being able to change such levels of granularity
when performing a refinement. In this paper we discuss the issues surrounding
such refinements and derive general rules to support their use. We illustrate
our ideas by looking at a specification of a cash point machine at a bank.
Elements of an object-based model for distributed and mobile computation
by Jean-Bernard STEFANI, Florence GERMAIN, Elie NAJM
Abstract:
This paper introduces an abstract model for distributed and
mobile computation, based on a notion of domain. The model is shown
expressive enough to simulate faithfully several recent distributed
process calculi such a s the mobile ambient calculus and the DJoin
calculus. This in turn hints at the relevance of the model as a basis
for development of a primitive formal model for distributed and
mobile programming.
On a Temporal Logic for Object-Based Systems
by Dino Distefano, Joost-Pieter Katoen and Arend Rensink
Abstract:
This paper presents a logic, called BOTL (Object-Based Temporal
Logic), that facilitates the specification of dynamic and static properties
of object-based systems.
The logic is based on the branching temporal logic CTL and the Object
Constraint Language (OCL), an optional part of the UML standard for
expressing static properties over class diagrams.
The formal semantics of BOTL is defined in terms of a general operational
model that is aimed to be applicable to a wide range of object-oriented
languages.
A mapping of a large fragment of OCL onto BOTL is defined, thus
providing a formal semantics to OCL.
A Formal Specification of the CORBA Event Service
by Remi Bastide, Philippe Palanque, Ousmane Sy, David Navarre
Abstract:
CORBA is a standard proposed by the Object Management Group (OMG)
that promotes interoperability between distributed object systems.
Following the standardization of this object-oriented middleware,
the OMG has specified a set of Common Object Services (COS) that are
meant to serve as the building blocks of distributed CORBA applications.
The COS are specified using CORBA Interface Definition Language (IDL)
that describes the syntactic aspects of services supported by
remote objects.
However, CORBA-IDL does not support specification of the behaviour
of objects in an abstract and formal way, and behavioural specification
is mostly provided in plain English.
To overcome this problem, we have proposed a formal description
technique (Cooperative Objects) based on high-level Petri nets,
and developed a software support environment.
The goal of this paper is to demonstrate that our approach is suited
to the formal specification of typical CORBA COS,
and presents a Cooperative Object model of the CORBA event service,
a COS that provides asynchronous, one-to-many communication
between objects.
The advantages of dealing with a tool-supported,
executable formal notation are detailed,
as well as the results that can be obtained through
Petri net analysis techniques.
Using Relational and Behavioural Semantics in the Verification of Object Models
by Christie Bolton, Jim Davies
Abstract:
This paper shows how a combination of relational and
behavioural semantics might be used in the creation and verification
of object models. Specifications written in UML may be expressed in
terms of abstract data types and processes; different notions of
refinement may then be used to establish consistency between diagrams,
or to verify that a design is faithful to the specification.
Atomic Failure in Wide-Area Computation
by Dominic Duggan
Abstract:
The ATF Calculus is a kernel language for wide-area network
programming languages, with atomic failure semantics as its central
organizing principle.
Stochastically Enhanced Timed Automata
by Lynne Blair, Trevor Jones, Gordon Blair
Abstract:
There is currently considerable interest in the formal
specification
of distributed multimedia systems, with the majority of research in
this area considering the use of timed formal languages for the
specification of such systems. In contrast, however, there has been
less research on the specification of stochastic behaviour, and yet
this style of behaviour is predominant in this class of system. We
therefore present stochastically enhanced timed automata, as a
solution to the problem. The paper also describes an associated tool
suite that supports the editing, composition and simulation of such
automata. Crucially, the technique (and indeed the associated tool
suite) supports a more general aspect-oriented and multi-paradigm
specification architecture, with the stochastically enhanced timed
automata providing a common underlying model. Finally, a multimedia
example is presented, illustrating the use of the enhanced automata
and the associated tool suite.
Specification of Mobile Code Systems using Graph Grammars
by Fernando Luís Dotti, Leila Ribeiro
Abstract:
In this paper we introduce a formal approach for the specification of
mobile code systems. This approach is based on graph grammars, that is
a formal description technique that is suitable for the description of
highly parallel systems, and is intuitive even for non-theoreticians.
We discuss aspects of semantics of mobile components in view of the
dynamic changes that may occur within the open environment while the
component is executing.
Components as Processes: An Exercise in Coalgebraic Modeling
by L. S. Barbosa
Abstract:
Software components are persistent data abstractions, with a public
interface and a private encapsulated state, which arise
typically, not only
in systems' analysis,
but also at latter development
stages, namely in object and component-oriented programming.
This paper is an exercise in modeling
such components as
coalgebras for some kinds of endofunctors on Set,
capturing both interface types and behavioural patterns.
The construction of component categories, cofibred over
the interface space, emerges by generalizing
the usual notion of a coalgebra morphism. A collection of
composition operators as well as a tailored notion of bisimilarity,
are discussed.
FORMALLY MODELING UML AND ITS EVOLUTION: A HOLISTIC APPROACH
by Ambrosio Toval Alvarez, Jose Luis Fernandez Aleman
Abstract:
Due to the pervasiveness of diagrams in human communication and
by the increasing availability of graphical notations in Software
Engineering, the study of diagrammatic notations is in the foresight of
many research efforts. The expressive power of this kind of languages and
notations can be remarkably improved by adding extensibility mechanisms.
Extensibility, the ability of a notation or modeling language to be
extended from their own modeling constructs, is a feature that has assumed
considerable importance with the appearance of the UML (Unified Modeling
Language). Moreover, inasmuch as the UML is expected to go on substantial
changes in its semantics in the forthcoming years (three versions have
emerged in the last four years). Extensibility may play a pivotal role in
this endeavor.
In this paper, a holistic proposal to formally support the evolution of the
UML graphical notation metamodel is presented. To attain this aim, an
algebraic formalization is proposed which leads to a seamless formal model
of the UML four-layer semantics architecture. These two characteristics -
being holistic and seamless together with reflection are the most
innovative aspects of the research with respect to formalizing the UML. In
particular, a central role is played by reflection. A formal language
supporting this feature called Maude is studied and put forward as the
basis for the formalization of the UML extensibility mechanisms. According
to the approach of formalizing followed in this research, and since Maude
is an executable specification language, the final set of formal models
can also be used as a UML virtual machine, at the specification level. To
illustrate the approach, a UML Class Diagram prototype is implemented using
the Maude interpreter. An integration of such Maude prototype with a UML
commercial CASE has been developed, in Java, and is currently running.
Keywords: Extension Mechanism, Algebraic Specification, Maude, UML
Evolution, Metaprogramming.