Search

Abstract: We present a formal model to represent orchestrations and choreographies and we define several conformance semantic relations allowing to detect whether a set of orchestration models, representing some web services, leads to the overall communications described in a choreography. Given this formal model, we develop automatic methods to derive a set of web services from a given choreography, in such a way that the system consisting of these services necessarily conforms to the choreography. These methods enable the construction of conforming systems of services even in cases where projecting the choreography into each service would lead to a non-conforming system. This issue is addressed by adding some control messages that make services interact as required by the choreography. Two different derivation methods are presented. In the centralized method, a new service is responsible of managing these additional control messages. In the decentralized method, the responsibility of handling these messages is distributed among all services. [Copyright &y& Elsevier]

Abstract: Jackal is a fine-grained distributed shared memory implementation of the Java programming language. It aims to implement Java’s memory model and allows multithreaded Java programs to run unmodified on a distributed memory system. It employs a multiple-writer cache coherence protocol. In this paper, we report on our analysis of this protocol. We present its formal specification in μCRL, and discuss the abstractions that were made to avoid state explosion. Requirements were formulated and model checked with respect to several configurations. Our analysis revealed two errors in the implementation. [Copyright &y& Elsevier]

Abstract: One of the goals of software engineering is to provide what is necessary to write relevant, legible, useful descriptions of the systems to be developed, which will be the basis of successful developments. This goal was addressed both from informal approaches (providing in particular visual notations) and formal ones (providing a formal sound semantic basis). Informal approaches are often driven by a software development method, and, while formal approaches sometimes provide a user method, it is usually aimed at helping to use the proposed formalism when writing a specification. Our goal here is to provide a companion method that helps the user to understand the system to be developed, and to write the corresponding formal specifications. We also aim at supporting visual presentations of formal specifications, so as to “make the best of both formal and informal worlds”. We developed this method for the (logical-algebraic) specification languages CASL (Common Algebraic Specification Language, developed within the joint initiative CoFI) and for an extension for dynamic systems Casl-Ltl, and we believe it is general enough to be adapted to other paradigms. Another challenge is that a method that is too general does not encompass the different kinds of systems to be studied, while too many different specialized methods result in partial views that may be difficult to integrate in a single global one. We deal with this issue by providing a limited number of instances of our method, fitted for three different kinds of software items, while keeping a common “meta”-structure and way of thinking. More precisely, we consider here that a software item may be a simple dynamic system, a structured dynamic system, or a data structure, and we show here how to support property-oriented (axiomatic) specifications. We are thus providing support for the “building-bricks” tasks of specifying software artifacts that in our experience are needed for the development process. Our approach is illustrated with a lift case study. [Copyright &y& Elsevier]

In an environment of continuous and rapid evolution, software design methodologies must incorporate techniques and tools that support changes in software artifacts. In the FERUS project, we are developing a tool targeted at software designers that integrates a collection of operations on algebraic specifications written in the CASL language. The scope of FERUS includes not only modification of existing specifications, but also creation or derivation of new specifications, as well as their proof and execution, which are realized through inter-operability with existing tools. As FERUS involves the manipulation of software specification and inter-operability with other tools, the question of choosing appropriate representation formats is important. In this paper, we discuss the advantages and limitations of ATerms as a manipulation and exchange format in the setting of FERUS. We also present a new, graph-like format, which offers complementary features to a term-based format. Moreover, we present visualization utilities for these formats. [Copyright &y& Elsevier]

Statechart diagrams provide a graphical notation to model dynamic aspects of system behaviour within the unified modelling language (UML). In this paper, we present a formal operational semantics for a behavioural subset of UML statechart diagrams (UMLSDs) including a formal proof of their correctness with respect to major UML semantics requirements concerning behavioural issues. We show how the modularity of our semantics definition can be exploited to define extensions, in particular we show an extension to models composed of collections of communicating statechart diagrams, which we call multicharts. Finally we present all the conceptual issues related to building a tool for action based branching time model-checking, for the automatic verification of formal correctness of UML multicharts. The approach we propose preserves all the information necessary to report the results of model-checking in terms of the original UMLSD specification. The reference verification environment used for this model-checking approach is JACK, where automata are represented in a standard format which facilitates the use of a collection of tools for automatic verification. [Copyright &y& Elsevier]