Formal Methods for Open Object-Based Distributed Systems

Piccola is a “small composition language” currently being developed within the Software Composition Group. The goal of Piccola is to support the flexible composition of applications from software components.

We introduce an object-oriented language following a “process algebra” style. The idea is to define a formalism that enjoys a clean formal definition allowing the reuse of the rich algebraic theory typical of the process algebras in a context where an high level object oriented programming style is preserved. We provide an operational semantics based on a labelled transition system which allows to discuss, e.g., how different notions of equivalence, such as standard and asynchronous bisimulation, can be adapted to reason about our language. Finally, we illustrate the framework showing that an explicit receive primitive expressing a synchronization constraint or an update operation on the state of an object can be implemented in the language preserving a notion of observation equivalence among objects.

The OO-action systems formalism is a recent extension of action systems towards object-orientation. An OO-action system models an object-oriented system with active objects. In this paper we make the notion of a distributed object clear within this framework. Moreover, we show how object-based distributed systems are designed stepwise within a formal framework, the refinement calculus.

The goal of this paper is to develop a compositional proof system for reasoning about systems consisting of a dynamically evolving collection of objects, which are all executing in parallel, and which know each other by maintaining and passing around references.The proof system formalizes reasoning about these dynamic structures on an abstraction level that is at least as high as that of the programming language. The only operations on ‘pointers’ (references to objects) are testing for equality and dereferencing. Moreover, in a given state of the system, it is only possible to mention the objects that exist, or are known to exist, in that state. Objects that have not (yet) been created do not play a role.Compositionality is achieved by recording for each object both the history of its communications and the history of its creations.

A model, arising as a combination of the name managing techniques of the π-calculus with the natural representation of concurrency and locality of Petri nets, is presented.We exploit the suitability of our model to represent concurrent systems with an evolving structure by means of the Hurried Russian Philosophers case study, an extension of the Dining Philosophers with dynamic reconfiguration features and multiple levels of activity.

In the object-oriented languages, inheritance is a fundamental relation among classes, that originally indicated the is-a relation; however it has been often used for code-reuse. The integration between object-orientation and concurrency gives the possibility of using theoretical tools, such as the notions of action and state observation equivalences and preorders, developed within concurrency theories (Petri nets, CCS). In this paper we propose a semantic characterisation of two forms of inheritance in concurrent context: in particular, we propose a preorder based on action observation to give the semantics of inheritance used as is-a relation (type inheritance), and a preorder based on state observation for the semantics of inheritance as code-reuse (implementation inheritance).

We study different techniques by which formal methods can be applied within real software development environments for Java. We use the Metamata Toolsuite (our software development environment for Java) to experiment with these techniques. The goal is to improve the value of these environments from the point of view of a customer. Essentially, this means that the formal methods considered must be made extremely practical, while providing significant value for the average Java developer. We describe various kinds of formal methods we have defined and experimented with so far. One of our goals is to create an interest in formal methods enthusiasts to develop more such practical formal methods that can be made available to Java developers not conversant with this field.

This paper introduces a technique for the design and the implementation of coordination protocols in distributed cooperative applications using distributed objects and CORBA. An application architecture is designed as a group of cooperating “sites” having symmetrical configurations represented using “The Coordination Graph”, a graph structure whose nodes may be associated with abstract software components acting according to user-defined behaviors. The graph structure may be transformed following a set of rewrite rules. Application of a rule leads to the deletion and creation (at each site) of cooperating objects associated respectively with the nodes being removed from or inserted into the graph. These main coordination actions allow the configuration of applications to be automatically managed by the coordination service. The transformation rules are also used to control the cooperative activity supported by the application, i.e. for example, managing user access to the shared cooperation information. Hence the proposed technique allows both architectural and behavioral coordination issues to be handled for distributed applications.

Large software systems offer to software designers complex problems to solve. To manage such complexity several techniques have been developed to make this task easier and to allow the designer to reuse prior experience. However such techniques and frameworks often lack formal notations to support formal reasoning about the resulting products. We propose a interface specification language for Java modules and a methodology to support the design of Java components. We show how such a notation helps in designing software systems built of Java components, like JavaBeans.

In [10], we have presented an object-oriented method, called eXtended Object Modelling Technique, XOMT for shorthand. In this paper, we modify the developmental approach used in XOMT to include the specification of the behavior of composite objects based on synchronous interactions. The new developmental process consists of describing the application structure in terms of objects and associations between these objects. Object associations are then further refined by describing the object interactions that occur in the context of these associations. Object and association behaviors are specified in CSL, a specification language based on rendezvous interaction. CSL specifications can be translated in TLA. This adds a reasoning capability to the development process. The translation into TLA is motivated by the existence of a variety of specification and verification tools for TLA.

