Research activity in 2001
1) Petri Nets
Stochastic Petri Nets (SPN) are a flexible and effective graphical language to describe the system under study. 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. In this field we have focused on the relations that exist among the existence of efficient solution technique called product form solution and the structural properties of the SPN and on the identification of a class of GSPNs for which the product form solution technique can be applied.
In several cases although, the assumption that all durations are exponentially distributed results in inaccurate modeling. The class of Stochastic Petri Nets in which any general firing time can be assigned to activities is referred to as Non-Markovian Stochastic Petri Nets (NMSPN). A question raised by NMSPN is the treatment of preempted activities. The modeler has to decide what happens if an activity (for example a job) modeled by a transition is preempted. This decision is taken through associating a preemption policy to each transition. Different policies result in different underlying stochastic behaviour which can be described by a set of differential equations and the differential equations have been solved by discretization.
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 behaviour. We have shown how, as for NMSPNs, the differential equations that describe the stochastic behaviour can be derived automatically from the model. The resulting differential equations, however, can be very hard to solve and we have proposed a discretization technique, based on Kronecker-algebra, to obtain results for a special class of FSPNs.
Moreover, the basic model of Fluid Stochastic Petri Nets has been extended adding a new primitive called flush-outs. Equations for this new formalism have been derived. The proposed formalism has been used to analyse communication protocols. In particular the fluid formalism has been used for computing performance measures of communication networks offering General Packet Radio Service (GPRS).
A way to model non-exponential durations within the framework of Markovian models is to apply Phase-type (PH) distributions. PH distributions are given by distribution of time to absorption in discrete- or continuous-time Markov-chains. In our work we have proposed a construct, PH timing, to unify stochastic and non-stochastic analysis of Petri Nets. With this technique, activity durations can be given either by PH distributions (for stochastic analysis) or by an interval from which the firing time is non-deterministically (but not stochastically) chosen. We have also shown how to model check Petri Nets with PH timing.
In order to assist the construction of complex SPN models, automatic program tools are developed. A class of stochastic Petri Nets are the Stochastic Well Formed Petri Nets (SWN). The result of the activity connected to SWNs was to define and implement a compositional algebra that gives the possibility to build models of real systems in an efficient compositional manner. The tool called algebra is integrated into the existing Petri Net package GreatSPN. Compositional construction can lead to very large models that may have undesired behaviours, we have therefore constructed a bridge between the GreatSPN tool for SWN and the PROD tool for algebraic nets. 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.
Moreover the application of the theoretical results to real case studies requires the possibility to define set of experiments and the organization of the experiment results in an easy manner: this need has been addressed by the tool Multisolve that allows to plan experiments using various Petri net solvers for a number of varying parameters.
2) Rejuvenation of Software System
In this case we address the problem of preventive maintenance of operational software systems, an approach recently proposed to counteract the phenomenon of software aging. Software rejuvenation consists in periodically stopping the software system and then restarting it in a robust state after a proper maintenance, and we propose a methodology for the quantitative analysis of rejuvenation strategies. The methodology is based on a fine grained model that assumes that it is possible to identify the current degradation level of the system by monitoring an observable quantity, so that the rejuvenation strategy can be tuned on the measured degradation. The methodology is demonstrated by applying it to a real-world case study, arising in the area of database maintenance for data archiving.
3) 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 SWNs from a quantitative and qualitative point of view. Moreover a general framework for studying dependability properties has been defined. An activity has been started on the automatic derivation of SWN models from UML specifications (state charts and sequence diagrams), 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. A study of a Programmable Logic Controller (PLC) has been conducted using several methodologies, according to the requirements of IEC 61508: different probabilistic techniques of increasing modeling power (Fault Tree (FT), Bayesian Networks (BN), Generalized Stochastic Petri Nets (GSPN) and coloured SPN) have been compared. Furthermore, an accurate dependability assessment of the PLC has been developed using the Parametric Fault Tree formalism.
4) Stochastic Process Algebras
In the field of Markovian process algebras we have reconsidered a technique we proposed some years ago to specify performance measures by attaching yield and bonus rewards to process algebra actions.
In particular, we have reworked the notion of reward Markovian bisimulation congruence in such a way that more terms are now equated. This has been achieved by taking into account the interplay between action execution probabilities, yield rewards, and bonus rewards.
Moreover the comparison between Stochastic Process Algebra and Stochastic Well-formed Nets has be continued with the aim of importing, when possible, the characteristics of one formalism into the other.
An important application area for Stochastic Process Algebra is that of software architecture. In this field we have improved our previous proposal of a process algebra based architectural description language by introducing an architectural compatibility check (for acyclic topologies) and an architectural interoperability check (for cyclic topologies) that provide some sufficient conditions for obtaining a deadlock free architecture starting from deadlock free components. Both checks are based on observational behavioural equivalencies and preserved by the architectural conformity check, i.e. every member of an architectural type possesses the same compatibility and interoperability properties.
The process algebra based architectural description language has been employed in the following case studies:
- Detection of architectural mismatches in a compressing proxy system.
- Detection of architectural mismatches in a cruise control system.
- Comparison of the performance of different server selection algorithms for replicated web services.
5) Telecommunications
The research activity has focused on the modeling and analysis of telecommunication networks and on the definition of appropriate stochastic models for the IP traffic.
In particular, an accurate new approximate analytical technique for the performance analysis of cell-based switch architectures has been developed; it is based on the separate study of two parts of the switch: the internal switching fabric, and the buffers associated with the output line interfaces. The study of the first part, subjected to the switch input traffic, allows the probabilistic characterization of the cell flows at the ingress of the output buffers. This in turn permits the study of the second part separately considering each output buffer subjected to an input cell flow generated by a synthetic source that tries to mimic the characteristics of the true cell flow entering the output buffer under investigation.
Traffic measurement studies on real high speed networks carrying data packets of various applications show high variability and burstiness of the traffic process over several time scales. Several models are considered in the literature to capture these characteristics: fractional Gaussian noises, traditional and fractional ARIMA processes, fractals and multi-fractals. These models are analytically hardly tractable and often computationally expensive. The analytical tractability of Markovian models initiated a research effort to approximate real traffic behaviour with Markovian models. Connected to the project Planet-IP, in this line of research we have investigated the possibility of constructing Markovian arrival processes that exhibit multi-fractal behaviour over a number of time scales and we have studied the applicability of these Markovian models to approximate real-traffic
2001 Publications
M. Ajmone, M. Marsan, M. Gribaudo, Meo and M. Sereno. Performance Analysis of Data Services over GPRS. International Conference On High Performance Computing. LNCS Volume 2228, 11-14 September, 2001, pp. 424-444.
A. Aldini, M. Bernardo, R. Gorrieri, M. Roccetti. Comparing the QoS of Internet Audio Mechanisms via Formal Methods, ACM Trans. on Modeling and Computer Simulation, January, 2001, Vol. 11, pp. 1-42
G. Balbo. Introduction to Stochastic Petri Nets. Formal Methods and Performance Analysis LNCS 2090, 2001, May, Springer-Verlag, Berlin, Germany, E. Brinksma AND H. Hermanns AND J.-P. Katoen eds, pp. 84-155.
G. Balbo, Bruell and M. Sereno. Embedded Processes in Generalized Stochastic Petri Nets, Proc. 9th Intern. Workshop on Petri Nets and Performance Models, 2001, 11-14 September, IEEE-CS Press, Aachen, Germany, pp. 71-80.
S. Bernardi and G. Balbo. Concurrent Generalized Petri Nets: Regenerative Conditions, Proc. 9th Intern. Workshop on Petri Nets and Performance Models, 2001, 11-14 September, IEEE-CS Press, Aachen, Germany, pp. 125-134.
S. Bernardi, C. Bertoncello, S. Donatelli, G. Franceschinis, R. Gaeta, M. Gribaudo, and A. Horváth. GreatSPN in the new millenium. In Tool Session of 9th Intern. Workshop on Petri Nets and Performance Models, Aachen, Germany, 2001, 11-14 September.
S. Bernardi e S. Donatelli, Performance validation of fault-tolerance software: a compositional approach, Proceedings of the International conference on dependable systems and networks DSN2001, Goteborg, Sweden, 1-4 July 2001, IEEE-CS edition, pp. 379-388.
S. Bernardi, S. Donatelli, and A. Horváth. Special session on the practical use of high-level Petri Nets: Implementing compositionality for stochastic petri nets. International Journal on Software Tools for Technology Transfer (STTT), 3(4), pp. 417-430, 2001.
M. Bernardo, M. Bravetti. Reward Based Congruences: Can We Aggregate More?, in Proc. of Joint International Workshop on Process Algebra and Performance Modeling and Probabilistic Methods in Verification PAPM/PROBMIV 01, Lecture Notes in Computer Science Vol. 2165, Aachen, Germany, 2001, 11-14 September 2001, pp. 136-151.
M. Bernardo, P. Ciancarini, L. Donatiello. Detecting Architectural Mismatches in Process Algebraic Descriptions of Software Systems, 2nd Working IEEE/IFIP Conf. on Software Architecture (WICSA 2001), August 2001, Amsterdam, The Netherlands, IEEE-CS Press, pp. 77-86.
M. Bernardo. A Simulation Analysis of Dynamic Server Selection Algorithms for Replicated Web Services, 9th Int. Symp. on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS 2001), August 2001, Cincinnati (OH), USA, IEEE-CS Press, pp. 371-378.
A. Bobbio and A. Horváth. Petri nets with discrete phase type timing: A bridge between stochastic and functional analysis. In Proc. of 2nd Workshop on Models for Time-Critical Systems, vol.52, No. 3 of Electronic Notes in Theoretical Computer Science, Aalborg, Denmark, Aug. 2001.
A. Bobbio and A. Horváth. Model checking time petri nets using NuSMV. In Proc. of the 5th International Workshop on Performability Modeling of Computer and Communication System, Erlangen, Germany, Sep. 2001.
A. Bobbio, M. Sereno and C. Anglano. Fine Grained Software Degradation Models for Optimal Rejuvenation Policies, Performance Evaluation, September 2001, Vol 46 n.1, pp. 45-62.
S. Donatelli, "Petri nets and Kronecker algebra: is it worth the effort?", invited talk and paper at Proc. 22nd International conference on application and theory of Petri nets LNCS 2075, New Castle, UK, June 2001, pp. 1-18, Springer-Verlag, M. Koutny and J.M. Colom Editors.
S. Donatelli e P. Kemper. "Integrating Synchronization with Priority into a Kronecker Representation", Performance Evaluation, 44 (2001), pp. 73-96, North Holland Elsevier, B. Haverkort Editor (special issue of the 11th International conference TOOLS2000).
R. Gaeta, M.Ajmone Marsan and M. Meo. Accurate approximate analysis of cell-based switch architectures, PERFORMANCE EVALUATION, 2001, May, vol. 45, n. 1, pp. 33-56.
R. Gaeta, A.Bobbio, G.Franceschinis and L.Portinale. Dependability assessment of an industrial programmable logic controller via Parametric Fault-tree and High-Level Petri Nets, PNPM - INT. WORKSHOP ON PETRI NETS AND PERFORMANCE MODELS, 2001, 11-14 September, Aachen, Germany, IEEE-CS Press, pp. 29-38.
R. Gaeta, S. Bologna, E. Ciancamerla, M. Minichino, A. Bobbio, G. Franceschinis and L. Portinale.Comparison of methodologies for the safety and dependability assessment of an industrial programmable logic controller, ESREL International Conference, Politecnico di Torino, 16-20 September 2001, Turin, Italy, pp. 411-418.
S. Gilmore, M. Ribaudo. An Efficient Algorithm for Aggregating PEPA Models. IEEE Transactions On Software Engineering, May 2001, Vol. 27, pp. 449-464.
S. Gilmore, J. Hillston and M. Ribaudo. PEPA-coloured stochastic Petri nets, 17th UK Performance Engineering Workshop, July 2001, Leeds, UK, University of Leeds.
A. Horváth and M. Telek. Time domain analysis of NMSPNs with PRI transitions. In Proc. of 9th Intern. Workshop on Petri Nets and Performance Models, Aachen, Germany, Sep 2001. IEEE-CS Press.
M. Gribaudo, A Bobbio and M. Sereno. Modeling Physical Quantities in Industrial Systems using Fluid Stochastic Petri Nets. Modeling Physical Quantities in Industrial Systems using Fluid Stochastic Petri Nets, September 2001, Erlangen, Germany, pp. 81-85.
M. Gribaudo and R. German. Numerical Analysis of Bounded Fluid Models using Matrix Exponentiation. Proceeding of Eleventh GI/ITG Conference on Measuring, Modeling and Evaluation of Computer and Communication Systems, MMB'01, September 2001, Aachen, Germany, Springer-Verlag, pp.41-57.
M. Gribaudo, M. Sereno, A. Horváth and A. Bobbio. Fluid Stochastic Petri Nets Augmented with Flush-out Arcs: Modelling and Analysis' Discrete Event Dynamic Systems, 2001, Vol. 11, n. 1-2, pp. 97-117.
M. Gribaudo and A. Horváth. Fluid stochastic petri nets augmented with flush-out arcs: A transient analysis technique. In Proc. of 9th Intern. Workshop on Petri Nets and Performance Models, Aachen, Germany, Sep 2001. IEEE-CS Press.
M. Gribaudo and D. Sessi. A multiparadigm simulation framework. International Conference on Parallel and Distributed Processing Techniques and Applications, June 2001, Las Vegas, USA, pp. 1647-1653.
S. Haddad, P. Moreaux, M. Sereno and M. Silva. Structural characterization and qualitative properties of Product Form Stochastic Petri Nets, 22th Intern. Conf. on Appl. and Theory of Petri nets. LNCS 2075, 2001, pp. 164-183.
J. Hillston, L. Recalde, M. Silva and M. Ribaudo. A Comparison of the Expressiveness of SPA and Bounded SPN models. 9th International Workshop on Petri Nets and Performance Models, September 2001, Aachen, Germany, IEEE Computer Society, pp. 197-206.
M. Kwiatkowska, G. Norman and J. Sproston. Symbolic Computation of Maximal Probabilistic Reachability, CONCUR, 2001, Aalborg, Danimarca, Springer-Verlag, pp.169-183
M. Kwiatkowska, G. Norman J. and Sproston. Probabilistic Model Checking of Deadline Properties in the IEEE1394 FireWire Root Contention Protocol, International Workshop on Application of Formal Methods to IEEE 1394 Standard, 2001 Berlino, Germania, University of Stirling.
M. Telek and A. Horváth. Transient analysis of age-MRSPNs by the method supplementary variables. Performance Evaluation, 45(4), pp. 205-221, 2001.
