Publications of Gianna Reggio

From Conditional Specifications to Interaction Charts: A Journey from Formal to Visual Means to Model Behaviour

In this paper, addressing the classical problem of modelling the behaviour of a system, we present a paradigmatic journey from purely formal and textual techniques to derived visual notations, with a further attention first to code generation and finally to the incorporation into a standard notation such as the UML.
We show how starting from Casl positive conditional specifications with initial semantics of labelled transition systems, we can devise a new visual paradigm, the interaction charts, which are diagrams able to express both reactive and proactive\autonomous behaviour.
Then, we introduce the executable interaction charts, which are interaction charts with a special semantics, by which we try to ease the passage to code generation.
Finally, we present the interaction machines, which are essentially executable interaction charts in a notation that can be easily incorporated, as an extension, into the UML.

A preliminary pdf version of this paper is available at ReggioEtAll03a.pdf.

A Formally Grounded Software Specification Method

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.

A preliminary pdf version of this paper is available at ChoppyReggio05b.pdf.

A UML-Based Approach for Problem Frame Oriented Software Development

We propose a software development approach that combines the use of the structuring concepts provided by problem frames, the use of the UML notation, together with our methodological approach for well-founded methods. Problem frames are used to provide a first idea of the main elements of the problem under study. Then we provide ad hoc UML based development methods for some of the most relevant problem frames together with precise guidelines for the users. The general idea of our method is that, for each frame, several artifacts have to be produced, each one corresponding to a part of the frame. The description level may range from informal and sketchy, to formal and precise, while this approach is drawn from experience in formal specifications.
Thus we show how problem frames may be used upstream of a development method to yield an improved and more efficient method equipped with the problem frames structuring concepts.

A preliminary pdf version of this paper is available at ChoppyReggio05a.pdf.

A UML-Based Method for the Commanded Behaviour Frame

Using UML for Problem Frame Oriented Software Development

We propose a software development approach that combines the use of the UML notation, the use of the structuring concepts provided by the problem frames, together with our methodological approach for well-founded methods.
The problem frames are used to provide a first idea of the main elements of the problem under study. Then we provide ad hoc UML based development methods for some of the most relevant problem frames together with precise guidelines for the users. The general idea of our method is that, for each frame, several artifacts have to be produced, each one corresponding to a part of the frame.
The description level may range from informal and sketchy, to formal and precise, while this approach is drawn from experience in formal specifications.

The postscript version of an extended version of this paper is available at UFRAMESlong.ps.

Scientific Engineering of Distributed Java Applications: Third International Workshop, FIDJI 2003 Luxembourg-Kirchberg, Luxembourg, November 27-28, 2003 Revised Papers.

Tight Structuring for Precise UML-based Requirement Specifications

On the basis of some experience in the use of UML-based use case-driven methods, we believe and claim, contrary to a recent wave for allowing almost total freedom as opposed to disciplined methods, that a tighter and more precise structuring of the artifacts for the different phases of the software development process may help speed-up the process, while obviously making easier the consistency checks among the various artifacts. To support our claim we have started to investigate an approach, that, though being compliant with the \UML notation and a number of UML-based methods, departs from them both in the basic philosophy, that follows the "tight and precise" imperative, and in the technical solutions for structuring the various artifacts.
Building on some previous work concerning the structure of the requirement specification artifacts, here we complete upwards and improve our proposal, investigating the link between the analysis of the problem domain and the requirement capture and specification. Indeed, one of our assumptions, as advocated by some methodologists and backed by our own experience, is the neat separation between the problem domain and the system. To that purpose we propose a rather new way of structuring the problem domain model and then the link with the system, that encompasses the most popular current approaches to domain modelling. Then we exploit both the domain model and our requirement specification frame for capturing and specifying the requirements. From our construction we can derive rigorous guidelines, only hinted to here, for the specification tasks, in a workflow that allows and suggests iteration and incrementality, but in a way that is not just based on the single use cases and takes more care of the overall construction. The various concepts and constructions are illustrated with the help of a small running case study.

The postscript and pdf versions of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/AstesianoReggio03f.ps. and /person/ReggioG/AstesianoReggio03f.pdf.

Architecture Specific Models: Software Design on Abstract Platforms

We address in general the problem of providing a methodological and notational support for the development at the design level of applications based on the use of a middleware.
In order to keep the engineering support at the appropriate level of abstraction, we formulate our proposal within the frame of Model Driven Architecture (MDA).
We advocate the introduction of an intermediate abstraction level (between PIM and the PSM), called ASM for Architecture Specific Model, which is particularly suited to abstract away the basic common architectural features of different platforms.
In particular, we consider the middlewares supporting a peer-to-peer architecture, because of the growing interest in mobile applications with nomadic users and the presence of many proposals of peer-to-peer middlewares.

The postscript and pdf versions of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/ReggioEtAll03a.ps. and /person/ReggioG/ReggioEtAll03a.pdf.

Improving Use Case Based Requirements Using Formally Grounded Specifications

Our approach aims at helping to produce adequate requirements, both clear and precise enough so as to provide a sound basis to the overall development.
We present a technique for improving use case based requirements, by producing a companion Formally Grounded specification, that results both in an improved requirements capture, and in a requirement validation. The Formally Grounded requirements specification is written in a "visual" notation, using both diagrams and text, with a formal counterpart (written in the Casl-Ltl language). The resulting use case based requirements are of high quality, more systematic, more precise, and its corresponding Formally Grounded specification is available. We illustrate our approach on an Auction System case study.

The postscript and pdf versions of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/ChoppyReggio04a.ps. and /person/ReggioG/ChoppyReggio04a.pdf.

Towards a Well-Founded UML-based Development Method

This paper presents an attempt, perhaps unorthodox, at bridging the gap between the use of formal techniques and the current software engineering practices. After years of full immersion in the development and use of formal techniques, we have been led to suggest a Virtuous Cycle philosophy, better marrying the rigour of formalities to the needs and, why not, the wisdom of current practices. What we have called Well-Founded Software Development Methods is a strategy compliant with that philosophy, that essentially aims at proposing methods where the formalities provide the foundational rigour, and perhaps may inspire new techniques, but are kept hidden from the user.
In a stream of papers we have outlined an approach - a possible instantiation of a particular well-founded method - which is Model-Driven and adopts a UML notation. Here, after introducing our basic philosophy and the Well-Founded methods strategy, we outline in summary our sample approach and, as a new contribution, we show in some detail how to handle the Model-Driven Design (or Platform Independent Design) phase.

The postscript and pdf versions of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/AstesianoReggio03g.ps. and /person/ReggioG/AstesianoReggio03g.pdf.

From Formal Techniques to Well-Founded Software Development Methods

We look at the main issue of the Colloquium "Formal Methods at the Crossroads from Panacea to Foundational Support" reflecting on our rather long experience of active engagement in the development and use of formal techniques.
In the years, we have become convinced of the necessity of an approach more concerned with the real needs of the software development practice. Consequently, we have shifted our work to include methodological aspects, learning a lot from the software engineering practices and principles.
After motivating our current position, mainly reflecting on our own experience, we suggest a Virtuous Cycle for the formal techniques having the chance of a real impact on the software development practices. Then, to provide some concrete illustration of the suggested principles, we propose and advocate a strategy that we call Well-Founded Software Development Methods, of which we outline two instantiations.

The postscript and pdf versions of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/AstesianoEtAll03a.ps. and /person/ReggioG/AstesianoEtAll03a.pdf.

From Requirement Specification to Prototype Execution: a Combination of a Multiview Use-Case Driven Method and Agent-Oriented Techniques

In this paper we discuss how to combine a multiview use-case driven method for the requirement specification of a system with an agent-oriented method for developing a working prototype. The rationale behind this combination is to cover the complete software development cycle, while the two methods it originates from only cover a part of it. The prototype execution allows to obtain useful feedbacks on the coherence of the UML artifacts produced during the requirement specification phase.