The design of components for open and distributed systems is challenging the software community with its specific problems. One of the current approaches is based on a reflective model that uses standard, independent, composible meta-components (controllers) to coordinate components and modify their behavior according to the user. requirements. However, this approach still has some pending issues, like the definition of design methodologies that lead to reusable and composible components and controllers, and the use of formal tools to reason about the correctness of the composed applications. This paper presents a formal framework in Object-Z for specifying reusable controllers, based on a component model for this kind of systems. The basic mechanisms of the model are formalized, together with the concepts and methods that allow developers of the controllers to prove their correctness, specify their behavior, and characterize the effect of adding them to components.

A (behavioural) algebraic formalization of composition and interaction for open distributed systems is proposed. Components (behavioural specifications) can be composed in a way that local behaviours and independence are preserved. This construction, called Independent Composition, verifies universal properties that favour distributivity of proofs. Interaction is modeled by Interactive Composition, a construction that adds new operations to the independent composition that affect both the components, so to allow them to communicate. As for many-sorted algebras, specifications can be put together via colimits, and the corresponding categories of models via limits.

In this short paper we sketch an enhancement of our co-notation, a specification language for the behavioural description of a wide class of information processing systems which supports a constraint-oriented specification style. The enhancement substantially improves previous versions of the notation by allowing for the dynamic creation and elimination of constraints. The formal, operational semantics of the (extended) co-notation has been re-designed in a form which should favour both the exploration of further variants of the notation and its object-oriented implementation.

Telecommunication networks are complex, distributed, and long-lived. In addition to the common problems of all software with these characteristics, telecommunication software has some severe problems that are particular to this application domain at this time.

Recently, SDL patterns have been introduced as a new concept to increase reusability in system design that is based on the formal description technique SDL. An integral part of this approach is the notion of pattern application, comprising the selection, adaptation, and composition of SDL patterns with a (possibly empty) specification context. We argue that the application of SDL patterns is a general form of specialization, supporting the reusability of design decisions, and compare it to the well-known reuse mechanism of inheritance in SDL.

If formal techniques are to be more widely accepted then they should evolve as current software engineering approaches evolve. Current techniques in the development of distributed systems use interface definition languages (IDLs) as a basis for the underlying communication and also as an abstraction tool. Object-oriented technologies [6] and the idea of engineering software through frameworks [5] are also widely accepted approaches in developing software. In this paper we show how the formal specification language SDL and associated tool support have been applied in the TOSCA1 project to engineer telecommunication services using these current techniques.

We show how SDL can be applied during object-oriented analysis to produce a formal object-oriented requirements specification. Building a formal specification from informal requirements is difficult. To simplify this, we first build a formal user-centred model that specifies behaviour from the viewpoint of the environment. It is used to construct the formal object-oriented requirements specification, i.e. a system-centred model. Both models are represented in SDL. The user-centred model is validated with respect to the requirements. Validation of the system-centred model can then be achieved by verifying that it provides the behaviour expected by the user-centred model.

Two of the dominant paradigms for formally describing and analysing OO distributed systems are state based specification, e.g. Object-Z, and behavioural specification, e.g. process algebra. The style of specification embodied by the two paradigms is highly contrasting. With state based techniques the data state is explicitly defined while the temporal ordering of operations is left implicit, in contrast in behavioural techniques, no explicit data state definition is given while the temporal ordering of action offers is focused on. However, in order to support sophisticated software engineering principles, e.g. multi-paradigm specification, viewpoints modelling and subtyping, there is now considerable interest in developing strategies for relating state based and behavioural specification paradigms.This paper serves two purposes — firstly, it reviews the existing body of work on relating these two specification paradigms and secondly, it presents some new results on the topic. In particular, we present a testing characterisation of downward simulation, which is the standard state based refinement relation and is also closely related to subtyping. Central to this characterisation is giving a behavioural interpretation to the meaning of state based operations outside their pre-conditions.

Conventionally, interfaces of objects export a set of messages with their types; and suggest nothing about the order in which these services may be accessed. This leaves room for a large number of run-time errors or misbehaviours in type correct designs. To mend this, we introduce the notion of protocol, expressing offered and expected orderings of messages, along with a notion of protocol correctness. We do this by defining the Protocol Assuring Universal Language Paul, which describes protocol aspects of classes, and a semantics of in terms of CSP.

