Pisa - Dipartimento di Informatica - Research Evaluation Exercise 1999
Vincenzo Ambriola, Egon Börger, Carlo Montangero
Università di Pisa, Dipartimento di Informatica
Corso Italia 40, I-56125 Pisa, Italy
Nowadays, the major problems of software engineering are encountered
at the high levels of system development, both scientifically and in
the industrial practice. The modern software life-cycle models
recognize that defects injected in the initial software development
phases are the most expensive ones. A related experience is
encountered in the hardware-software co-design area where it
has been recognized recently that the CAD process of complex systems
has to begin at an early abstract stage, before the partitioning
into hardware-software components .
Besides, there is a simultaneous need
for heterogeneity, to capture the richness of different
application domains, and for a uniform approach which unfolds the
commonalties across domains and makes them available for analysis,
validation and verification.
Current approaches to prevent errors early in the life-cycle include
multiple high-level views of the system, to facilitate understanding by
all stakeholders, domain specific architectures, to factorize common
facets of product lines, and executable architectures, to get
early feed-back on major design decisions.
A notable example of emerging consensus on multiple views and levels
of abstraction is the software architecture hierarchy proposed in
: the conceptual architectural level deals with
the major design elements of a system, largely determined by
application domain structures. The module interconnection level
exhibits the (horizontal) functional decomposition of the system and
the (vertical) partitioning of functional components into layers. The
execution architecture introduces the run-time system structure,
allocating functional components to run-time elements and handling
their communication and synchronization. The code architecture
level deals with the organization of the source code.
The early phases in software development are characterized by a)
capturing the problem requirements reliably and in rigorous form, b)
representing the basic architectural decisions taken to compose the
system out of interacting components, and c) linking, in transparent
and reliable ways, the abstract
models to more detailed ones,
paving the way to implementation.
To foster error prevention in the up-stream modeling activities,
current research looks
for reliable techniques to turn the informally presented requirements of
the desired system into a
functionally complete but abstract system description
which a) can be read and understood
by and justified to the customer as solving his problem, b) defines
every system feature as far as this is semantically relevant for the
work the user expects the system to achieve, c) contains only what the
logic of the problem requires for the system behavior, i.e. does not
rely upon any further design decision belonging to the system
implementation. Models with these characteristics have been called
ground models , and we will use this term in this
The research presented here intends to contribute to the current trend
towards software development methods centered on ground models. It is
important to guarantee two capabilities: a) to relate requirements
capture and architectural decomposition reliably, and b) to transform
the abstract models by controllable refinements down to a level where
an implementation can be built by well-established design methods. We
are interested in practical methods that can be used for
rigorous high-level system development also under industrial
constraints. We consider our work as a contribution to the emerging ``science
of [software] construction principles'', which, together with domain sciences and engineering processes has been recently identified as one of the basis of the Software Discipline .
The proponents have an expertise in requirements engineering
[3,4], software process (in particular refinement
for software process modeling) [2,20,18],
software architecture [1,5,19,21,22],
high-level modeling and analysis of systems (control software
[11,13], instruction set architectures
[9,12,10], programming languages implementations
[6,8,14,15,16], and hardware design
The proponents are involved in several research projects: ESPRIT WG
21185 PROMOTER.2 on Software Process Technology (1996-2000), ESPRIT WG
24512 COORDINA on Coordination Models and Applications (1997-2000),
ESPRIT Network of Excellence 20800 RENOIR on Requirements Engineering
(1998 - 2001), FALKO project on the high-level specification and
implementation of a train simulation and planning system (Siemens
Corporate Research, 1997-1999), ASM project (Microsoft Research,
Foundations of Software Engineering Group, 1999-2001), Java/JVM
project (University of Ulm, ETH Zürich, Siemens Corporate Research
We aim at providing system models that can be the subject
of high-level analysis (both verification and validation) and to which
a detailed design process can be applied leading through controllable
transformations (refinements) to executable code. We will concentrate
our attention on system (de-)composition. As an intended result, we want
to support the reuse of architectural patterns. This is crucial, given
that in the future only very few systems (if any) will be designed from
scratch. We will focus on the conceptual (semantical) facets of system
(de-)composition, so that they can be mapped to widespread particular
notations (like UML) and their tool support.
For the next two years the research will address methods to develop,
analyze and refine high-level models of control intensive software
systems. We want to concentrate upon three themes: a) capturing
requirements and expressing them in ground models which are well suited
for further system
design, b) finding paradigmatic architectural models --ground model
templates-- which allow one to make different system views
explicit, and c) refining the ground models and their architectural
structure into specific architectures and code design.
Requirements Capture. One concrete requirement capture method we
want to investigate consists in mechanically extracting the knowledge
from requirements documents in the form of collections of unambiguous
atomic statements. These ``atoms'', given a specific modeling
framework (like FSMs, temporal logics, etc.), are interpreted to
generate various system models. We want these
interpretations to be done by application domain aware software agents
(``modelers''), to produce models
that can be visualized, and analyzed in terms of completeness,
consistency and fundamental architectural constraints. The crucial
concern is to come up with a trustworthy basis for the further
detailed design process, in a joint effort by experts in the
application domain on one side and in system design on the other.
In the framework of ASMs (Abstract State Machines in the sense of
Gurevich ) the models are expressed by first-order
statements and transition rules. We will investigate
the usefulness of the machine character of ASMs for early validation and
simulation of requirements, when they are given by
use cases. Indeed, use cases can be directly expressed by computation
segments of the ground model.
We also plan to relate the ground model concept to the
conceptual software architecture level proposed in
Paradigmatic Architectural Models. We intend to define a
collection of ground model templates which capture
paradigmatic architectural composition principles and allow one
to make different basic system views explicit, in particular in
terms of static system properties, user interfaces, communication
mechanisms and notions of time.
We expect two concrete short-term results of conceptual nature:
characterizations and formalizations of the best known
architectural styles in the logic Oikos-adtl
[19,21], and the definition of frequently used ASM
composition principles (forms of submachine, conservative extension,
lifting). We will validate these concepts through experiments with
software developments appearing in the literature and through a
requirements capture case study for realistic non-toy control
We will test the practicality of the ASM structuring
principles also by applying them for a complete but succinct high-level
architectural definition of the Java Virtual Machine out of its major
components (for loading, linking, bytecode verification and
execution). We intend to use this definition for analyzing and
comparing different implementations of the machine, in terms of
software security and correctness (type correctness, correctness of
compilation of Java like languages, etc.).
Refinement. We will use refinement methods to link ground models
and their architectural structure to a hierarchy of specific
architectures and code designs which are ready for being transformed, by
known methods, to an implementation. As an aside, we obtain a well
documented and easy to inspect set of intermediate design steps.
We have two short-term goals. One consists in identifying, as
standard refinement steps, the mappings of the conceptual architecture
level to the module interconnection, the execution architecture and
the code architecture levels. The other is to develop formal
architectural refinement techniques where verification occurs not a
posteriori but by construction.
For each of the themes above, the analysis and in particular the
validation aspects include quality analysis. The quality analysis will
be pursued along two classical points of view. We will measure the quality
the software product, in term of parametric
quality models (ISO 9126). On another side, we will measure the software
development process by projecting the product measures along the
development time and investigating the emerging patterns. Some
preliminary quantitative results obtained so far indicate that
significant and recurring schemes show up in the time
We plan to link the proposed concepts and results to existing
component based software development and analysis environments and in
particular to their tool support. We will try to enhance these
environments by integrating the proposed high-level abstract design
concepts which incorporate most general abstraction, decomposition and
refinement mechanisms. The rigorous albeit versatile character of our
models will allow us to combine the simplicity of the modeling
activity with the well known advantages that precision yields for
correctness and tool support.
For requirements engineering the long term goal is to provide an
environment for writing and validating requirements, guided by an
explicitly defined process, and for early
prototyping through high-level simulation of ground models. The three major
activities we want to pursue are semantic modeling, information extraction
and process guidance for requirements writing.
In all these activities the software
architecture schemes will be treated as parameters.
The cooperation with and integration into other software development
tools and environments will be realized upon the basis of emerging
We intend to extend Oikos-adtl to mobile components. The goal
of mobility will be reached along two orthogonal lines, one dealing
with security and the other with dynamic creation of components.
Security entails the formalization of the guardians, i.e. components
which are in charge of controlling access to a site, and of authorizing
movement to other sites. Dynamism may need higher order logics, but we
will first explore limited forms that might be accommodated in our first
We will investigate the links, which are necessary to
exploit existing FSM synthesis tools for synthesizing ASMs. We also
plan to use the ASM approach to study the role different computation
models have for software architectures (sequential versus distributed
computation, forms of interaction, in particular different
communication models). We also want to better understand the trade-off
between the uniformity and thus generality of the resulting approach
on the one side, and on the other side the advantages gained by
tailoring the development technique to specific domains, capturing the
peculiarities of the different applications domains. Examples are
(tele-)communication systems, hybrid and/or embedded control systems,
image and signal processing systems. They typically differ with
respect to the main system characteristics, like size,
throughput, fault-tolerance and real-time, distributed,
multi-processing, safety-critical concerns.
In order to figure out whether the methods scale up, as we expect, we
also plan to apply them to larger case studies, possibly with
Vincenzo Ambriola is associate professor of Software Engineering at
the Department of Informatics of the University of Pisa since 1992.
Vice-Rector for the University Computing Services. Chairman of CEPIS
Software Engineering Special Interest Network. Member of the Steering
Committee of ESEC. Director of the national section of CINI on
Sistemi di produzione del software e servizi. Coordinator of the
subproject Protagora (strategic project CNR). PC member of numerous
international conferences. Co-author of two books and over 40 research
papers. Reviewer of numerous international journals (IEEE TSE, ACM
TOSEM, IEEE Software and others).
Egon Börger is full professor of CS in Pisa since November
1985. Previously lecturer/professor at the Universities of Salerno (I
1972-1976), Münster (D 1976-1978), Dortmund (D 1978-1985), Udine (I
1982/83). Offer of a chair in CS/Udine declined 1983, in
Math. Logic/Bonn 1985, in Theoretical CS/Stuttgart 1988, in CS/Bonn
1997. Guest Researcher at IBM Scientific Center Heidelberg/D
(1989/1990), Dept of EECS University of Michigan at Ann Arbor/USA
(March-April 1991), Fachbereich Informatik University of Paderborn/D
(May-July 1993, Sept 1995), CIS Universität München/D (May 1994),
IIG Universität Freiburg/D (Sept 1994), BRICS University of
Aarhus/DK (Aug 1995), DIMACS Rutgers University in New Jersey/USA
(Oct-Nov 1995), Siemens AG Corporate Research and Development
München/D (Jan-Aug 1996), Software Technology Dept. of GMD FIRST
Berlin/D (Sept-Oct 1996), IRIN Nantes/F (April-May 1998). (Co-)Author
of three books and of over 80 research papers, editor of 15 books and
organizer of over 20 international conferences, workshops, schools in
logic and CS.
Carlo Montangero is full professor of Programming at the Department of
Informatics, University of Pisa since 1982. There he chaired the
Scientific Committee for the Mathematical Sciences (including
Informatics), and the Undergraduate Curriculum in Computer Science.
Currently vice-director of the Department.
Co-ordinator of the sub-program on Methods and Tools for the Design of
Software Systems in the special program ``Sistemi Informatici e Calcolo
Parallelo'' of the Italian National Research Council (CNR).
Guest researcher at Datalogilaboriet Uppsala/S, A.I. Lab. Stanford/USA,
CS Dept. City University London/UK.
on the Steering Committee of the European Workshops on
Software Process, and
served on the PC of several workshops and conferences,
including ICSE and ESEC. (Co-)Author of 2 books and of over 50 research
papers, editor of 2 books, he regularly reviews for major journals,
including IEEE TSE and ACM
TOSEM, and many
Vincenzo Gervasi (U. of Pisa), Yuri Gurevich (Microsoft
Research, Redmond), Paola Inverardi (U. of L'Aquila), Peter Paeppinghaus
(Siemens Corporate Research,
München), Elvinia Riccobene (U. of Catania), Joachim Schmid
(Siemens Corporate Research, München),
Wolfram Schulte (Microsoft Research, Redmond), Laura Semini (U. of
Florence), Dilip Soni (Siemens
Corporate Research, Princeton), Robert Staerk (ETH Zürich).
Keywords. Software Engineering, Requirements Capture, Software
Architecture, Formal Methods, Refinement.
- Ambriola, V., Ciancarini, P. and A. Corradini.
Declarative Specification of the Architecture of a Software
Development Environment. Software Practice and Experience, 25:2,
- Ambriola, V., Conradi, R. and A. Fuggetta. Assessing
Process-centered Software Engineering Environment. ACM
Transactions on Software Engineering and Methodology, 6:3, 1997,
- Ambriola, V. and V. Gervasi. An Environment for
Cooperative Construction of Requirement Bases. Proc. 8th
Int. Conf. on Software Engineering Environments,
Cottbus, 1997. IEEE Computer Society Press, Los Alamitos,
- Ambriola, V. and V. Gervasi. Processing Natural
Language Requirements. Proc. 12th Int. Conf.
on Automated Software Engineering, Lake Tahoe, 1997. IEEE
Computer Society Press, Los Alamitos, 36-45.
- Ambriola, V. and V. Gervasi. Representing
Structural Requirements in Software Architecture, Proc. of the
Int. Conf. on Systems Implementation 2000: Languages,
Methods and Tools, Berlin, 1998. Chapman and Hall, London,
- Börger, E. and D. Rosenzweig. A Mathematical
of Full Prolog. Science of Computer Programming 24, 1995,
- Börger, E., Glässer, U. and W. Müller.
Formal Definition of an Abstract VHDL'93 Simulator by EA-Machines.
C. Delgado Kloos and P. T. Breuer (Eds.) Formal Semantics
for VHDL. Kluwer Academic Publishers, 1995, 107-139.
- Börger, E. and D. Rosenzweig.
The WAM - Definition and Compiler Correctness.
C. Beierle and L.Plümer (Eds.) Logic Programming: Formal Methods
Applications. Elsevier Science
B.V./North-Holland, 1995, 20-90 (chapter 2).
- Börger, E. and G. Del Castillo.
A formal method for provably correct composition of a
real-life processor out of basic components (The APE100 reverse
engineering project). Proc. First IEEE Int. Conf. on Engineering of
Complex Computer Systems (ICECCS'95). IEEE Computer Society Press,
Los Alamitos, 1995, 145-148.
- Börger, E. and I. Durdanovic.
Correctness of Compiling Occam to Transputer Code. The Computer
Journal 39:1, 1996, 52-92.
- Beierle, C., Börger, E., Durdanovic, I.,
Glässer U. and E. Riccobene E. Refining abstract machine
specifications of the
steam boiler control to well documented executable code.
J.-R. Abrial, E.Börger, H. Langmaack (Eds.) Formal Methods for
Industrial Applications. Specifying and Programming the Steam-Boiler
Control. Springer LNCS 1165, 1996,
- Börger, E. and S. Mazzanti.
A Practical Method for Rigorously Controllable Hardware Design. Bowen,
J.P., Hinchey, M.G., Till, D. (Eds.) ZUM'97: The Z Formal
Specification Notation. Springer LNCS 1212, 1997, 151-187.
- Börger, E. and L. Mearelli.
Integrating ASMs into the Software Development Life Cycle.
Journal of Universal Computer Science 3:5, Special ASM Issue,
- Börger, E. and W. Schulte.
Programmer friendly modular definition of the semantics of Java.
Jim Alves-Foss (Ed.) Formal Syntax and Semantics of Java.
Springer LNCS 1523, 1999, 353-404.
- Börger, E. and W. Schulte. Defining the Java
Virtual Machine as Platform for Provably
Correct Java Compilation.
L. Brim, J. Gruska, J. Zlatuska (Eds.) Proc. MFCS'98.
Springer LNCS 1450, 1998, 17-35.
- Börger, E. and W. Schulte.
Modular Design for the Java VM architecture. Architecture Design
and Validation Methods. Springer Verlag 1999.
- Börger, E. High Level System Design and Analysis
using Abstract State Machines. Hutter, D., Stephan, W., Traverso, P.,
Ullmann, M. (Eds.) Current Trends in Applied Formal Methods
98. Springer LNCS, 1999.
- Montangero, C. and L. Semini. Applying Refinement
Calculi to Software Process Modeling. In W. Schäfer (Ed.) Proc.
Conf. on the Software Process ICSP4, Brighton, 1996.
IEEE Computer Society Press, Los Alamitos, 63-74.
- Montangero, C. and L. Semini. Refining by
architectural style or Architecting by refinements. L.
Vidal and A. L. Wolf (Eds.) 2nd ACM SIGSOFT Int. Software
Architecture Workshop. S. Francisco, 1996. ACM Press, 76-79.
- Emmerich, W., Finkelstein, A., Montangero, C.,
Antonelli, S., Armitage, S. and R. Stevens. Managing Standards
Compliance. IEEE Transactions on Software
Engineering, 1999. To appear.
- Montangero, C. and L. Semini. Composing specifications
for coordination. P. Ciancarini and
A. Wolf (Eds) Proc. Coordination '99, Amsterdam, 1999. Springer
LNCS 1594, 118-133.
- Semini, L. and C. Montangero. A Refinement Calculus for
Tuple Spaces. Science of Computer Programming, 34,2, May 1999,
- Gurevich, Y. Evolving Algebra 1993:
Lipari Guide. Börger, E. (Ed) Specification
and Validation Methods. Oxford University Press, 1995, 9-36.
- Hofmeister, C., Nord, R., and D. Soni. Applied
Software Architecture, 1999. To appear.
- Lavagno, L., Sangiovanni-Vincentelli, A. and E.M.
Sentovich. Models of Computation for System Design. Börger, E. (Ed)
Architecture Design and Validation Methods.
Springer, 1999. To appear.
- V. R. Basili et al. NSF Workshop on a Software Research Program for the 21st Century. Software Engineering Notes 24, 3, May 99, 37-44.