Publications of Gianna Reggio
From Conditional Specifications to Interaction Charts:
A Journey from Formal to Visual Means to Model Behaviour
E. Astesiano and
G. Reggio.
In
Formal Methods in Software and System Specification.
Lecture Notes in Computer Science,
Berlin, Springer Verlag, 2005. To appear.
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
C. Choppy and G. Reggio.
Journal of Logic and Algebraic Programming.
Elsevier.
To appear. 2005.
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 (logicalalgebraic)
specification languages Casl (Common Algebraic Specification
Language, developed within the joint initiative CoFI)
and for an extension for dynamic systems CaslLTL,
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 propertyoriented (axiomatic)
specifications.
We are thus providing support for the "buildingbricks" 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 UMLBased Approach for Problem Frame Oriented Software Development
C. Choppy and G. Reggio.
Journal of Information and Software Technology.
Elsevier.
To appear. 2005.
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
wellfounded 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 UMLBased Method for the Commanded Behaviour Frame
C. Choppy and G. Reggio.
In Proc. of the 1st International Workshop on
Advances and Applications of Problem Frames (IWAAPF 2004); an ICSE 2004 workshop.
K. Cox and J.G. Hall and L. Rapanotti editors.
IEEE, 2004.
Using UML for Problem Frame Oriented Software Development
C. Choppy and G. Reggio.
In Proc of
the ISCA 13th Int. Conf. on Intelligent and Adaptative Systems and
Software Engineering (IASSE2004). W. Dosch and N. Debnath editors.
The International Society for Computers and Their
Applications (ISCA), USA, 2004.
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
wellfounded 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 LuxembourgKirchberg, Luxembourg, November 2728, 2003 Revised Papers.
N. Guelfi, E. Astesiano and
G. Reggio (editors).
Lecture Notes in Computer Science n. 2952,
Berlin, Springer Verlag, 2004.
Tight Structuring for Precise UMLbased Requirement Specifications
E. Astesiano and G. Reggio.
In
Radical Innovations of Software and Systems Engineering in the Future,
Proc. 9th Monterey Software Engineering Workshop, Venice, Italy, Sep. 2002.
Lecture Notes in Computer Science n. 2941,
Berlin, Springer Verlag, 2004.
On the basis of some experience in the use of
UMLbased use casedriven 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 speedup 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 UMLbased
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
E. Astesiano, M.
Cerioli and
G. Reggio.
In
Radical Innovations of Software and Systems Engineering in the Future,
Proc. 9th Monterey Software Engineering Workshop, Venice, Italy, Sep. 2002.
Lecture Notes in Computer Science n. 2941,
Berlin, Springer Verlag, 2004.
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 peertopeer
architecture, because of the growing interest in mobile applications
with nomadic users and the presence of many proposals of peertopeer
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
C..Choppy and G. Reggio.
In Proc. FASE 2004.
Lecture Notes in Computer Science, n. 2984.
Berlin, Springer Verlag, 2004.
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 CaslLtl 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 WellFounded UMLbased Development Method
E. Astesiano and G. Reggio.
In Proc. FASE 2004.
IEEE Computer Society, 2003.
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 WellFounded 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 wellfounded method  which is ModelDriven and adopts a UML notation.
Here, after introducing our basic philosophy and the WellFounded methods strategy,
we outline in summary our sample approach and, as a new contribution,
we show in some detail how to handle the ModelDriven 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 WellFounded Software Development Methods
E. Astesiano, G. Reggio
and M. Cerioli.
In Formal Methods at the Crossroads:
From Panacea to Foundational Support.
10th Anniversary Colloquium of UNU/IIST
the International Institute for Software Technology of
The United Nations University, Lisbon, Portugal, March 1820, 2002.
Revised Papers.
Lecture Notes in Computer Science n. 2757,
Berlin, Springer Verlag, 2003.
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 WellFounded 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 UseCase Driven Method
and AgentOriented Techniques
E. Astesiano and
G. Reggio.
In
Proc. SEKE 2003.
ACM Press, 2003.
In this paper we discuss how to combine a multiview
usecase driven method for the requirement specification of
a system with an agentoriented 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
E. Astesiano and
G. Reggio.
In
Recent Trends in Algebraic Development Techniques 16th
International Workshop, WADT 2002  Frauenchiemsee, Germany, September 2427, 2002.
Revised Selected Papers.
Lecture Notes in Computer Science, n. 2755
Berlin, Springer Verlag, 2003.
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 wellknown 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:
International Workshop, LuxembourgKirchberg, Luxembourg, November 2002. Revised
Papers.
N. Guelfi, E. Astesiano and
G. Reggio (editors).
Lecture Notes in Computer Science n. 2604,
Berlin, Springer Verlag, 2003.
A Notation to Support ComponentBased Design of Java Applications
C. Amza and
G. Reggio.
In FIDJI'2002  Scientific Engineering of Distributed Java Applications, proceedings of the
2nd International Workshop, LuxembourgKirchberg,
Luxembourg, November 2002(N. Guelfi, E. Astesiano and G. Reggio eds.).
Lecture Notes in Computer Science n. 2604,
Berlin, Springer Verlag, 2003.
In this paper we present JTN2 (Java Targeted Notation 2) a notation
for componentbased design of Java applications. JTN2 defines a component
model based on the fundamental objectoriented principles: abstraction,
encapsulation, modularization and typing. Indeed, JTN2 is an extension of JTN,
an objectoriented, 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. Predesigned 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
G. Reggio.
In Proc. IDPT 2002.
Society for Design and Process Science, USA, 2002.
CD included.
The "objectoriented metamodeling" seems currently to be
one of the most promising approach to the "precise" definition of UML.
Essentially this means using a kernel objectoriented 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 objectoriented 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 metamodel 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
E. Astesiano and G. Reggio.
In Proc. SEKE 2002.
ACM Press, New York, 2002.
On the basis of some experience in the use of use casedriven and
UMLbased methods, we believe that a more refined and stringent
structuring of the knowledge in the artifacts of a
Requirement Specification may help speedup
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
bestknown 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 casedriven and UMLbased; thus also
objectoriented.
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
E. Astesiano and
G. Reggio.
In Acta Informatica, Vol. 37. n.11,12, 2001.
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 firstorder structures called LTstructures.
Some advantages of the approach are the full integration of the specification
of static data and of dynamic
systems, which includes by free higherorder concurrency, and the exploitation of
wellexplored 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
G. Reggio, M.
Cerioli and E. Astesiano.
In Proc. FASE 2001 (H. Hussmann Editor).
Lecture Notes in Computer Science n. 2029,
Berlin, Springer Verlag, 2001.
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.
UMLSPACES:
A UML Profile for Distributed Systems Coordinated Via Tuple Spaces
E. Astesiano and
G. Reggio.
In Proc. ISADS 2001, IEEE Computer Society Press, 2001.
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
C. Choppy and
G. Reggio.
In Recent Trends in Data Type Specifications.
14th Workshop on Specification of Abstract Data Types.
(D. Bert and C. Choppy editors),
Lecture Notes in Computer Science, n. 1827,
Berlin, Springer Verlag, pages 106125, 2000.
In its book, "Software Requirements & Specifications:
a Lexicon of Practice, Principles and Prejudices"
(AddisonWesley, 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
G. Reggio, M. Cerioli and E. Astesiano.
In Proc. AMiLP 2000 (D. Heylen, A. Nijholt and G. Scollo Editors).
Twente Workshop on Language Technology n. 16,
Enschede, University of Twente, 2000.
We aim at using algebraic techniques, and in particular an extension,
CaslLtl 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 ParadigmSpecific Languages:
towards an Application to UML (Invited Lecture)
E. Astesiano, M. Cerioli and G. Reggio.
In Proc. AMAST 2000 (T. Rus Editor).
Lecture Notes in Computer Science n. 1816,
Berlin, Springer Verlag, 2000.
We are interested in the composition of languages, in particular a
data description language and a paradigmspecific language, from a
pragmatic point of view.
Roughly speaking our goal is the description of languages in a
componentbased 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
"paradigmspecific" 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 "prepost" 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
CASLCHART: a Combination of
Statecharts and of the Algebraic Specification Language CASL
G. Reggio and L. Repetto.
In Proc. AMAST 2000 (T. Rus Editor).
Lecture Notes in Computer Science n. 1816,
Berlin, Springer Verlag, 2000.
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
G. Reggio,
E. Astesiano, C. Choppy and H. Hussmann.
In Proc. FASE 2000  Fundamental Approaches to Software Engineering.
Lecture Notes in Computer Science n. 1783 (T. Maibaum Editor),
Berlin, Springer Verlag, 2000.
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
E. Astesiano and
G. Reggio.
In T.C.S., Vol. 236. n.1,2, 2000.
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
R. Wieringa, E. Astesiano,
G. Reggio,
A. Le Guennec,
H. Hussman,
K. van den Berg, P. van den Broek.
In ECOOP Workshop Reader: UML Semantics FAQ(S.Kent, A.Evans, B. Rumpe editors), 1999.
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 JavaTargeted Graphic
Formal Notation for Reactive and Concurrent Systems
E. Coscia and G. Reggio.
In Proc. FASE 99  Fundamental Approaches to Software Engineering.
Lecture Notes in Computer Science,
Berlin, Springer Verlag, 1999.
JTN is a formal graphic notation for Javatargeted 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/JTNFase.ps
Stores as Homomorphisms and Their Transformations 
A Uniform Approach to Structured Types in Imperative Languages
E. Astesiano,
G. Reggio and
E. Zucca.
Science of Computer Programming, Vol. 34. n.3, pages 163190,
1999.
We address the problem of giving a clean and uniform mathematical model
for handling user defined data types in imperative languages, contrary to
the adhoc 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
E. Astesiano, M. Broy and
G. Reggio.
In IFIP WG 1.3 Book on Algebraic Foundations of System Specification
(E. Astesiano, B. KriegBruckner and H.J. Kreowski editors),
Berlin, Springer Verlag, 1999.
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 firstorder structure or algebra) in which some elements
represent concurrent systems.
We can qualify the approaches of this kind as
"algebraic specifications of dynamicdata 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 datatypes"; 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
E. Astesiano and G. Reggio.
In Requirements Targeting Software and Systems Engineering, Proc. RTSE '97.
(M. Broy and B. Rumpe editors),
Lecture Notes in Computer Science, n. 1526
Berlin, Springer Verlag, 1998.
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 wellknown 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 prefeatures (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 antiframe 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
G. Reggio.
In Proc. of Int. Workshop "Comparing Specification
Techniques: What Questions Are Prompted by Ones Particular Method of
Specification. March 1998, Nantes (France) (M. Allemand, C. Attiogbe
and H. Habrias editors),
IRIN  Universite de Nantes, 1998.
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 branchingtime temporal logic,
which can be termed firstorder, manysorted, with edgeformulae 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 (nonstructured) 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
M. Cerioli and G. Reggio.
In Mathematical Structures in Computer Science, 1997.
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 hyperloose 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
G. Reggio and M. Larosa.
In Proc. FME 97  Industrial Applications and Strengthened Foundations of Formal Methods
(J. Fitzgerald and C.B. Jones editors),
Lecture Notes in Computer Science, n. 1313,
Berlin, Springer Verlag, 1997.
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
E. Astesiano and G. Reggio.
In Proc. TAPSOFT '97
(M. Bidoit and M. Dauchet editors),
Lecture Notes in Computer Science, n. 1214,
Berlin, Springer Verlag, pages 93114, 1997.
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
G. Costa and G. Reggio.
In T.C.S., Vol. 173. n. 2, pages 513554, 1997.
A concrete dynamicdata 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 dynamicdata type (addt) is an isomorphism class of such algebras.
To obtain specifications for addt's, we propose a logic which combines
manysorted firstorder logic with branchingtime 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 RPCMemory Problem
E. Astesiano and G. Reggio.
In Formal System Specification:
The RPCMemory Specification Case Study
(M. Broy, S. Merz and K. Spies editors),
Lecture Notes in Computer Science, n. 1169,
Berlin, Springer Verlag, pages 67108, 1996.
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
E. Coscia and G. Reggio.
In Recent Trends in Data Type Specifications.
11th Workshop on Specification of Abstract Data Types. Oslo Norway, September 1995
(M.Haveraaen, O. Owe and O.J. Dahl editors),
Lecture Notes in Computer Science, n. 1130,
Berlin, Springer Verlag, pages 161182, 1996.
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
(nonpermitted) activities,
making more natural the specification of recovery policies after non ideal behaviours.
Moreover,
deontic qualifications on behaviour may be combined with branchingtime 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
E. Astesiano, G. Reggio and
F. Morando
In Proc. of TAPSOFT '95
( P.D. Mosses, M. Nielsen and M.I. Schwartzbach editors),
n. 915 of Lecture Notes in Computer Science,
Berlin, Springer Verlag, pages 810801, 1995.
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
M. Cerioli and G. Reggio
In Algebraic Methodology and Software Technology (AMAST'93)
(M. Nivat, C. Rattray, T. Rus and G. Scollo editors),
Workshops in Computing,
London, Springer Verlag, 1993.
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 highlevel
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 nonovercomplex) and the addition of the features
needed in the particular case (e.g. entities for structured parallelism or
higherorder 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 algebraicoriented
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 algebraicoriented institution is
an algebraicoriented 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 algebraicoriented 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
knowhow 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
M. Cerioli and G. Reggio
In Recent Trends in Data Type Specification
(H. Ehrig and F. Orejas editors),
n. 785 of Lecture Notes in Computer Science,
Berlin, Springer Verlag, pages 113127, 1994.
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 wellestablished 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 HighLevel Algebraic Petri Nets
M Bettaz and G. Reggio
In Recent Trends in Data Type Specification
(H. Ehrig and F. Orejas editors),
n. 785 of Lecture Notes in Computer Science,
Berlin, Springer Verlag, pages 98112, 1994.
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
E. Astesiano, G. Reggio and
E. Zucca
In Proc. MFCS'93 (Mathematical Foundations of Computer Science)
(H. Ehrig and F. Orejas editors),
n. 711 of Lecture Notes in Computer Science,
Berlin, Springer Verlag, pages 242251, 1993.
In the classical denotational model of imperative languages
handling structured types, like arrays, requires an
adhoc treatment for each data type, including e.g. an adhoc 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 Pascallike 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 wellknown 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 Adalike 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
E. Astesiano and G. Reggio
In Proc. of Seventh International Workshop on Software Specification and Design (IWSSD7),
Los Alamitos, CA,
IEEE Computer Society, 1993.
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
E. Astesiano and G. Reggio
In Proc. FME'93: IndustrialStrength Formal Methods
(J.C.P. Woodcock and P.G. Larsen editors),
n. 670 of Lecture Notes in Computer Science,
Berlin, Springer Verlag, 1993.
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)
E. Astesiano and G. Reggio
In Recent Trends in Data Type Specification
(M. Bidoit and C. Choppy editors),
n. 655 of Lecture Notes in Computer Science,
Berlin, Springer Verlag, pages 139, 1993.
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 manysorted algebra;
various categories of manysorted algebras
can be considered, like total, partial, ordersorted, 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
G. Reggio
In Recent Trends in Data Type Specification
(M. Bidoit and C. Choppy editors),
n. 655 of Lecture Notes in Computer Science,
Berlin, Springer Verlag, pages 292309, 1993.
A dynamic algebra is just a manysorted 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 firstorder 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 welldeveloped 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 basic idea is that, given a labelled transition system, an "event"
is just a set of partial execution paths (those corresponding to occurrences of that event).
As a consequence, we have that in this framework events are not considered
instantaneous and so we can also express finer relationships between them, as:

there is no instant at which e' and e" occur simultaneously,

e is the sequential composition of e' and e",

each occurrence of e' includes an occurrence of e"
(i.e., e" starts either together or after e' and terminates either before or together e').
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
E. Astesiano, A. Giovini,
F. Morando and
G. Reggio.
In Proc. AMAST'91 (Algebraic Methodology and Software Technology),
Berlin, Springer Verlag, 1992.
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 testbed.
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
E. Astesiano, A. Giovini and
G. Reggio.
In T.C.S., Vol. 96, 1992, pages 249283.
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 firstorder 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
nonobservable 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 HennessyMilner 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
firstorder structures various modal logics for labelled transition systems.
Applications are shown to multilevel parallelism, higherorder 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
G. Costa and
G. Reggio.
In Proc. MFCS'91 (A. Tarlecki editor),
n. 520 of Lecture Notes in Computer Science,
Berlin, Springer Verlag, pages 103112, 1991.
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
G. Reggio.
In Recent Trends in Data Type Specification
(H. Ehrig, K.P. Jantke, F. Orejas and H. Reichel editors),
n. 534 of Lecture Notes in Computer Science,
Berlin, Springer Verlag, pages 244265, 1991.
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
E. Astesiano,
A. Giovini and
G. Reggio.
In Proc. of 18eme Ecole de Printemps en Informatique Theorique, Semantique du Parallelism
(I. Guessarian editor),
n. 469 of Lecture Notes in Computer Science,
Berlin, Springer Verlag, pages 120, 1990.
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 wellknown 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 HennessyMilner theorem holds.
SMoLCSDriven Concurrent Calculi
E. Astesiano and
G. Reggio.
In Proc. TAPSOFT'87, Vol. 1
(H. Ehrig, R. Kowalski, G. Levi and U. Montanari editors),
n. 249 of Lecture Notes in Computer Science,
Berlin, Springer Verlag, pages 169201, 1987.
Data in a Concurrent Environment
E. Astesiano,
A. Giovini and
G. Reggio.
In Proc. Concurrency '88 (International Conference on Concurrency), Hamburg, R.F.T., 1988
(F. Vogt editor),
n. 335 of Lecture Notes in Computer Science,
Berlin, Springer Verlag, pages 140159, 1988.
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 higherorder 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
E. Astesiano,
A. Giovini, F. Mazzanti,
G. Reggio and
E. Zucca .
In Ada: Managing the Transition, Proc. of the AdaEurope International Conference, Edimburgh, 1986,
Cambridge, University Press, pages 239248, 1986.
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 CECMAP 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
E. Astesiano,
G. Reggio and M. Wirsing.
In Proc. MFCS'86,
n. 233 of Lecture Notes in Computer Science,
Berlin, Springer Verlag, pages 209217, 1986.
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 CECMAP
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
E. Crivello and G. Reggio.
Technical Report of DISI  Università di Genova,
DISITR0516, Italy, 2005.
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
C. Choppy and G. Reggio.
Technical Report of DISI  Università di Genova,
DISITR0510, Italy, 2005.
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 UMLBased Method for the Commanded Behaviour Frame
C.Choppy and G. Reggio.
Technical Report of DISI  Università di Genova,
DISITR0412, Italy, 2004.
In this paper we show
how to assist the development for problems fitting the Commanded Behaviour
frame, using UML with a wellfounded 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)
C.Choppy and G. Reggio.
Technical Report of DISI  Università di Genova,
DISITR0411, Italy, 2004.
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
wellfounded 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)
C.Choppy and G. Reggio.
Technical Report of DISI  Università di Genova,
DISITR0345, Italy, 2003.
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 CaslLtl
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.
CaslLtl: A Casl Extension for Dynamic Reactive Systems Version 1.0  Summary
G. Reggio, E.
Astesiano and C. Choppy.
Technical Report of DISI  Università di Genova,
DISITR0336, Italy, 2003.
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.
CASLLTL 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
logicalgebraic 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 CASLLTL. 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
C.Choppy and G. Reggio.
Technical Report of DISI  Università di Genova,
DISITR0335, Italy, 2003.
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 (logicalalgebraic)
specification languages CASL (Common Algebraic Specification
Language, developed within the joint initiative CoFI)
and for an extension for dynamic systems CASLLTL,
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 propertyoriented (axiomatic) and
modeloriented (constructive) specifications.
We are thus providing support for the "buildingbricks" 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 UMLbased Requirement Specifications
(Complete Version)
E. Astesiano and G. Reggio.
Technical Report of DISI  Università di Genova,
DISITR034, Italy, 2003.
On the basis of some experience in the use of
UMLbased use casedriven 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 speedup 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 UMLbased
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 UMLbased Software Development: Workshop Materials
L. Kuzniarz, G. Reggio,
J.L. Sourrouille and Z. Huzar (editors).
Research Report Blekinge Institute of Technology (Sweden), 200206, 2002.
The pdf version
of this book is available at
http://www.ipd.bth.se/uml2002/RR200206.pdf.
Between PIM and PSM: the P2P Case
G. Reggio, M.
Cerioli and E. Astesiano.
Technical Report of DISI  Università di Genova,
DISITR0249, Italy, 2002.
Presented at "Monterey 2002 Workshop:
Radical Innovations of Software and SystemsEngineering in the Future", Venezia October 2002.
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 peertopeer 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 peertopeer middlewares.
Technically, the support for the ASM level is presented in the form of
a UML, hence objectoriented, profile which embodies a
basic abstract peertopeer 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)
G. Reggio.
Technical Report of DISI  Università di Genova,
DISITR023, Italy, 2002.
The "objectoriented metamodeling" seems currently to be
one of the most promising approach to the "precise" definition of UML.
Essentially this means using a kernel objectoriented 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 objectoriented 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 metamodel 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 MiddlewareOriented Visual Notation for Distributed Mobile Systems
G. Reggio, M.
Cerioli
and E. Astesiano.
Technical Report of DISI  Università di Genova,
DISITR0154, Italy, 2001.
We are witnessing a growing demand for applications characterized by
decentralization and mobility for which the peertopeer
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 UMLbased, 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
G. Reggio and E. Astesiano.
Technical Report of DISI  Università di Genova,
DISITR0117, Italy, 2001.
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 behaviouraldynamic 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 MetaModeling 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
nonPurelyReactive Behaviour of Active Objects
G. Reggio and E. Astesiano.
Technical Report of DISI  Università di Genova,
DISITR0028, Italy, 2000.
Modelling nonpurelyreactive 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 nonpurelyreactive 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.
CaslChart: Syntax and Semantics
G. Reggio and L. Repetto.
Technical Report of DISI  Università di Genova,
DISITR0001, Italy, 2000.
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
G. Reggio,
E. Astesiano, C. Choppy and H. Hussman.
Technical Report of DISI  Università di Genova,
DISITR9916, Italy, 1999.
Revised March 2000.
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
G. Reggio and R. Wieringa.
OOPSLA'99 workshop "Rigorous Modelling and Analysis of the UML: Challenges and Limitations",
Denver, 1999.
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
C. Choppy and
G. Reggio.
Technical Report of DISI  Università di Genova,
DISITR9933, Italy.
1999.
In its book, "Software Requirements & Specifications:
a Lexicon of Practice, Principles and Prejudices"
(AddisonWesley, 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
H. Hussmann, M. Cerioli, G. Reggio and F. Tort.
Technical Report of DISI  Università di Genova,
DISITR9915, Italy.
1999.
Objectoriented 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 objectoriented 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 objectoriented
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 objectoriented 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
MultiThreaded Good Java Programs
E. Coscia and
G. Reggio.
Technical Report of Imperial College  London,
1998.
We have given an operational semantics to multithreaded 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
E. Astesiano and
G. Reggio.
Technical Report of DISI  Università di Genova,
DISITR9815, Italy, 1998.
Presented at
the OOPSLA Workshoop: Formalizing
UML. Why? How?, Vancouver, October 1998.
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 HighVoltage Station
G. Reggio.
Technical Report of DISI  Università di Genova,
DISITR9833, Italy, 1998.
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
E. Astesiano and
G. Reggio.
Technical Report of DISI  Università di Genova,
DISITR9620, Italy, 1996.
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 firstorder structures called LTstructures.
Some advantages of the approach are the full integration of the specification
of static data and of dynamic
elements, which includes by free higherorder concurrency, and the exploitation of
wellexplored 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 HighVoltage Substation:
Revised ToolChecked Version
G. Reggio and V. Filippi.
Technical Report of DISI  Università di Genova,
DISITR9509, Italy, 1995.
Specification of
a Hydroelectric Power Station: Revised ToolChecked Version
G. Reggio and E. Crivelli.
Technical Report of DISI  Università di Genova,
DISITR9417, Italy, 1994.
FormallyDriven Friendly Specifications of Concurrent Systems: A TwoRail Approach
E. Astesiano and
G. Reggio.
Technical Report of DISI  Università di Genova,
DISITR9420, Italy, 1994.
Presented at ICSE'17Workshop on Formal Methods, Seattle April 1995.
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 "tworail 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 formallydriven informal specification (for the nonspecialist
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
G. Reggio, D. Bertello and A. Morgavi.
Technical Report of DISI  Università di Genova,
DISITR9412, Italy, 1994.
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
G. Reggio and F. Parodi.
Technical Report of DISI  Università di Genova,
DISITR9413, Italy, 1994.
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 Internode Communication Architecture
E. Astesiano, F. Mazzanti,
G. Reggio and E. Zucca .
n. 140 of Quaderni Cnet, ETS, Pisa, 1985.
Please send suggestions and comments to:
Gianna Reggio reggio@disi.unige.it
Last Updated: 18/4/2004