The pdf version of this paper are available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/AstesianoEtAll03b.pdf.

Consistency Issues in Multiview Modelling Techniques

In this paper, after introducing the problem and a brief survey of the current approaches, we look at the consistency problems in the UML in terms of the well-known machinery of classical algebraic specifications. Thus, first we review how the various kinds of consistency problems were formulated in that setting. Then, and this is the first contribution of our note, we try to reduce, as much as possible, the \UML problems to that frame. That analysis, we believe, is rather clarifying in itself and allows us to better understand what is new and what instead could be treated in terms of that machinery. We conclude with some directions for handling those problems, basically with constrained modelling methods that reduce and help precisely individuate the sources of possible inconsistencies.

The pdf version of this paper are available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/AstesianoReggio03b.pdf.

Scientific Engineering for Distributed Java Applications

A Notation to Support Component-Based Design of Java Applications

In this paper we present JTN2 (Java Targeted Notation 2) a notation for component-based design of Java applications. JTN2 defines a component model based on the fundamental object-oriented principles: abstraction, encapsulation, modularization and typing. Indeed, JTN2 is an extension of JTN, an object-oriented, formal, visual notation for designing concurrent Java applications. JTN2 component model aims to deal with three issues of Java based component development: component definition, component interconnection and component implementation in Java.
JTN2 allows a component to be described, understood and analyzed independently from other components. Pre-designed components are interconnected to form complete systems. JTN2 provides a static type system that checks if two components can be interconnected. Java code can be, then, generated automatically by taking advantage of multiple Java technologies, e.g., JavaBeans, Enterprise JavaBeans and JINI.

The pdf version of this paper are available through anonymous ftp at ftp.disi.unige.it, in /person/AmzaC/fidji2002/fidji2002.pdf.

Metamodelling Behavioural Aspects: the Case of the UML State Machines

The "object-oriented meta-modeling" seems currently to be one of the most promising approach to the "precise" definition of UML. Essentially this means using a kernel object-oriented visula notation to define UML. This has proved itself to be an intuitive way of defining the abstract syntax of UML. For what concerns the "static part", the initial work of the pUML group seems to confirm that the approach is workable, whereas no convincing proposal have been presented to cover the dynamic aspects, as active classes, cooperation/communications among active objects, state charts, sequence diagrams, and so on.
We think that to conveniently and precisely define such aspects, we need an underlying formal model of the dynamic behaviour of the active objects, and we think, supported by our past experience, that labelled transition systems are a good one.
We thus propose how to use a kernel visual notation to define labelled transition systems in an object-oriented way. Furthermore, we present also a new kind of diagrams, quite similar to state charts, LTD (Labelled Transition Diagrams) to visually present such definitions. As an example, we work out the meta-model of the state machines starting from our formal definition of their semantics based on labelled transition systems.

The pdf version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/Reggio02c.pdf.

Knowledge Structuring and Representation in Requirement Specification

On the basis of some experience in the use of use case-driven and UML-based methods, we believe that a more refined and stringent structuring of the knowledge in the artifacts of a Requirement Specification may help speed-up the specification process and make easier the consistency checks among the various components.
Thus we propose a way of structuring and representing the Requirement Specification artifacts that presents a number of novelties w.r.t. the best-known current methods, though in the end it can be seen as a complement/refinement of some of them and thus inserted in a more general process model, such as, e.g., RUP.

Our proposal is multiview, use case-driven and UML-based; thus also object-oriented. However, also benefitting of some earlier work, notably in the Structured Analysis, method and various hints by M. Jackson, we take a rather abstract view, trying to avoid a preemptive decision on the classes structuring the software system to build; that is achieved not only making a sharp distinction between business/domain modelling and the system, but also dealing with the system at the requirement level as a black box, providing only the minimal structure needed to express the interactions with the context.
From our construction we can derive rigorous guidelines for the specification tasks; the approach allows iteration and incrementality, but in a way that is not just based on the single use cases and takes more care of the overall construction.

The pdf version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/AstesianoReggio02a.pdf.

Labelled Transition Logic: An Outline

In the last ten years we have developed and experimented in a series of projects, including industry test cases, a method for the specification of reactive/concurrent/parallel/distributed systems both at the requirement and at the design level. We present here in outline its main technical features, providing pointers to appropriate references for more detailed presentations of single aspects, applications and documentation.

The overall main feature of the method is its logical (algebraic) character, because it extends to labelled transition systems the logical/algebraic specification method of abstract data types; moreover systems are viewed as data within first-order structures called LT-structures. Some advantages of the approach are the full integration of the specification of static data and of dynamic systems, which includes by free higher-order concurrency, and the exploitation of well-explored classical techniques in many respects, including implementation and tools.

On the other hand the use of labelled transition systems for modelling systems, inspired by CCS, allows us to take advantage, with appropriate extensions, of some important concepts, like communication mechanisms and observational semantics, developed in the area of concurrency around CCS, CSP and related approaches.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/AstesianoReggio01b.ps

Towards a Rigorous Semantics of UML Supporting its Multiview Approach

We discuss the nature of the semantics of the UML. Contrary to the case of most languages, this task is far from trivial. Indeed, not only the UML notation is complex and its informal description is incomplete and ambiguous, but we also have the UML multiview aspect to take into account.
We propose a general schema of the semantics of the UML, where the different kinds of diagrams within a UML model are given individual semantics and then such semantics are composed to get the semantics on the overall model.
Moreover, we fill part of such a schema, by using the algebraic language CASL as a metalanguage to describe the semantics of class diagrams, state machines and the complete UML formal systems.

The pdf version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/CerioliM/FASE2001.pdf.

UML-SPACES: A UML Profile for Distributed Systems Coordinated Via Tuple Spaces

Coordination via tuple spaces is a well known and accepted technique for designing distributed systems; originally introduced in Linda, it has been very recently adopted within the Java environment as underlying mechanism of the JavaSpaces™ technology.
Here we explore the possibility of using UML in the development of systems using such technique. While tuple spaces are modelled quite naturally in UML as particular passive classes and objects, state machines do not seem adequate for modelling active objects interacting via tuple spaces. A solution is to use the UML lightweight extension mechanism to propose an appropriate extension of state machines by adding transition triggers corresponding to successful and failed execution of lookup operations on a tuple space.
The result is a UML profile, and thus a visual notation, for modelling autonomous distributed systems based on tuple spaces.

The pdf version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/AstesianoReggio00a.pdf.

Using CASL to Specify the Requirements and the Design: A Problem Specific Approach

In its book, "Software Requirements & Specifications: a Lexicon of Practice, Principles and Prejudices" (Addison-Wesley, 1995) M. Jackson introduces the concept of problem frame to describe specific classes of problems, to help in the specification and design of systems, and also to provide a framework for reusability. He thus identifies some particular frames, such as the translation frame (e.g., a compiler), the information system frame, the control frame (or reactive system frame), ... Each frame is described along three viewpoints that are application domains, requirements, and design.
Our aim is to use CASL (or possibly a sublanguage or an extension of CASL if and when appropriate) to formally specify the requirements and the design of particular classes of problems ("problem frames"). This goal is related to methodology issues for CASL, that are here addressed in a more specific way, having in mind some particular problem frame, i.e. a class of systems.
It is hoped that this will provide both a help in using, in a really effective way, CASL for system specifications, a link with approaches that are currently used in the industry, and a framework for the reusability of CASL specifications.
This approach is illustrated with some case studies, e.g., the information system frame is illustrated with the invoice system case study.

The postscript version of a complete version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/ChoppyReggio99a.ps

An Algebraic Semantics of UML Supporting its Multiview Approach

