DIPARTIMENTO   DI   INFORMATICA
Università di Torino

Research Report Year 2002

Computer Science

Computer Systems and Networks

  People   Research Activities   Publications   Software Products   Research Grants

Methods and Tools for the Analysis and Development of Performance Oriented Computer Systems

People

People

Last and first name

Position

Email

Balbo Gianfranco

Full Professor

balbo(at)di.unito.it

Donatelli Susanna

Associate Professor (until 1st November)
Full Professor (
from 1st November)

susi(at)di.unito.it

Gaeta Rossano

Associate Professor

rossano(at)di.unito.it

Sereno Matteo

Associate Professor

matteo(at)di.unito.it

Gribaudo Marco

Researcher

marcog(at)di.unito.it

Sproston Jeremy

Research Assistant (until 1st November)
Researcher (
from 1st November)

sproston(at)di.unito.it

Ballarini Paolo

Ph.D. Student

ballarini(at)di.unito.it

Bernardi Simona

Ph.D. Student

bernardi(at)di.unito.it

De Pierro Massimiliano

Ph.D. Student

depierro(at)di.unito.it

 

Research activity in 2002

Petri Nets

Stochastic Petri Nets (SPN), and their extension Generalized Stochastic Petri Nets (GSPN) are a flexible and effective graphical language to describe concurrent and distributed systems.. The resulting model is Markovian if all of the activity durations are exponentially distributed. In this case, traditional solution techniques of Markov chains can be used to obtain performance indices of the system. The size of the resulting Markov chain can seriously affect the possibility of computing the solution on cases of practical interest. To alleviate this problem efficient solution techniques that exploit the net structure have been pursued, in particular we have explored the relations that exist among the existence of the efficient solution technique called "product form" and the structural properties of the SPN and on the identification of a class of GSPN for which the product form solution technique can be applied [1].

Another Petri Net based formalism is the Fluid Stochastic Petri Nets (FSPN). In this formalism, there are two classes of places: discrete places that carry a natural number of distinct objects (tokens), and fluid places that hold a positive amount of fluid, represented by a real number. This formalism allows us to describe models with very complex underlying stochastic behavior. The discretization technique, based on Kronecker algebra, has been used to devise a model checker for FSPN.

Moreover, the basic model of Fluid Stochastic Petri Nets has been extended to include new features like flush-out arcs [10], fluid transfer and fluid jumps. New solution techniques have been devised accordingly, based on matrix geometric [12] techniques and Kronecker algebra.

An important application field for SPN and FSPN is that of telecommunication networks. The researches has focussed on the modelling of IP networks. In particular, SPN models of the TCP transport protocol have been developed for finite data sources; these models allow the computation of packet loss probability, average (as well as distribution) of transfer times. The solution technique is based on a fixed point iteration alternatively solving the sub-model of the IP transmission link and the sub-model of a TCP Reno source [8] as well as on FSPN[9].

In order to assist the construction of complex SPN models two ways are pursued: the use of an high level formalism like Stochastic Well Formed Nets (SWN), and the composition of Petri nets (SPN, GSPN and SWN). Both ways may lead to rather large nets, whose adherence to the system has to be validated. For this reason the GreatSPN tool (the SPN-, GSPN- and SWN-solver of the University of Torino) has been potentiated with model checking capabilities through the export [6] of GreatSPN nets to algebraic nets for the PROD tool. PROD is a tool that has a number of advanced features for model checking CTL temporal logics, and the translator allows to perform CTL model checking on GreatSPN nets. A case study on system evaluation through the GreatSPN-to-PROD translator has been presented in [2].

 

Tools play a very important role in the spreading of our research on solution algorithms for Petri nets. It is also widely accepted that, to adequately model a system, a number of different formalisms may be required or convenient. We are therefore working towards a new generation of modelling tools, based on a common framework that allows to define a common graphical interface for different sorts of formalism, as well as ways to compose models and to exchange results and/or parameters among models. The software Tool we are developing is called DrawNET, and in this last year it has been extended to support object oriented composition of models [7] described using different modelling languages. The DrawNET tool, using XML descriptions, is capable to both describe a modelling language and models expressed in that formalism [16,17]. Works on a new improved graphical user interface have been started, and new integration possibilities with other existing tools have been considered.

