A Composable Reflective Communication Framework
by Sebastian Gutierrez-Nolasco, Nalini Venkatasubramanian (University of California, Irvine)
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)
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)
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)
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)
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.