We aim at using algebraic techniques, and in particular an extension, Casl-Ltl of the Casl basic language in order to produce a formal semantics of the UML. Contrary to most cases, this task is far from trivial. Indeed, the UML notation is complex, including a lot of heterogeneous notations for different aspects of a system, possibly described in different phases of the development process. Moreover, its informal description is incomplete and ambiguous, not only because it uses the natural language, but also because the UML allows the so called semantics variation points, that are constructs having a list of possible semantics, instead of just one.

The postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/AstesianoEtAll00b.ps

Plugging Data Constructs into Paradigm-Specific Languages: towards an Application to UML (Invited Lecture)

We are interested in the composition of languages, in particular a data description language and a paradigm-specific language, from a pragmatic point of view.
Roughly speaking our goal is the description of languages in a component-based style, focussing on the data definition component. The proposed approach is to substitute the constructs dealing with data from the "data" language for the constructs describing data that are not specific to the particular paradigm of the "paradigm-specific" language in a way that syntax, semantics as well as methodologies of the two components are preserved.
We illustrate our proposal on a toy example: using the algebraic specification language CASL, as data language, and a "pre-post" condition logic à la Hoare, as the paradigm specific one.
A more interesting application of our technique is fully worked out in ReggioRepetto00b and the first step towards an application to UML, that is an analysis of UML from the data viewpoint, following the guidelines given here, is sketched at the end.

The postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/AstesianoEtAll00a.ps

CASL-CHART: a Combination of Statecharts and of the Algebraic Specification Language CASL

The postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/ReggioRepetto00b.ps

Analysing UML Active Classes and Associated State Machines -- A Lightweight Formal Approach

We consider the problem of precisely defining UML active classes with an associated state chart. We are convinced that the first step to make UML precise is to find an underlying formal model for the systems modelled by UML. We argue that labelled transition systems are a sensible choice; indeed they have worked quite successfully for languages as Ada and Java. Moreover, we think that this modelization will help to understand the UML constructs and to improve their use in practice. Here we present the labelled transition system associated with an active class using the algebraic specification language CASL.
The task of making precise this fragment of UML raises many questions about both the "precise" meaning of some constructs and the soundness of some allowed combination of constructs.

The postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/Reggio99a.ps

Formalism and Method -- Full version

Luckily, is getting strength the view that formal methods are useful tools within the context of an overall engineering process, heavily influenced by other factors that developers of formalisms should take into account.
We argue that the impact of formalisms would much benefit from adopting the habit of systematically and carefully relating formalisms to methods and to the engineering context, at various levels of granularity. Consequently we oppose the attitude of conflating formalism and method, with the inevitable consequence of emphasizing the formalism or even just neglecting the methodological aspects.
In order to make our reflections more concrete we illustrate our viewpoint addressing one particular activity in the software development process, namely the use of formal specification techniques.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/AstesianoReggio99a.ps.Z

Is it feasible to construct a semantics for all of UML?: Dynamic behaviour and concurrency

This paper reports the results of a workshop held at ECOOP'99.
The workshop was set up to find answers to questions fundamental to the definition of a semantics for the Unified Modelling Language. Questions examined the meaning of the term semantics in the context of UML; approaches to defining the semantics, including the feasibility of the metamodelling approach; whether a single semantics is desirable and, if not, how to set up a framework for defining multiple, interlinked semantics; and some of the outstanding problems for defining a semantics for all of UML.

The PDF version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/Vari99a.pdf

JTN: A Java-Targeted Graphic Formal Notation for Reactive and Concurrent Systems

JTN is a formal graphic notation for Java-targeted design specifications, that is specifications of systems that will be implemented using Java.
JTN is aimed to be a part of a more articulated project for the production of a development method for reactive/concurrent/distributed systems. The starting point of this project is an existing general method that however does not cover the coding phase of the development process. Such approach provides formal graphic specifications for the system design, but they are too abstract to be transformed into Java code in just one step, or at least, the transformation is really hard and complex.
We introduce an intermediate step that transforms the above abstract specifications into JTN specifications, for which the transformation into a Java program is almost trivial; thus such transformation can be automatized and guaranteed correct.

The postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/CosciaE/papers/JTN-Fase.ps

Stores as Homomorphisms and Their Transformations - A Uniform Approach to Structured Types in Imperative Languages

We address the problem of giving a clean and uniform mathematical model for handling user defined data types in imperative languages, contrary to the ad-hoc treatment usual in classical denotational semantics.
The problem is solved by defining the store as a homomorphic mapping of an algebraic structure of left values modelling containers into another one of right values modelling contents.
Consequently store transformations can be defined uniformly on the principle that they are minimal variations of the store embedding some basic intended effects and compatible with the homomorphic structure of the store.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/ZuccaE/SCP99.ps.gz

Algebraic Specification of Concurrent Systems

Most software systems are concerned with concurrent systems and thus it is of paramount importance to provide good formal support to the specification, design, and implementation of concurrent systems. Algebraic/logic methods have also found interesting applications in this field, especially to treat at the right level of abstraction the relevant features of a system, helping to hide the unnecessary details and thus to master system complexity.

Due to the particularly complex nature of concurrent systems, and contrary to the case of classical (static) data structures, there are different ways of exploiting algebraic methods in concurrency.

In the literature, we can distinguish at least four kinds of approaches.

The algebraic techniques are used at the metalevel, for instance, in the definition or in the use of specification languages. Then a specification involves defining one or more expressions of the language, representing one or more systems.

A particular specification language (technique) for concurrent systems is complemented with the possibility of abstractly specifying the (static) data handled by the systems considered using algebraic specifications.
We can qualify the approaches of this kind by the slogan "plus algebraic specifications of static data types".

These methods use particular algebraic specifications having "dynamic sorts", which are sorts whose elements are/correspond to concurrent systems. In such approaches there is only one "algebraic model" (for instance, a first-order structure or algebra) in which some elements represent concurrent systems.
We can qualify the approaches of this kind as "algebraic specifications of dynamic-data types", which are types of dynamic data.

These methods allow us to specify an (abstract) data type, which is dynamically changing with time. In such approaches we have different "algebraic" models corresponding to different states of the system.
We can qualify the approaches of this kind as "algebraic specifications of dynamic data-types"; here the data types are dynamic.

We have organized the paper around the classification above, providing significant illustrative examples for each of the classes. Our rationale has been mainly to present representatives. In particular, there is no intention of providing a comparative study of the methods. This is a goal outside the scope of the book.
We use a common example for the presentation of all approaches, a very simple concurrent system.

The postscript and pdf versions of this paper are available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/AstesianoEtAll99a.ps and /person/ReggioG/AstesianoEtAll99a.pdf.

A Discipline for Handling Feature Interaction

A challenging problem within the wider software evolution problem is the development of systems by features. While most of the recent work centered around the detection of feature interactions, we present an approach based on modular specification, separation of concerns and prevention of unwanted interactions. We illustrate our approach extending a formalism for the specification of reactive systems and showing its application to some aspects of the well-known case of telephone systems (POTS and variations).
The paper concentrates more on the methodological aspects, which are, at large extent, independent of the formalism. Indeed, this seems to be the case of some rather novel concepts like the distinction between pre-features (features in isolation) and features, closed and open semantics, feature composition and discipline of feature interaction, and finally the pervading role of a kind of anti-frame assumption.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/AstesianoReggio98c.ps.Z

A Method to Capture Formal Requirements: the INVOICE Case Study