Recent advances in telecommunication and software technology have motivated the study of components with dynamically changing syntactic interfaces. Formal development methods are traditionally directed towards components with static interfaces. We investigate this short-coming of formal development methods and outline how it can be overcome.We start by presenting a semantic model for interactive components communicating asynchronously by message passing. On the top of this model we build a simple specification language directed towards components with static interfaces. Then we generalise this language to handle components with dynamic interfaces. We introduce operators for composition and hiding.

The growth of computer networks and the increasing transmission capacity enables a rising number of service offers in distributed systems. One of the CORBAservices is the trading service, which supports clients searching for suitable services.This paper presents the idea of a service metric which can be implemented in an evaluation component for a CORBA trader. A service distance function is used to select an optimal service offer from a trader’s database. It computes the distance between a service request and a service offer with regard to their service properties. The service with the minimal distance to the service request represents the best offer. Hence, existing methods for distance computation between vectors are used, and a set of rules for computing the distance between service properties is developed. The resulting evaluation procedure is implemented in a CORBA trader using the distributed platform Orbix. The implementation is compared with the classic evaluation mechanism of the trader. Furthermore, the various methods for distance computation are compared.

The Reference Model for Open Distributed Processing (RM-ODP) [5] describes an architecture for the design of distributed services where the basic idea is to split the design concerns into several viewpoints. This is in order to overcome the immense complexity of today’s distributed systems by structuring the design process.

While message sequence charts (MSCs) are widely used in industry to document the interworking of processes or objects, they are expressively quite weak, being based on the modest semantic notion of a partial ordering of events as defined, e.g., in the ITU standard. A highly expressive and rigorously defined MSC language is a must for serious, semantically meaningful tool support for use-cases and scenarios. It is also a prerequisite to addressing what we regard as one of the central problems in behavioral specification of systems: relating scenario-based inter-object specification to state-machine intra-object specification. This paper proposes an extension of MSCs, which we call live sequence charts (or LSCs),since our main extension deals with specifying “liveness”, i.e., things that must occur. In fact, LSCs allow the distinction between possible and necessary behavior both globally, on the level of an entire chart and locally, when specifying events, conditions and progress over time within a chart. This also makes it possible to specify forbidden scenarios, and strengthens structuring constructs like as subcharts, branching and iteration.

Specification diagrams are a novel form of graphical notation for specifying open distributed object systems. The design goal is to define notation for specifying message-passing behavior that is expressive, intuitively understandable, and that has formal semantic underpinnings The notation generalizes informal notations such as UML’s Sequence Diagrams and broadens their applicability to later in the design cycle. In this paper we show how it is possible to reason rigorously and modularly about specification diagrams. An Actor Theory Toolkit is used to great advantage for this purpose.

Statechart Diagrams are a notation for describing behaviours in the framework of UML, the Unified Modeling Language of object-oriented systems. UML is a semi-formal language, with a precisely defined syntax and static semantics but with an only informally specified dynamic semantics. UML Statechart Diagrams differ from classical statecharts, as defined by Harel, for which formalizations and results are available in the literature. This paper sets the basis for the development of a formal semantics for UML Statechart Diagrams based on Kripke structures. This forms the first step towards model checking of UML Statechart Diagrams. We follow the approach proposed by Mikk and others: we first map Statechart Diagrams to the intermediate format of extended hierarchical automata and then we define an operational semantics for these automata. We prove a number of properties of such semantics which reflect the design choices of UML Statechart Diagrams.

The last decades have seen the emergence of the “sea of objects” paradigm for structuring complex distributed systems on workstations and local area networks. In this approach, applications and system services are composed of and communicate among themselves through reliable and transparently accessible object interfaces, leading to the interaction of hundred or thousands of unstructured objects.

Concurrent object-oriented languages, such as POOL [1], ABCL [12], Obliq [3] or Java [7], usually structure the program into objects, model the parallelism with threads and the mutual exclusion with locks (or some variant of them). These attempts to integrate concurrency and object-oriented features are somehow naive and no rigorous motivation for the design choices is given. As a result, the semantics is often crisp and one stumbles into anomalies (cfr. inheritance anomaly [8]) or typing flaws [10].

In a previous work [12] we presented COB, an object calculus which features objects with dynamically changing service offers. We also defined a type system for interfaces and a typing discipline that guarantees that no object may experience an unexpected service request at run-time. In the present paper, we extend our type system such that it describes “infinite state” types. We define equivalence and subtyping relations over those types based on bisimulation and simulation relations. We also define an algorithm to decide the equivalence or the subtyping relation of two types.The type system is applied to OL, a new calculus that uses the interface “states” in the behavior of the objects. As in COB, in OL there is a distinction between private and public interfaces. A private interface can have at most one client at a time whereas a public interface can be known by more that one client. Private interfaces can thus propose a non-uniform service offer (the set available services may change during the computation). OL extends the results of COB to infinite types: in spite of non-uniform service offers, in a well-typed configuration, there may not occur any “service not understood” error at runtime.

The main purpose of this work is the static detection of orphan messages in actor based languages. An orphan is a message which may not be handled by its target in some execution paths. Two kinds of orphan messages may be encountered, i.e., safety and liveness ones. Safety orphans occur when all target behaviors on a given execution path do not know how to handle the message. Liveness orphans occur when one of the target behaviors in each execution path knows how to handle the message but the target is deadlocked and will never assume the corresponding behavior. This paper presents a safe static analysis which detects all safety orphan messages in actor-based programs. This result extends previous work derived from sequential object-oriented languages type systems to non-uniform behaviors.

We present Multi-Object Dynamic Logic (MODL), a generalization of Dynamic Logic of which the intended use is the declarative specification of systems that are conceptually described by a multitude of objects. In an example specification of the controls of a railroad crossing we demonstrate how MODL can be used to give semantics and reasoning capacity to graphical languages for communicating multi-object systems. Finally we study to what extend temporal and mixed dynamic/temporal properties can be expressed in MODL.

There are recently growing interests in distributed/mobile applications. Specification of such applications requires consideration of some specific features that were not present in single processor applications: migration of data and computation, location-dependence, etc. Objects are attractive devices for describing such applications because an object gives a natural unit of migration and the location dependence can be expressed by binding the same name to different objects on different locations.One way for modeling such distributed objects would be to take what we call the process calculi approach [1, 3, 9], in which the syntax for expressing migration and location dependence is introduced and then its precise operational semantics is defined using transition systems. This approach can specify the precise behavior of distributed objects to the extent that their implementation on actual machines is fairly clear. On the other hand, such approach is often likely to overspecify the desired behavior of objects. For example, suppose we want to express computation that invokes methods of two remote objects and gathers the result. From an operational viewpoint, we can specify such computation either as a migrating object that moves to the location of each object and invokes the methods locally, and comes back to the original location, or as an object that stays at current location and remotely invokes methods of the objects. However, if we are only interested in the result of computation, both objects can be considered to reveal the same behavior. Although process calculi usually emphasize some process equivalence theories, it is often cumbersome to actually check the equivalence of two processes.In this work, we would rather take a different approach: we use linear logic for expressing distributed objects. Linear logic [4] has been successfully used for specifying concurrent processes/objects [2, 8, 6]. Following such success, we use here some extensions of linear logic [7, 5] and show how the behavior of many kinds of distributed objects can be specified. As was already observed in [7], we can elegantly express object migration and location dependence by using modal operators. One advantage of our approach is that it can give a more abstract specification of distributed object behavior than an operational approach: indeed, the two objects in the above example can be expressed as logically equivalent formulas of a modal linear logic, hence they are not distinguished. Of course, this fact can also be considered a disadvantage: we cannot specify the exact operational behavior of distributed objects. As discussed in [7], when we express objects as formulas of the modal linear logic, the logical equivalence implies only may equivalence of object behaviors. We can, however, remedy this problem by further extending the underlying linear logic with temporal operators such as those introduced in [5]. Thus, by choosing a certain kind of linear logic, we can specify the behavior of distributed objects with an appropriate degree of preciseness.

This paper addresses the issue of composition in a multi-paradigm environment. Our work focuses on the application domain of distributed multimedia systems and, in addition to considering quality of service properties, we also explore dynamic quality of service management functions based on the concepts of monitors and controllers. We advocate the use of a multi-paradigm specification technique which, to suit our chosen application domain, consists of LOTOS, real-time temporal logic and timed automata specifications. We illustrate our approach by giving an example of a simple phone system, extended with dynamic QoS management capabilities.

This paper presents TLO, an approach to the formal development of object-based systems in a temporal logic framework. The behavior of an object-based system is viewed as derivable from the behaviors of its constituent component objects. Temporal logic is a formalism well suited for specifying behavior of concurrent systems; it also provides conceptually simple notions of composition and refinement: Composition of objects is expressed as conjunction of the associated component specifications. The refinement relation between a low-level and a high-level specification requires that the former specification implies the latter.Specifically in an object-based approach, systems and their components need to be viewed as open systems: Each object guarantees some service (behavior), provided its environment conforms to certain assumptions. Hence, such components are most appropriately specified in an assumption/guarantee style.TLO adopts TLA as the underlying logical formalism. It encompasses a specification language for object-based designs and a corresponding method for specification and verification. The concepts are illustrated by an example involving both functional and fault-tolerance requirements.