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

- People

- Research Activities

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. The research in the field of Petri nets of the group has considered four main topics.

Product Form Solution for SPNs
For SPNs, efficient solution techniques that exploit the net structure have been pursued, in particular, the existence of the efficient solution technique called "product form solution" (PFS) has been investigated. In [44] the relation between the existence of the PFS the structural properties of the SPNs has been investigated.

Efficient algorithms for DSPNs
In [19] a new algorithm for the transient solution of a sub-class of Deterministic Stochastic Petri Nets (DSPN) is proposed. The technique can be applied to DSPNs comprising only deterministic and immediate transitions and such that in each tangible marking only one deterministic transition is enabled.

Bounding techniques for Time Interval Petri Nets
We have proposed bounding techniques for the performance assessment of software systems modelled with Time Interval Petri Nets, that is Petri nets in which transition firing delays fall within time intervals [5].

Model-checking SPNs
Model checking is a method in which formally-described properties of a system model are automatically verified. Properties of systems can be described in terms of temporal logic or automata. Recently model-checking methods have also been applied to probabilistic and stochastic systems. In [12], we considered the application of model-checking techniques to SPNs. We developed tools for translating SPN models into the input languages used by the model-checking tools PRISM and ETMCC.

Performance Analysis of Distributed Systems, Peer-to-Peer Applications, and Communication Networks
In this case we studied also the evaluation of distributed applications such as high performance Web applications and peer-to-peer applications. In particular in [22] we proposed a model based evaluation of a routing mechanism based on the use of the Domain Name System (DNS). These mechanism are used in geographically-distributed Web systems. In [21,43,46,47] we developed models for the performance evaluation of file sharing peer-to-peer systems. In [41] we developed an analytical model for the performance evaluation of wireless sensor networks.

Extending the Fault Tree formalism
The Fault Tree is a stochastic model oriented to the Reliability evaluation of systems (Reliability is a particular measure of Dependability). A Fault Tree model represents the failure mode of a system as combinations of basic component failure events. The Fault Tree formalism has been extended in order to increase its modelling power by including new modelling primitives to represent the dynamic behavior of the system, the presence of redundant parts and the presence of repair processes [9, 10, 30]. The analysis methods developed for the new forms of Fault Tree are based on the use of Binary Decision Diagrams [32], Stochastic (Colored) Petri Nets [11, 33].

Activity on the Draw-Net Modelling System
The Draw-Net Modelling System (DMS) is a framework for the definition of formalisms and models. The DMS can be customized by the user to deal with any kind of graph-based model and to be integrated with model solvers. Recently, the DMS was extended to deal with multi-formalism models [35], i. e. models composed by several submodels, each conforming to a certain formalism; in this way, several formalisms (Fault Trees, Petri Nets, Markov Chains, …) are involved in the model at the same time, together with their analysis methods. Each aspect of the system can be modelled by means of the most suitable formalism.

Phase-type distributions
Phase-type (PH) distributions are given by the time to absorption in a Markov chain. The advantage of the application of this distribution is that a model in which all durations are PH distributed is a Markov chain and hence can be analysed by standard techniques developed for Markov chains. In this area one important aim is to develop methods that allow us to approximate a non PH distribution by a PH distribution. One possible approach is to construct a PH whose moments are identical to the moments of the distribution to be approximated. This approach is discussed in [39].

A PH distribution is either discrete time or continuous time. The two classes are similar but have important differences as well. A comparison of the two classes is published in [24].

The Markov chain of a model with PH distributed durations is structured. It is possible to develop analysis techniques that take advantage of the structuredness and hence perform better than general approaches. Such a technique for the computation of steady state measures is given in [40].

Stochastic fluid models
Hybrid systems are systems in which the notion of state is defined in terms of both discrete and continuous variables. Stochastic fluid models can be used to describe stochastic hybrid systems, and can model a wide range of phenomena.

A subclass of fluid models are the reward models where the continuous variables cannot decrease. An analysis technique for inhomogeneous Markov reward models is given in [23].

Recent years have seen the development of model checking procedures for stochastic models. Model checking of general stochastic models however is far from being resolved. A first step in this direction is taken in [20].

Some Dynamic Reliability problems concerning hybrid systems have been considered. We talk about Dynamic Reliability when the Reliability parameters (such as failure rates) are expressed as a function of variables describing the current state of the system. The Dynamic Reliability of several cases of hybrid system has been evaluated by means of Fluid Stochastic Petri Nets [34, 36, 37], a rather recent form of Stochastic Petri Nets, allowing the representation of both discrete and continuous quantities.

Dependability analysis of fault tolerant systems
We have conceived a modelling methodology for the elicitation of the temporal and dependability requirements of distributed automation systems and for the definition and analysis of fault tolerant strategies to be adopted for such systems. Three formalisms are envisaged in the methodology: UML Class Diagrams, TRIO (Tempo Reale ImplicitO) and Stochastic Petri Nets. Class Diagrams support the collection of the system requirements [6]. TRIO supports the formalization and the assessment of the temporal requirements and of the fault tolerance strategies [3]. Stochastic Petri net are instead used for the dependability analysis. Modularity and inheritance principles are used to derive, in a semi-automatic manner, dependability SPN models from UML Class Diagram specification [8].

We have also investigated on the current standard extensions for the UML annotation of non functional requirements of software systems. In this context, a comparative analysis between the two UML profiles (UML Schedulability, Performance and Time profile and UML Quality of Service and Fault Tolerance Mechanism profile) has been carried out in order to emphasize the advantages and the drawbacks of the two approaches [7].

Model checking for probabilistic timed systems
Further methods for model-checking analysis of probabilistic timed automata have been developed. Probabilistic timed automata are a probabilistic extension of the widely-adopted formalism of timed automata, and can model systems in which non-deterministic, probabilistic and timed behavior co-exist. Probabilistic timed automata have been used previously to model leader election and communication protocols. In order to increase the efficiency and applicability of model-checking methods for probabilistic timed automata, we developed a symbolic model-checking technique, in which the portions of the state space are represented using "zones" (a concept exploited in tools for timed automata such as UPPAAL) [26].

We also considered a simple discrete-time model for probabilistic timed systems, called durational probabilistic systems. We presented an algorithm in which the magnitude of the timing constants used in the description of the probabilistic timed system has no impact on the running time of the model-checking analysis [45].

Model checking for Markovian models
We considered the applicability of state equivalences in the context of model-checking analysis of continuous-time Markov chains (CTMCs), which are the underlying model of high-level modelling formalisms such as stochastic Petri nets and stochastic process algebras. A state equivalence can be used to identify systems states which have the same future behavior; this can be useful in analysis, because equivalent states can be aggregated into a single state, and therefore the size of the CTMC considered can be reduced. We considered backward stochastic bisimulation [27], a variant of bisimulation in which considers principally the incoming transitions of a states, rather than the outgoing transitions, which is the case for traditional bisimulation.

On the negative side, we showed that backward stochastic bisimilar states do not satisfy the same formulae of Continuous Stochastic Logic, a well-known temporal logic for the specification of properties of CTMCs. However, we also showed that analysis can nevertheless be carried out for a practically significant class of properties, and, in particular, can result in potentially large gains in the case of steady-state properties.

- Publications