In the last years myself in cooperation with other people have developed various specification formalisms for systems which can be named concurrent, parallel, reactive, ..., and applied to various case studies also in projects in cooperation with industry. While the people forwarding the case studies have found satisfactory the formal specifications produced with our cooperation, they were asking "how can we produce such specifications?" and "how can be such specifications integrated into a development process?" That has lead us to try to derive, out of a specification formalism for systems, a method for supporting the development process. Here we present the part concerning requirement specifications (thus requirements capture and specification) and a visual presentation of such specifications.
Our requirement specifications are formal, follow an axiomatic (or better property oriented) style, and use a variant of the CTL branching-time temporal logic, which can be termed first-order, many-sorted, with edge-formulae and equality.
Here the emphasis in on "HOW" to get the formal specifications, and on how to present them in a sensible way, rendering visually any part that it is possible. The proposed method provides precise instructions ({\em guidelines}) guiding the user to find, after some analysis of the system, in an exhaustive way (all\slash most of ?) the reasonable properties.
In this paper we consider only the part of our method concerning requirement specifications of simple (non-structured) systems, and the method is presented by using the two variants of the simple INVOICE case study, proposed in a workshop about comparing methods for formal requirements.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/Reggio98b.ps.Z

Very Abstract Specifications: A formalism Independent Approach

Given an already fully developed formal specification method for reactive systems, Two operations are presented for a modular approach to the definition of frameworks for rigorous development of software, formally represented as institutions. The first one generalize models, allowing them to have more structure than the minimal required by their declared signatures, as it happens for software modules, having local routines that do not appear in their interface. The second one extends sentences, and their interpretation in models, allowing sentences on richer signatures to be used as formulae for poorer ones. Combining the application of these operations, powerful institutions can be defined, like those for very abstract entities, or for hyper-loose algebraic specifications. The compatibility of different sequential applications of these operations and properties of the resulting institutions are studied as well.
This is an extended version of Institutions for Very Abstract Specifications.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/CerioliM/MSCS97.ps.gz

A Graphic Notation for Formal Specifications of Dynamic Systems

Given an already fully developed formal specification method for reactive systems, we also develop an alternative graphic notation for its specifications to improve writing and understanding of such specifications and, hopefully, the acceptance of the method by industrial users.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/ReggioLarosa97a.ps.Z

Formalism and Method

Luckily, is getting strength the view that formal methods are useful tools within the context of an overall engineering process, heavily influenced by other factors that developers of formalisms should take into account.
We argue that the impact of formalisms would much benefit from adopting the habit of systematically and carefully relating formalisms to methods and to the engineering context, at various levels of granularity. Consequently we oppose the attitude of conflating formalism and method, with the inevitable consequence of emphasizing the formalism or even just neglecting the methodological aspects.
In order to make our reflections more concrete we illustrate our viewpoint addressing one particular activity in the software development process, namely the use of formal specification techniques.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/AstesianoReggio97a.ps.Z

Specification of Abstract Dynamic DataTypes: A Temporal Logic Approach

A concrete dynamic-data type is just a partial algebra with predicates such that for some of the sorts there is a special predicate defining a transition relation.
An abstract dynamic-data type (ad-dt) is an isomorphism class of such algebras. To obtain specifications for ad-dt's, we propose a logic which combines many-sorted first-order logic with branching-time combinators.
We consider both an initial and a loose semantics for our specifications and give sufficient conditions for the existence of the initial models. Then we discuss structured specifications and implementation.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/CostaReggio97a.ps.Z.

A Dynamic Specification of the RPC-Memory Problem

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/AstesianoReggio96a.ps.Z

Deontic Concepts in the Algebraic Specification of Dynamic Systems: The Permission Case

Deontic logic is the logic dealing with real as well as with ideal behaviour. Concepts of obligation, permission and prohibition are useful in formal specification to give a picture of what a system ought or it is permitted to do or to be, without forcing its behaviour in any way.
In this paper, permission and prohibition concepts are introduced by means of particular predicates within a framework for the specification of Abstract Dynamic Data Types. This allows us to treat separately normal (permitted) and abnormal (non-permitted) activities, making more natural the specification of recovery policies after non ideal behaviours. Moreover, deontic qualifications on behaviour may be combined with branching-time combinators, to express properties on particular kinds of behaviours.

The postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/CosciaReggio96a.ps.Z

The SMoLCS Toolset

A short presentation of the SMoLCS toolset.

The postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/AstesianoEtAll95a.ps

Algebraic Oriented Institutions

In many recent applications of the algebraic paradigm to formal specification methodologies, basic frameworks are endowed with new features, tailored for special purposes, that mostly are "orthogonal" to the underlying algebraic framework, in the sense that they are instances of a parametric constructions. This lack of generality is conflicting with the ability of changing the basic formalism, and hence with the reuse of methodologies, seen as high-level theoretical tools for the software development.
In any real application two steps can be distinguished in the process of getting the most suitable algebraic formalism: the choice of the most appropriate basic algebraic formalism (i.e. sufficiently powerful for the problem, but non-overcomplex) and the addition of the features needed in the particular case (e.g. entities for structured parallelism or higher-order functions for functional programming). Thus here we propose a modular construction of algebraic frameworks, formalized by means of operations on institutions, used as a synonym for logical formalism, in order to build richer institutions by adding one feature at a time.
Many constructions used in the practice have meaning only for those institutions that represent "algebraic formalisms". In order to give sound foundations for the treatment of such operations, a preliminary step is the formal definition of which institutions correspond to algebraic frameworks. Here we propose a first attempt at the definition of algebraic-oriented institutions, that includes all interesting cases. Then, using this definition, we formally define some operations adding features to basic algebraic frameworks and show that the result of such operations applied to any algebraic-oriented institution is an algebraic-oriented institution, too; so that the result can be used as input for other operations, modularly building a formalism as rich as needed by the application.
Technically algebraic-oriented institutions are described by (standard) algebraic specifications, so that both theoretical and software tools are at hand to help in the building process; moreover algebraic specification users already have the know-how to understand and manipulate metaoperations building algebraic formalisms.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/CerioliM/AMAST93.ps.z

Institutions for Very Abstract Specifications

This paper is a first attempt at the definition of a set of operations on specification frameworks, supporting the modular construction of formal software specification methodologies.
Since obviously a formalism providing tools to deal with all possible software specification features, if any, would be a monster and would become out of date in a short time, in our opinion the first step, in order to produce formal specifications, is to get a framework including all the features needed by the particular problem under examination, but as simple as possible.
Following an obvious reuse principle, the best way to get such a framework is to assemble pieces of formalisms, studied once and forever, or to tune an available formalism, adding only the local features.
In this paper, following the well-established approach by Goguen and Burstall, specification frameworks are formalized as institutions; thus enrichments and assembling of formalisms become, in this setting, operations among institutions.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/CerioliM/WADT93.ps.gz

A SMoLCS Based Kit for Defining the Semantics of High-Level Algebraic Petri Nets

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/BettazReggio94a.ps.Z

Stores as Homomorphisms and their Transformations

In the classical denotational model of imperative languages handling structured types, like arrays, requires an ad-hoc treatment for each data type, including e.g. an ad-hoc allocation and deallocation mechanism. Our aim is to give a homogeneous approach that can be followed whichever is the data structure of the language.
We start from the traditional model for Pascal-like languages, which uses a notion of store as a mapping from left values (containers for values, usually called locations), into right values; we combine this idea with the well-known algebraic approach for modelling data types. More precisely, we consider an algebraic structure both for the right and the left values; consequently, the store becomes a homomorphic mapping of the left into the right structure.
Seeing a store as a homomorphism has a number of interesting consequences. First of all, the transformations over a store can be uniformly and rigorously defined on the basis of the principle that they are minimal variations compatible with some basic intended effect (e.g., some elementary substitution). Thus semantic clauses too, which rely on these transformations as auxiliary functions, can be given uniformly; for example, we can give a unique clause for assignment for any data type in Pascal and Ada-like languages.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/AstesianoReggioEtAl93a.ps.Z

Specifying Reactive Systems by Abstract Events

