/Stochastic-model-of-a-Key-Distribution-Centre

Stochastic model and analysis of the Key Distribution Centre model, exploiting PEPA specification language.

Stochastic-model-of-a-Key-Distribution-Centre

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:

  1. Short introduction containing an informal, but careful, explanation of the problem which we wish to model;
  2. Identification of the components of interest and the activities which they undertake either individually or in co-operation;
  3. Description of these components behaviourally, explaining how they interact with each other;
  4. High-level description of each component in the PEPA stochastic process algebra;
  5. Specification of the entire system in the PEPA process algebra as the co-operation of the above components;
  6. Drawing of the derivation graph of the model (or part of it);
  7. Definition of the infinitesimal generator matrix Q of the Markov process underlying the system;
  8. Definition of the steady state probabilities, throughput and utilisation using theoretical formulas;
  9. Encoding of the system with the PEPA Eclipse Plug-in and computation of some measures.

Contributors

The projetc was accomplished together with Laura Martignon (879707@stud.unive.it) and Riccardo Maso (885271@stud.unive.it), 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.