The project consists of applying stochastic modelling techniques to the KDC model that is obtained as a variation of the one presented in the article. More specifically, the work is organized as follows:
- Short introduction containing an informal, but careful, explanation of the problem which we wish to model;
- Identification of the components of interest and the activities which they undertake either individually or in co-operation;
- Description of these components behaviourally, explaining how they interact with each other;
- High-level description of each component in the PEPA stochastic process algebra;
- Specification of the entire system in the PEPA process algebra as the co-operation of the above components;
- Drawing of the derivation graph of the model (or part of it);
- Definition of the infinitesimal generator matrix Q of the Markov process underlying the system;
- Definition of the steady state probabilities, throughput and utilisation using theoretical formulas;
- Encoding of the system with the PEPA Eclipse Plug-in and computation of some measures.
The projetc was accomplished together with Laura Martignon ([email protected]) and Riccardo Maso ([email protected]), as part of the course of Formal Methods for System Verification (prof. Sabina Rossi), from the master degree of Computer Science and Information Technology, from the Ca' Foscari University of Venice.