We consider the problem of specifying reactive systems at different level of abstraction and propose a method for connecting the requirement to the design phase.
As in a variety of other approaches, we assume that a process is modelled by a labelled transition system. The requirement phase is supposed to define a class of models, while at the design level, usually via a stepwise refinement, essentially one model is singled out. The connection between the two phases is provided by the notion of abstract event, with its associated specification language.
An abstract event is defined as a set of its concrete instances, which are labelled transition sequences and can occur as partial paths over labelled transition trees. Abstract events, which may be noninstantaneous and overlapping, are a flexible tool for expressing abstract requirements and, because of their semantics in term of labelled transition sequences, provide a rather transparent support to the refinement procedure.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/AstesianoReggio93e.ps.Z

A Metalanguage for the Formal Requirement Specification of Reactive Systems

Various formalisms have been proposed for the specification of software / hardware systems characterized by the possibility of performing some dynamic activities interacting with an external world, called reactive systems; however in the literature sometimes also terms as: concurrent, parallel, distributed, ... systems have been used for pointing out to some particualr features of the systems; here we simply use the term reactive systems. Some of these formalisms deal with properties at what we may call design level, when already architectural decisions have been taken and a specification determines essentially one structure, though still at a rather abstract level (we say abstract specifications). At the requirement level, the proposed formalisms are dealing with the abstract dynamic properties, i.e. those related to the possible events in a system life, usually classified in safety and liveness properties. Now the experience shows that also the structural properties of a system (including the static data) and their relationships with dynamic features of a system are fundamental also at the requirement level; however the specification mechanism should be able to avoid overspecification, not confusing requirements and design.
In this paper to propose an approach, supported by a metalanguage (schema), for dealing, at the requirement level, with both static and dynamic properties.
The approach is based on a specification formalism which, according to the institution paradigm, consists in models (semantic structures), sentences or formulae (syntax) and validity (semantics of sentences). A specification is a set of formulae determining a class of models, all those satisfying the formulae. The new and central idea of this paper is the proposed models, that we call entity algebras. Those models can support statements about the structure of reactive systems, dealing with the subcomponents of a system, without referring to detailed structuring combinators, which are essential at the design level, but here would spoil the generality of requirements.
In the first section we give a rather informal presentation of entity algebras, illustrated by a small example. In the second we present the syntax of a specification language and in the third section the notion of validity of a formula and the semantic of a specification; some examples concerning also the application to an industrial test case are reported in the fourth section.
Two important comments are in order. First our metalanguage is rather schematic, in the sense that we can choose various formalisms for expressing the dynamic properties. Here, we give just a set of combinators, taken from the branching time logic, sufficient for expressing some common interesting requirements on reactive systems. In general, depending on the specific application field (e.g., industrial plants handled by automatisms, software / hardware architectures and so on) one can choose a minimal set of combinators getting a formalism powerful enough but rather simple. The important point is that now the dynamic formulae are "anchored" to a term representing a dynamic element and so we have a formalism where it is possible to express requirements involving properties on the activity either of different systems or of a system and some of its components; for example we can express properties of the form "a new component which can eventually reach a certain situation cannot be added to a system satisfying some condition".

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/AstesianoReggio93c.ps.Z

Algebraic Specification of Concurrency (invited lecture)

Algebraic specification methods provide techniques for data abstraction and the structured specification, validation and analysis of data structures. Classically, a (concrete) data structure is modelled by a many-sorted algebra; various categories of many-sorted algebras can be considered, like total, partial, order-sorted, with predicates and so on. An isomorphism class of data structures is called an abstract data type (shortly adt) and an algebraic specification is a description of one or more abstract data types. There are various approaches for identifying classes of abstract data types associated with an algebraic specification, which constitute its semantics: initial, terminal, observational; a semantics is loose when it identifies a class (usually infinite) of adt's. Since data structures can be very complex (a flight reservation system, e.g.), structuring and parameterization mechanisms are fundamental for building large specifications.
Together with a rigorous description of data structures, algebraic specifications support stepwise refinement from abstract specifications to more concrete descriptions (in the end, programs) of systems by means of the notion of implementation and techniques for proving correctness of implementations. In this respect formal proof systems associated with algebraic specifications play a fundamental role. Finally specification languages provide a linguistic support to algebraic specifications.
The purpose of the algebraic specification of concurrent systems is to specify structures where some data represent processes or states of processes, i.e. objects about which it is possible to speak of dynamic evolution and interaction with other processes; more generally we can consider as the subject of algebraic specification of concurrency those structures able to describe entities which may be active participants of events. Such data structures will be called simply "concurrent systems", where "concurrent" conveys different meanings, from "occurring together" to "compete for the same resources" and to "cooperate for achieving the same aim".
The aim of this paper is twofold: to analyse the aims and the nature of the algebraic specifications of concurrency and to give, as examples, a short overview of some (not all) relevant work. First we introduce some basic concepts and terminology about processes: the various models around which the specification models are built and the fundamental issues of (observational) semantics, formal description and specification; moreover we give some illustrative examples of specification problems to be used later for making more concrete some general considerations and for assessing different methods. After we try to qualify the field: indicating three different fundamental motivations/viewpoints (and distinguishing between methods and instances); then outlining the issues to deal with; finally illustrating by two significant examples/approaches how this field stimulates innovations and improvements beyond the classical theory of adt's. Finally we outline some relevant approaches; however, being impossible to report on all methods, we have mainly used some approaches to illustrate, as examples, concrete ways of tackling the issues of the field.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/AstesianoReggio93b.ps.Z

Event Logic for Specifying Abstract Dynamic Data Types

A dynamic algebra is just a many-sorted algebra with predicates such that for some of the sorts (dynamic sorts) there is a special predicate defining a labelled transition relation; thus the dynamic elements are modelled by means of labelled transition systems. An abstract dynamic data type (addt) is an isomorphism class of dynamic algebras.
To obtain specifications for addt's we have first used first-order logic; however such logic is not suitable for expressing all interesting abstract properties of dynamic elements. Here we present an "event logic" for specifying addtÕs; the name "event" comes from "event structures". Event structures are a nice formalism for abstractly modelling dynamic elements, which allows to express properties such as causality and true concurrency; but they lack well-developed techniques for structuring detailed descriptions of complex systems.
Event logic is an attempt at building up an integrated specification framework for:

• expressing abstract properties of dynamic elements by giving some "relationships" between events;
• modelling dynamic elements in a simple and intuitive way as labelled transition systems.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it in /person/ReggioG/Reggio93a.ps.Z

Algebraic Specification at Work

Concurrent software systems are used in fields where safety and reliability are critical. In spite of that, the validation of concurrent software tends to rely more on empirical experiments rather than on rigorous proofs. This practice, which is already bad for sequential software, becomes awful for concurrent systems since, due to nondeterminism, the behaviour observed during testing is only the most likely to occur.
We present a formal approach with associated tools for handling this situation. This method allows us to derive from the specification all possible behaviours of a concurrent program and hence to be sure that a tested program will always behave correctly on its test-bed. We outline the approach discussing its application to a typical situation in industrial practice.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/AstesianoGioviniEtAl92b.ps.Z

Observational Structures and their Logic

