E. Börger, Università di
Pisa
Structuring the JVM architecture
The Java Virtual Machine is analysed to reveal a modular structure of its architecture. The goal is to exhibit orthogonal language, machine and compiler components, which fit together and provide the basis for a stepwise and provably correct design--for--reuse.
First, concise abstract (ASM) code is provided for a fast Java Virtual Machine (JVM), which serves as platform for a general compilation scheme of Java programs to JVM code. This definition, coupled with a corresponding model for Java and a compiler scheme, allow us to prove that any compiler that satisfies some natural conditions compiles legal Java code correctly.
Then the fast JVM is extended to a defensive JVM which can be used as Java independent platform for safely executing byte code. Separating the checking mechanism from the execution we obtain a model for the bytecode verifier which can be proved to be correct and complete. By extending the compiler to a certifying compiler we can prove our compiler to generate code which successfully passes the bytecode verifier.
As last step this bytecode verifier is integrated into a loading machine which together with the executing ASM provides a full JVM model.
These abstract machines for Java, the JVM and the compiler have also been refined to executable machines, which have been validated through experimentation with ASMGofer (available at http://www.tydo.de/AsmGofer/). A full documentation is in the forthcoming book by R. Staerk, J. Schmid, E. Boerger: Java and the Java Virtual Machine: Definition, Verification, Validation. Springer-Verlag (2001), see http://www.inf.ethz.ch/~jbook
We present the process followed by the Firenze team in addressing the case studies proposed inside the project.
The technologies we were interested to apply to the case studies were:
The analysis of the two proposeed cases studied has shown that the technologies referred at item a) were not applicable to the first one, which contained a UML description of a software architecture.
On the other hand, the Klaim language has shown itself suitable for describing the second case study, provided some extensions are made to the language.
We will introduce the language Klaim (both the formal calculus and the programming language), by stating the motivations for this new language and the design choices. We will also present some programming examples and sketch some future works.
M. Bernardo, Università di Torino,
P. Ciancarini, L. Donatiello Università di Bologna
Architecting Software Systems with Process Algebras
In this talk we present the activities conducted by the Bologna-Torino site in the field of software architecture during the first year of Saladin. We start by briefly presenting AEMPA, a process algebra based language for the description of families of software architectures, the detection of their architectural mismatches, and the analysis of their functional and performance properties. We then illustrate the features of AEMPA by means of three case studies:
We present the project activity of integrating quantitative performance
model and software architecture specification. In particular, we present
an approach to evaluating the expected performance of a software
architecture (SA).
The method allows the derivation of a performance evaluation model, based
on a Queueing Network model, from a software architecture formal
specification modeled as a Labeled Transition System (LTS).
The goal of this approach is to provide a set of measures to compare the
performance of two or more competing software architectures, even at
their high level of abstraction. Even in the absence of relevant pieces
of information we want to be able to carry on an evaluation of concurrent
execution of SA, which should allow the validation of the possibly
critical design choices made at the SA level. We aim at deriving
mathematical relations among the parameters characterizing the competing
models. These relations are obtained by using implementation scenarios to
relate the performance indices that can then be suitably evaluated.
Besides assisting in the choice of a software architecture, these
relations give information on how to carry on the development process in
order to maintain the given performance. This suggests the possibility of
developing performance models at the SA design level that can then be
used to derive the performance models related to further development
steps.
Finally, we illustrate the proposed approach for a software description
based on Message Sequence Charts and the algorithm to derive the
corresponding QN model, and the use of finite capacity service centers to
model synchronous communication among concurrent system components.
S. Balsamo, M. Simeoni, Università Ca'
Foscari di Venezia
Using UML diagrams to derive performance models
The derivation of performance models from software architecture specifications has recently become a challenging research issue. The aim is to integrate quantitative analysis into the software development process, since the early stage of the software design. This would allow in fact the derivation or validation of non-functional properties of the system, and the comparison of design alternatives also from the performance viewpoint.
We present and compare some approaches which consider UML as specification language, and propose transformation techniques for obtaining performance models of the specified systems. We aim at describing how the considered approaches make use of the different UML diagrams. From the comparison of the various transformation techniques we make some observations concerning their generality, the constraints on the software system, the set of employed UML diagrams, and the additional information specified in the diagrams.
V. Cortellessa, V. Grassi, Università di Roma "Tor Vergata"
A Performance based Methodology to Early Evaluate the
Effectiveness of Mobile Software Architectures
Modern programming languages and hardware technologies require (and effectively enable) ever more software to be distributed. Different paradigms (client-server, mobility based, etc.) can be adopted to design distributed software, and deciding the "best" paradigm is a typical choice to be made in the very early software design phases. Several factors should drive this choice, that can also change depending on the software application domain. Within this framework, we focus on a class of attributes related to the performance, and the contribute of this paper is twofold: we extend an existing architecture description language (ADL) to model the physical and logical mobility of single components; we introduce a complete methodology that, starting from a software architecture described using this extended notation, generates a performance model (namely a Markov Decision Process) that allows the designer to evaluate the convenience of introducing logical mobility into a software application. The insights gained by adopting our methodology do not consist only in deciding whether a mobile paradigm is effective for the performance improvement of a given application, but also how to use it, that is where a component should move, based on a certain type of performance indices.
M. Loreti, R. Pugliese, Università di Firenze
Dynamically evolving networks in KLAIM
In this talk we will show how to use Klaim to represent dynamical aspects of communication in order to deal with the case study proposed by Politecnico di Milano.
First we will show how to program networks connection and disconnection by using standard Klaim. Afterwards we will introduce some new features for specifying the communication layer more naturally. Finally we will show that these new features can be encoded in standard Klaim.
M. Pighin, Università di Udine
Using IR Techniques Catalogue, Reuse and Maintain Existing SW Objects
The basic idea is to utilize in Software Engineering applications a tool born in Information Retrieval environment (the statistical search engine Z-prise).
The experimentation done up-to-date concerned on code aspects, allowed us to successfully start with a Software System of about 150.000 lines of code, to automatically index it on Z-Prise server, and to build a specialized interface adapted to SW-engineer activities to maintain and reuse software modules.
Indexing was done by a lexical analyzer, which recognized particular keywords related to the particular language (like names of variables, functions, etc.), to the particular methodology used (like interactive dialog, batch elaboration, etc), to the particular application semantic (naming, comment use, etc.) and automatically built the objects with the syntax of Z-Prise.
Starting form a particular specification environment (UML, E-R, etc.), we are now working to produce an analyzer which could interpret the features (syntactic or semantic), with attention of "mobility" features (like Type of Execution, Migration, Remote cloning, etc).
The user interface will have features specialized on these environment. The System will so index the specification and transform them with a format compatible with Z-Prise engine.
The potential results are: