A Composable Reflective Communication Framework
by Sebastian Gutierrez-Nolasco, Nalini Venkatasubramanian
(University of California, Irvine)
Abstract:
The work described here proposes a feflective communication architecture
capable of expressing and representing diverse communication models in a
transparent way, while ensuring system consistency and correctness that
integrates with QoS-enabled customizable middleware frameworks such as
ComPOSE|Q currently being developed at the University of California, Irvine
Efficient Methods for Verification of Distributed Systems by Petri Nets
by Andrei Kovalyov (University of Manitoba)
Abstract:
We study the verification of distributed system correctness, i.e. one of its
quality which may be established formally, without knowing the specific
purpose of the system, and just on the basis of general requirements to the
system of the class. Several approaches are proposed: Reduction, Graph
Theory and Linear Algebra. We applied our methods for the verification of
Logical Control Algorithms and Workflow Procedures.
PetShop : a tool for the formal specification of CORBA systems.
by Remi Bastide (LIHS Universite Toulouse 1)
Abstract:
This demonstration complements a paper presentation (A Formal Specification
of the CORBA Event Service, by Bastide et al.).
The Object Management Group (OMG) has defined a standard for distributed objects communication called Common Object Request Broker Architecture (CORBA). However, CORBA fails in two respects: on the one hand, its specification language, CORBA-IDL does not provide for the behavioural specification of systems, and on the other hand the development of CORBA systems is cumbersome.
To support the development of CORBA-based distributed systems, we have developed a CASE tool called PetShop that uses an object-oriented Petri net formalism, namely Cooperative Objects (CO) to address the problem of behavioural specification. The tool addresses five main objectives:
BOBJ Behavioral Specification and Reasoning System
by Joseph Goguen, Kai Lin and Grigore Rosu
(University of California, San Diego)
Abstract:
BOBJ is a new system for behavioral specification and reasoning based on
hidden order sorted algebra. It implements behavioral rewriting, which takes
account of the weaker rules for inference of hidden equational logic, as well
as circular coinductive rewriting, which combines behavioral rewriting with
circular coinduction, giving a surprisingly powerful proof method for
behavioral properties. BOBJ also has an algorithm that finds cobases for
coinduction proofs, and support for the concurrent connection of behavioral
specifications.
Concurrent Object-Oriented Specification and Analysis in Maude
by Mark-Oliver Stehr (SRI International)
Abstract:
Maude is a high-performance reflective language and system supporting both
equational and rewriting logic specification and programming for a wide
range of applications. Rewriting logic is a logic of concurrent change that
can naturally deal with state and with concurrent computations. It has good
properties as a general semantic framework for giving executable semantics
to a wide range of languages and models of concurrency. In particular, it
supports very well concurrent object-oriented computation.
Maude supports in a systematic and efficient way logical reflection. Some of the most interesting applications of Maude are reflective applications, in which Maude is used to formally analyze specifications of concurrent systems and to create executable environments for different logics, theorem provers, languages, and models of computation.
The demo will introduce the basic concepts of distributed object system specification in Maude through a series of examples, and will also illustrate several uses of Maude in the execution and formal analysis of distributed object systems.