A powerful paradigm is presented for defining semantics of data types which can assign sensible semantics also to data representing processes. Processes are abstractly viewed as elements of observable sort in an algebraic structure, independently of the language used for their description. In order to define process semantics depending on the observations we introduce observational structures, essentially first-order structures where we specify how processes are observed. Processes are observationally related by means of experiments considered similar depending on a similarity law and relations over processes are propagated to relations over elements of non-observable sort by a propagation law. Thus an observational equivalence is defined, as union of all observational relations, which can be seen as a very abstract generalization of bisimulation equivalences introduced by David Park.
Though being general and abstract our construction allows to extend and improve interesting classical results. For example it is shown that for finitely observable structures the observational equivalence is obtainable as a limit of a denumerable chain of iterations; our conditions, which apply to algebraic structures in general, when instantiated in the case of labelled transition systems, are more liberal than the finitely branching condition. More importantly, we show how to associate with an observational structure various modal observational logics, related to sets of experiment schemas, that we call pattern sets.
The main result of the paper proves that for any family of pattern sets representing the simulation law the corresponding modal observational logic is a Hennessy-Milner logic: two observable objects are observationally equivalent if and only if they satisfy the same set of modal observational formulas. Indeed observational logics generalize to first-order structures various modal logics for labelled transition systems. Applications are shown to multilevel parallelism, higher-order concurrent calculi, distributed and branching bisimulation.
The theory presented in the paper is not at all confined to give semantics of processes. Indeed it provides a general semantic paradigm for abstract data type specifications, where some data are processes. In order to support this claim, in the final section we briefly consider algebraic specifications and give small examples of specifications integrating processes, data types and functions.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/AstesianoGioviniEtAl92a.ps.Z

Abstract Dynamic Data Types: a Temporal Logic Approach

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/CostaReggio91a.ps.Z

Entities: an Institution for Dynamic Systems

The paper introduces the entity framework, entity algebras and specifications, and shows how they can be used for formally modelling and specifying dynamic systems.
Entity algebras give integrated formal models for both data types, processes and objects; they are a subclass of partial algebras with predicates, having the following features: some sorts correspond to dynamic elements (entities); entities may have subcomponent entities together with usual (static) subcomponents; the structure of an entity is not fixed but defined in each case; entities have identities in such a way that it is possible to describe sharing of subcomponents.
Correspondingly to this model level we have entity specifications; more precisely: specifications in the small and specifications in the large; the first ones can be used to formally specify particular dynamic systems; while the latter are suitable for expressing very abstract properties of classes of dynamic systems.
In the paper we consider the specifications in the small showing their properties (e.g., they constitute an institution) and giving several examples; while specification in the large are handled in a forthcoming paper.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/Reggio91a.ps.Z

Processes as Data Types: Observational Semantics and Logic

The paper presents an attempt towards a unifying approach for the semantics of concurrency, abstracting from the particular language used for describing processes.
Processes are here abstractly viewed as elements of observable sort in an algebraic structure; and in order to define appropriate semantics we embody in the algebraic structure an observational viewpoint, obtaining what we call an observational structure. With each observational structure an observational equivalence is associated, which is an abstract version of the well-known bisimulation equivalence of Park for transition systems.
The main result shows how to associate with a class of observational structures a set of modal observational logic formulas, such that an abstract version of the Hennessy-Milner theorem holds.

SMoLCS-Driven Concurrent Calculi

Data in a Concurrent Environment

Integrating specifications of data types and concurrency seems not only a necessity, but an issue to be handled quite naturally. However, if we look at recent research on this topics, we can realize that the integration is very much affected by the basic method for the specification of concurrency. As a result not always the specification of data types is handled in a simple and natural way. We take the position that processes should in a sense just be a data type as any other one and that an overall approach to specification should permit the specification of a data type as in the case when no concurrency is involved. Thus handling the interaction of processes with data should be part of the specification of the dynamic aspects of a system.
Accordingly to this position, since some years (and in cooperation with other authors) we have elaborated a specification technique by which processes/concurrent systems are special abstract data types, modelling concurrent systems as algebraic transition systems with possibly the specification of a parallel structure (in the following "abstract data type" is abbreviated to adt). Our technical framework looks naturally apt to accommodate data type specifications. Indeed all the components of a concurrent system are specified as adts. Moreover, since processes are themselves specified as adts, they can be treated as data. As we permit the specification of functions (we use higher-order algebraic specification), we can thus specify data of any complexity and also model systems where processes are exchanged between processes, stored and so on.
After illustrating our specification technique by means of a simple example we discuss formally the two above aspects.
First we show how the embedding of adt specifications into the specification of a concurrent system does not affect their semantics, whatever is the semantics chosen for the system; second we show that this fact also holds when the data are processes/concurrent systems. Then we tackle the main point of the interaction of processes with objects of some data type.

The Ada Challenge for New Formal Semantic Techniques

Ada is posing new challenging problems in the field of formal definitions, as it is witnessed by the many attempts at a solution.
We argue that the CEC-MAP project on AdaFD could be considered a new starting point, meeting the challenge to some extent. Indeed, following the SMoLCS methodology, the dynamic semantics is split in two parts, formalizing a model for the underlying concurrent structure and then connecting the abstract syntax to that model by a set of denotational, hence compositional, clauses. The formal model is given as an abstract data type which accomodates an operational semantics of concurrency and a parameterized modular specification of all the needed structures.
We outline how the followed approach can handle some of the basic problems, particularly the interference between sequential and concurrent features, together with permitting a local correspondence with the Language Reference Manual. We also point out some problems still to be settled.

Relational Specification and Observational Semantics

This paper introduces a special class of partial abstract data types, called relational specifications, in which some operations with boolean values, called relational operations, play a special role.
Roughly speaking, if r is one of such operations, then any right hand side of a conditional axiom in which r appears, has the form r(t1,...,tn) = true, and in t1,...,tn no relational operation appears. The simple underlying intuition is that r(t1,...,tn) = true asserts that t1,...,tn satisfy a certain observation, formalized by r. Hence a relational specification is meant for defining a data type satisfying some observational requirements.
The motivation for this study is twofold. On one side relational specifications allow a very simple and intuitive theory of behavioural equivalence. In particular it is possible to combine a loose semantics approach to specification, as advocated e.g. in ASL, with the choice of a terminal model in a class of algebras, possibly preserving a fixed model (e.g., initial) of a subspecification.
On the other side the algebraic specification of labelled transition systems used for the specification of concurrent systems are special cases of relational specifications. Indeed, following [BW1], a transition s - f -> s' is expressed by the assertion ->(s,f,s') = true, where -> is seen as a boolean operation. Thus relational specifications are well suited to specify in a unique framework concurrent systems together with their observational semantics. Indeed the present work provides a simple foundation to a parameterized, modular and hierarchical approach to concurrency, the SMoLCS approach, currently adopted in the CEC-MAP project on the formal definition of Ada.
First we give the introductory definitions and results showing the existence of initial models and studying various hierarchical relational specifications. Then we show how a natural semantics expressed by a terminal model can be associated to a relational specification; the terminal model formalizes the idea of behavioural semantics w.r.t. the observations made using the relations. Some applications and examples will illustrate concepts and results throughout the paper.

Technical Reports

A Development Frame for Web Sites -- Complete Version

In this paper we present a "development frame" for web sites.
Technically, a development frame consists of
-- a problem frame, i.e., a pattern that provides a precise conceptual model of what is the problem to be solved;
-- and a precise method based on UML to be used in that specific case. The development frame for web sites presented in this paper have been defined by specializing the precise one proposed by Astesiano and Reggio.

The pdf version of this paper is available at CrivelloReggio05a.pdf.

Requirements Capture and Specification for Enterprise Applications: a UML Based Attempt

We propose a software development method for enterprise applications that combines the use of the structural concepts provided by problem frames, and the use of the UML notation. Problem frames are patterns that provide a precise conceptual model of what is the problem to be solved.
The first step of our method is to match the current task with one of the problem frames that we propose for entreprise applications, and this helps to understand the nature of the problem under study. The problem frames to be considered for enterprise applications are clearly more complex than the basic ones. We then provide guidelines to develop all the artifacts required by the method through a dedicated choice of appropriate UML diagrams together with predefined schemas or skeletons for their contents. Thus, using our method provides a more direct path to the UML models, which saves time (no long questions about which diagrams to use and how) and improves the models quality (relevant issues are addressed, a uniform style is offered). In this paper, we consider the phases of modelling the domain, the requirements capture and specification, and their relationships.
Enterprise Applications cover a wide range of applications. Our method, using problem frames, leads to choose precise concepts to handle appropriate variants.

The pdf version of this paper is available at ChoppyReggio05c.pdf.

A UML-Based Method for the Commanded Behaviour Frame

In this paper we show how to assist the development for problems fitting the Commanded Behaviour frame, using UML with a well-founded approach, and we illustrate our ideas with a lift case study.

The pdf version of this paper is available at ChoppyReggioIWAAF.pdf.

Using UML for Problem Frame Oriented Software Development (Complete Version)

We propose a software development approach that combines the use of the UML notation, the use of the structuring concepts provided by the problem frames, together with our methodological approach for well-founded methods.
The problem frames are used to provide a first idea of the main elements of the problem under study. Then we provide ad hoc UML based development methods for some of the most relevant problem frames together with precise guidelines for the users. The general idea of our method is that, for each frame, several artifacts have to be produced, each one corresponding to a part of the frame.
The description level may range from informal and sketchy, to formal and precise, while this approach is drawn from experience in formal specifications.

The postscript version of this paper is available at UFRAMESlong.ps.

Improving Use Case Based Requirements Using Formally Grounded Specifications (Complete Version)

Our approach aims at helping to produce adequate requirements, both clear and precise enough so as to provide a sound basis to the overall development. Our idea here is to find a way to combine both advantages of use cases and of formal specifications. We present a technique for improving use case based requirements, using the formally grounded development of the requirements specification, and that results both in an improved requirements capture, and in a requirement validation. The formally grounded requirements specification is written in a "visual" notation, using both diagrams and text, with a formal counterpart (written in the Casl and Casl-Ltl languages). Being formally grounded, our method is systematic, and it yields further questions on the system that will be reflected in the improved use case descriptions. The resulting use case descriptions are of high quality, more systematic, more precise, and its corresponding formally grounded specification is available. We illustrate our approach on part of the Auction System case study.

The postscript and pdf versions of this paper are available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/ChoppyReggio03c.ps. and /person/ReggioG/ChoppyReggio03c.pdf.

Casl-Ltl: A Casl Extension for Dynamic Reactive Systems Version 1.0 - Summary

CASL the basic language developed within CoFI, the Common Framework Initiative for algebraic specification and development, cannot be used for specifying the requirements and the design of dynamic software systems. CASL-LTL is an extension to overcome this limit, allowing to specify dynamic system by modelling them by means of labelled transition systems and by expressing their properties with temporal formulae. It is based on LTL, the Labelled Transition Logic, that is a logic-algebraic formalism for the specification of dynamic systems, mainly developed by E.Astesiano and G. Reggio.

This document gives a detailed summary of the syntax and intended semantics of CASL-LTL. It is intended for readers who are already familiar with CASL.

The postscript and pdf versions of this paper are available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/ReggioEtAll03b.ps. and /person/ReggioG/ReggioEtAll03b.pdf.

Towards a Formally Grounded Software Development Method

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 languages) 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/language 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 and paradigms 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 and two specification approaches, 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. We also support both property-oriented (axiomatic) and model-oriented (constructive) specifications. We are thus providing support for the "building-bricks" tasks of specifying/modelling software artifacts that in our experience are needed for the development process.

Our approach is illustrated with a lift case study, it was also used with other large case studies, and when used on projects by students yielded homogeneous results.

Let us note that it may be used either as itself, e.g., for requirements specification, or in combination with structuring concepts such as the Jackson's problem frames.

The postscript and pdf versions of this paper are available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/ChoppyReggio03a.ps. and /person/ReggioG/ChoppyReggio03a.pdf.

Tight Structuring for Precise UML-based Requirement Specifications (Complete Version)

On the basis of some experience in the use of UML-based use case-driven methods, we believe and claim, contrary to a recent wave for allowing almost total freedom as opposed to disciplined methods, that a tighter and more precise structuring of the artifacts for the different phases of the software development process may help speed-up the process, while obviously making easier the consistency checks among the various artifacts. To support our claim we have started to investigate an approach, that, though being compliant with the UML notation and a number of UML-based methods, departs from them both in the basic philosophy, that follows the "tight and precise" imperative, and in the technical solutions for structuring the various artifacts.
Building on some previous work concerning the structure of the requirement specification artifacts, here we complete upwards and improve our proposal, investigating the link between the analysis of the problem domain and the requirement capture and specification. Indeed, one of our assumptions, as advocated by some methodologists and backed by our own experience, is the neat separation between the problem domain and the system.
To that purpose we propose a rather new way of structuring the problem domain model and then the link with the system, that encompasses the most popular current approaches to domain modelling. Then we exploit both the domain model and our requirement specification frame for capturing and specifying the requirements. From our construction we can derive rigorous guidelines, only hinted to here, for the specification tasks, in a workflow that allows and suggests iteration and incrementality, but in a way that is not just based on the single use cases and takes more care of the overall construction. The various concepts and constructions are illustrated with the help of a small running case study.

The pdf version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/AstesianoReggio03c.pdf.

Consistency Problems in UML-based Software Development: Workshop Materials

The pdf version of this book is available at http://www.ipd.bth.se/uml2002/RR-2002-06.pdf.

Between PIM and PSM: the P2P Case

We address in general the problem of providing a methodological and notational support for the software development at the design level of applications based on the use of a middleware. In particular, because of the growing interest in mobile applications with nomadic users, we consider the middlewares supporting a peer-to-peer architecture. In order to keep the engineering support at the appropriate level of abstraction we formulate our support within the frame of Model Driven Architecture (MDA), the approach proposed by OMG that considers the design development starting with a Platform Independent Model (PIM) then mapped into one or more Platform Specific Models (PSM) for different platforms, where a model has to be understood in a UML sense.

In this paper our main aim is to advocate the introduction of an intermediate abstraction level, called ASM for Architecture Specific Model, that is particularly suited to abstract away the basic common architectural features of different platforms, further separating concerns and allowing a greater flexibility and reuse when implementing on specific platforms. That solution seems particularly advantageous in presence of many proposals of peer-to-peer middlewares.

Technically, the support for the ASM level is presented in the form of a UML, hence object-oriented, profile which embodies a basic abstract peer-to-peer paradigm architecture. Within that profile the connection with middleware is for each peer naturally represented by an object whose operations correspond to its primitives.

To be concrete all concepts and notations are illustrated by means of a running example.

The pdf version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/ReggioEtAll02a.pdf.

Metamodelling Behavioural Aspects: the Case of the UML State Machines (Complete Version)

The "object-oriented meta-modeling" seems currently to be one of the most promising approach to the "precise" definition of UML.
Essentially this means using a kernel object-oriented visula notation to define UML.
This has proved itself to be an intuitive way of defining the abstract syntax of UML. For what concerns the "static part", the initial work of the pUML group seems to confirm that the approach is workable, whereas no convincing proposal have been presented to cover the dynamic aspects, as active classes, cooperation/communications among active objects, state charts, sequence diagrams, and so on.

We think that to conveniently and precisely define such aspects, we need an underlying formal model of the dynamic behaviour of the active objects, and we think, supported by our past experience, that labelled transition systems are a good one.
We thus propose how to use a kernel visual notation to define labelled transition systems in an object-oriented way. Furthermore, we present also a new kind of diagrams, quite similar to state charts, LTD (Labelled Transition Diagrams) to visually present such definitions.

As an example, we work out the meta-model of the state machines starting from our formal definition of their semantics based on labelled transition systems.

The postscript and the pdf versions of this paper are available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/Reggio02b.ps. and /person/ReggioG/Reggio02b.pdf.

A Middleware-Oriented Visual Notation for Distributed Mobile Systems