Dependability analysis of fault tolerant systems

The activity in this field has been mainly driven by the projects DepAuDE and ISIDE.

A number of fault tolerant mechanisms that have been defined in DepAuDE have been formalized and studied using GSPN and SWN [2,5] from a quantitative and qualitative point of view. Moreover a general framework for studying dependability properties has been defined. Part of the framework relies on the automatic derivation of GSPN and SWN models from UML specifications (in particular from state charts [3] and sequence diagrams [15]), so as to be able to validate and evaluate systems that are specified using UML, as it is indeed the case of the fault tolerant solutions proposed by DepAuDE.

Many formalisms and methodologies for dependability analysis exists in the literature, and it is a major goal of ISIDE to analyze and compare them. The comparison study of ISIDE has been applied to the case study of a turbine digital control [4] that has been modeled using probabilistic techniques of increasing modeling power (Fault Tree, Bayesian Networks, GSPN and SWN).

New version of FSPN have been introduced to model safety systems, by adding some non deterministic features, like non deterministic flow rates over the fluid arcs. FSPN have been used to model advanced production systems like a co-generative power plant[11].

Probabilistic Timed Automata

The task of modelling systems in which notions of time, probability and nondeterminism co-exist has been addressed with the further development of methods for the analysis of probabilistic timed automata, a probabilistic extension of the well-known timed automata model of Alur and Dill. Probabilistic timed automata are oriented towards analysis based on the technique of probabilistic model checking. Two streams of research have been addressed. Firstly, the use of probabilistic timed automata for the modelling of a sub-protocol of the IEEE802.11 standard for Wireless Local Area Networks was considered [14]. In order to facilitate the verification of the protocol, a number of abstraction techniques were employed together with a discrete-time semantics. Prompted by this case study, work has also been carried out on the definition of expected-time and reward-based properties within the framework of the discrete-time semantics of probabilistic timed automata [13]. The second stream of research concerning probabilistic timed automata considered the use of a more-expressive continuous-time semantics in combination with symbolic approaches. Such symbolic approaches represent the state sets computed during analysis in an implicit manner, thus facilitating probabilistic model checking of larger systems.

Symbolic techniques have also been studied in the context of data structures for the implicit representation of (Discrete- and Continuous-Time) Markov chains. Focus has been placed on the use of such data structures, for example Multi-Terminal Binary Decision Diagrams or Matrix Diagrams, in the presence of equivalence relations such as lumpability. Previous studies on the co-existence of equivalence relations and implicit data structures have emphasized the incompatability of the two concepts within the same analysis technique. Preliminary work has been conducted to explore the manner in which the benefits of equivalence relations and data structures can both be exploited during analysis.

2002 Publications:

[1] G. Balbo, S. Bruell, and M. Sereno, "Product Form Solution for Generalized Stochastic Petri Nets", IEEE Transactions on Software Engineering, vol. 28, no. 10, October 2002, pp. 915-932.

[2] P. Ballarini, S. Bernardiand S. Donatelli, Validation and Evaluation of a Software Solution for Fault Tolerant Distributed Synchronization, Proceedings of the International Conference on Dependable Systems & Networks (DSN), Washington, D.C., USA, June 23-26, 2002, pp. 773-782

[3] S. Bernardi, S. Donatelli, J. Merseguer, "From UML Sequence Diagrams and Statecharts to analys able Petri Net models", Proceedings of the 3rd International Workshop on Software and Performance (WOSP), ACM Press, Roma, July 2002, pp. 35-45.

[4] A.Bobbio, E.Ciancamerla, G. Franceschinis, R.Gaeta, M.Minichino, L. Portinale. Methods of increasing modelling power for safety analysis, applied to a turbine digital control system, In Proc. of the 21st International Conference on Computer Safety, Reliabiltiy and Security, SAFECOMP 2002, September 2002, LNCS 2434

