Pisa - Dipartimento di Informatica - Research Evaluation Exercise 1999

Rigorous Methods
for Requirements Capture
and Software Architecture

Vincenzo Ambriola, Egon Börger, Carlo Montangero
Università di Pisa, Dipartimento di Informatica
Corso Italia 40, I-56125 Pisa, Italy
$\{$% WIDTH=14 HEIGHT=37 vambriola,eboerger,cmontangero$\}$% WIDTH=14 HEIGHT=37 @di.unipi.it

State of the Art and Trends

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 [25]. 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 [24]: 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 [17], and we will use this term in this document. 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 [26].

Relevant Research Activities

The proponents have an expertise in requirements engineering [3,4], software process (in particular refinement calculi for software process modeling) [2,20,18], software architecture [1,5,19,21,22], and 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 languages [7]). 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 2000-2001).

Short Term Plans and Expected Results

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 [23]) 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 [24].

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 software. 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 attributes of 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 diagrams.

Long Term Scenarios

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 standards. 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 order setting. 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 industrial participation.

Short CV's

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. He is 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 conferences.


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, 1995, 143-174.

Ambriola, V., Conradi, R. and A. Fuggetta. Assessing Process-centered Software Engineering Environment. ACM Transactions on Software Engineering and Methodology, 6:3, 1997, 283-328.

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, 124-130.

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, 114-127.

Börger, E. and D. Rosenzweig. A Mathematical Definition of Full Prolog. Science of Computer Programming 24, 1995, 249-286.

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 and Practical 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, 52-78.

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, 1997, 603-665.

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 FM-Trends 98. Springer LNCS, 1999.

Montangero, C. and L. Semini. Applying Refinement Calculi to Software Process Modeling. In W. Schäfer (Ed.) Proc. 4th Int. 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, 79-140.

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.

Index Page