We are witnessing a growing demand for applications characterized by decentralization and mobility for which the peer-to-peer paradigm seems to have some clear advantages.
The use of a middleware, encapsulating the treatment of distribution and mobility and providing appropriate abstractions for handling them in a transparent way, improves and simplifies the development of such applications.
In this paper we present a visual notation supporting the development of software based on such middleware.
Our notation is characterized by the integration of the middleware into an OO paradigm, as an object whose operations correspond to the middleware primitives, and is UML-based, in the sense that, following the official UML terminology, we propose a new UML profile.
The models in our profile include diagrams to describe the software and the data on each kind of peer, the required cooperations among peers, the architecture of the overall system and the deployment on an actual network.

The pdf version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/ReggioEtAll01a.pdf.

A Proposal of a Dynamic Core for UML Metamodelling with MML

We present an initial proposal for an extension of MML, the basic language of [1], by adding a dynamic core and a basic visual notation to represent behaviour. Then we give some hints on how to use this extension for metamodelling UML covering the behavioural-dynamic aspects.
The presentation will follow the style of [1].
This report has to be considered complementary to [1].
[1] T.Clark, A.Evans, S.Kent, S.Brodsky, and S.Cook.
A Feasibility Study in Rearchitecting UML as a Family of Languages using a Precise OO Meta-Modeling Approach - Version 1.0. (September 2000).
Available at http://www.cs.york.ac.uk/puml/mmf.pdf, 2000.

The pdf version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/ReggioAstesiano01a.pdf.

An Extension of UML for Modelling the nonPurely-Reactive Behaviour of Active Objects

Modelling nonpurely-reactive systems, such as agents and autonomous processes, does not find a direct support in the UML notation as it stands, and it is questionable whether it is possible and sensible to provide it in the form of a lightweight extension via stereotypes.

Thus we propose to extend the UML notation with a new category of diagrams, "behaviour diagrams", which are, in our opinion, complementary to statecharts for nonpurely-reactive processes (active objects). The proposed diagrams, to be used at the design level, also enforce localization\encapsulation at the visual level. Together with motivating and presenting the notation, we also discuss the various possibilities for presenting its semantics in a palatable way, depending on the reader.

The pdf version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/ReggioAstesiano00b.pdf.

Casl-Chart: Syntax and Semantics

The postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/ReggioRepetto00a.ps.

A CASL Formal Definition of UML Active Classes and Associated State Machines

The postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/Reggio99b.ps.

Thirty one Problems in the Semantics of UML 1.3 Dynamics

The postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/ReggioWieringa99a.ps

Using CASL to Specify the Requirements and the Design: A Problem Specific Approach -- Complete Version

In its book, "Software Requirements & Specifications: a Lexicon of Practice, Principles and Prejudices" (Addison-Wesley, 1995) M. Jackson introduces the concept of problem frame to describe specific classes of problems, to help in the specification and design of systems, and also to provide a framework for reusability. He thus identifies some particular frames, such as the translation frame (e.g., a compiler), the information system frame, the control frame (or reactive system frame), ... Each frame is described along three viewpoints that are application domains, requirements, and design.
Our aim is to use CASL (or possibly a sublanguage or an extension of CASL if and when appropriate) to formally specify the requirements and the design of particular classes of problems ("problem frames"). This goal is related to methodology issues for CASL, that are here addressed in a more specific way, having in mind some particular problem frame, i.e. a class of systems.
It is hoped that this will provide both a help in using, in a really effective way, CASL for system specifications, a link with approaches that are currently used in the industry, and a framework for the reusability of CASL specifications.
This approach is illustrated with some case studies, e.g., the information system frame is illustrated with the invoice system case study.

The postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/ChoppyReggio99a.ps

Abstract Data Types and UML Models

Object-oriented modelling, using for instance the Unified Modeling Language (UML), is based on the principles of data abstraction and data encapsulation. In this paper, we closely examine the relationship between object-oriented models (using UML) and the classical algebraic approach to data abstraction (using the Common Algebraic Specification Language CASL).
Technically, possible alternatives for a translation from UML to CASL are studied, and analysed for their principal consequences.
It is shown that object-oriented approaches and algebraic approaches differ in their view of data abstraction. Moreover, it is explained how specification methodology derived from the algebraic world can be used to achieve high quality in object-oriented models.

The pdf version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/HussmannEtAlt99a.pdf

A Proposal for a Semantics of a Subset of Multi-Threaded Good Java Programs

We have given an operational semantics to multi-threaded Java (leaving aside, for the moment, mechanism for distributed computing) by following the informal specification given by the language developers.
This work had pointed out some questionable properties of the Java programs concerning the way concurrent threads can interact with shared objects. Java semantics allows the access to shared objects to occur in a very loose way and this sometimes has very strange effects and makes it impossible or, at least, very hard to reason about concurrent programs. We have formally characterized one subclass of Java programs having acceptable properties guaranteeing a reliable use of shared variables, based on the idea that the mechanism ensuring such properties is the use of synchronization.
The good point, is that the restriction to the class of Java programs allows the use of a simpler operational semantics, and, consequently, simpler observations and equivalence notion.

The postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/CosciaE/papers/JavaVancouver.ps

UML as Heterogeneous Multiview Notation: Strategies for a Formal Foundation

The postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/AstesianoReggio98e.ps.

A Graphic Specification of a High-Voltage Station

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/Reggio98d.ps.Z

Labelled Transition Logic: An Outline

In the last ten years we have developed and experimented in a series of projects, including industry test cases, a method for the specification of reactive concurrent systems both at the requirement and at the design level. We present here in outline its main technical features, providing pointers to appropriate references for more detailed presentations of single aspects and of the associated tools and reference manuals.
The overall main feature of the method is its logical\algebraic character, since it extends to labelled transition systems the logical\algebraic specification method of abstract data types and processes are viewed as data within first-order structures called LT-structures. Some advantages of the approach are the full integration of the specification of static data and of dynamic elements, which includes by free higher-order concurrency, and the exploitation of well-explored classical techniques in many respects, including implementation and tools.
On the other hand the use of labelled transition systems for modelling processes, inspired by CCS, allows us to take advantage, with appropriate extensions, of some important concepts, like communication mechanisms and observational semantics, developed in the area of concurrency around CCS, CSP and related approaches.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/AstesianoReggio96d.ps.Z

Specification of a High-Voltage Substation: Revised Tool-Checked Version

Specification of a Hydroelectric Power Station: Revised Tool-Checked Version

Formally-Driven Friendly Specifications of Concurrent Systems: A Two-Rail Approach

Throughout a multiannual projects with industry people on the applicability of a formal method for the specification of concurrent systems, it became apparent that, to make that method acceptable, it would be convenient, not to say necessary to have at hand, in all phases of the development process, an informal counterpart of the formal specification. As a catchword we suggest a "two-rail principle", to say that informal and formal specifications should proceed in parallel. Quite obviously the aim is twofold: on one side to overcome the skill problem, typical of most developers with an insufficient educational background and on the other one easing the interaction with clients and users, who quite often have a completely different background.
Hence we raise the question whether that principle is sensible and always advisable or just to be confined to special situations.
Here we offer the result of our experience, i.e. the instantiation of that principle to the method developed within that project. A key idea was to derive the schema for informal specifications from the formal method and not vice versa. In close analogy with what happens for program development in structured programming, in our method the development process is guided by a documentation language, whose structure is suggested by and embodies the structure of the models for the development phases and for the ultimate product (here the concurrent system).
The final document includes at every stage a natural language description (provided and\or checked by the client), a formal specification (perhaps done by a team of specialists) and a formally-driven informal specification (for the non-specialist developers and as an interface with the natural language description).

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/AstesianoReggio94a.ps.Z

The Reference Manual for the SMoLCS Methodology

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/ReggioBertelloEtAl94a.ps.Z

METAL: a Metalanguage for SMoLCS

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/ReggioG/ParodiReggio94a.ps.Z

Formal Specification of the Cnet Inter-node Communication Architecture