[5] V. De Florio, S. Donatelli, G. Dondossola, "Flexible Development of Dependability Services: An Experience Derived from Energy Automation Systems", Proc. of the 9th Annual IEEE International Conference and Workshop on the Engineering of Computer Based Systems (ECBS), IEEE Comp. Soc. Press, Los Alamitos, CA, Lund, Sweden, 8-11 April, 2002.

[6] S. Donatelli and L. Ferro, Validation of GSPN and SWN Models through the PROD Tool", 12th International Conference on Modelling Tools and Techniques for Computer and Communication System Performance Evaluation. (TOOLS 2002), LNCS 2324, London, UK, April 2002, pp.131-140.

[7] G. Franceschinis, M. Gribaudo, M. Iacono, N. Mazzocca and V. Vittorini. Towards an Object based Multi-Formalism, Multi-Solution Modeling Approach, Second Workshop on Modelling of Objects, Components, and Agents, (MOCA2002) Aarhus, DK, August 2002, pp. 47-66

[8] R. Gaeta, M. Gribaudo, M. Sereno. Performance Analysis of TCP Connections for Finite Data Transfer, Workshop dei progetti Planet-IP e Nebula, Courmayeur, Italia, 2002.

[9] R. Gaeta, M. Gribaudo, M. Sereno. Fluid-based Analysis of TCP Flows, Workshop dei progetti Planet-IP e Nebula, Courmayeur, Italia, 2002.

[10] M. Gribaudo, A. Horvath. Fluid Stochastic Petri Nets Augmented with Flush-Out Arcs: A Transient Analysis Technique, IEEE Transaction on Software Engineering, October 2002, Volume 28, Number 10, pp. 944-955

[11] M. Gribaudo, A. Horváth, A. Bobbio, E. Tronci, E. Ciancamerla, and M. Minichino. Model-Checking Based on Fluid Petri Nets for the Temperature Control System of the ICARO Co-generative Plant, 21st International Conference, SAFECOMP 2002, Catania, Italy, LNCS 2434, September 10-13 2002, pp. 273-283

[12] A. Horváth, M. Gribaudo. Matrix Geometric Solution of Fluid Stochastic Petri Nets, Proceedings of the Fourth International Conference on Matrix Analytic Methods in Stochastic Models (MAM 2002), Adelaide, Australia, 14-18 July, World Scientific, pp. 163-182, 2002.

[13] M.Z. Kwiatkowska, G. Norman, R. Segala and J. Sproston. Automatic Verification of Real-time Systems with Discrete Probability Distributions. Theoretical Computer Science 282, pp 101-150, 2002.

[14] M.Z. Kwiatkowska, G. Norman and J. Sproston. Probabilistic Model Checking of the IEEE802.11 Wireless Local Area Network Protocol. Proceedings of the 2nd Joint International Workshop on Process Algebra and Performance Modelling and Probabilistic Methods in Verification (PAPM-PROBMIV 2002), LNCS 2399, pp 169-187. Springer-Verlag, 2002.

[15] J. Merseguer, S. Bernardi, J. Campos, S. Donatelli, "A compositional semantics for UML State Machines aimed at performance evaluation, Proceedings of the 6th International Workshop on Discrete Event Sustems (WODES), IEEE-CS, Zaragoza, Spain, October 2002, pp. 295-302.

[16] V. Vittorini, G. Franceschinis, M. Gribaudo, M. Iacono, N. Mazzocca. DrawNet++: Model Objects to Support Performance Analysis and Simulation of Complex Systems, 12th International Conference on Modelling Tools and Techniques for Computer and Communication System Performance Evaluation. LNCS 2324, London, UK, April 2002, pp. 233-236.

[17] V. Vittorini, G. Franceschinis, M. Gribaudo, M. Iacono, C. Bertoncello. DrawNet++: a Flexible Framework for Building Dependability Models, Tools presentations, Proc. of the International Conference on Dependable Systems and Networks (DSN2002), Washington, USA, June 2002, p.540.

 

 

Department home [Information] [People] [Research] [Ph.D.] [Education] [Library] [Search]
[Bandi/Careers] [HelpDesk] [Administration] [Services] [Hostings] [News and events]

Administrator: wwwadm[at]di.unito.it Last update: May 17, 2018