An Experience on Probabilistic Model Checking and Stochastic Simulation to Design Self-Organizing Systems


Matteo Casadei, Mirko Viroli

IEEE Congress on Evolutionary Computation, 2009 (CEC 2009)., pages 1538-1545
May, 18-21 2009
IEEE Computer Society Press

The attention to self-organization as a feasible metaphor for dealing with the growing complexity of today's software systems is constantly growing. In particular, by adopting self-organization, systems can adapt to highly dynamic environments by local interaction among system's components. As a consequence, the global behavior of the system can be regarded as an emergent property since it appears by a process emerging from local interactions among components. The corresponding system dynamics is usually non-linear and complex so that the adoption of simulation and verification techniques in the early design stage becomes essential to carry out an effective design. Accordingly, in this paper we discuss a hybrid approach relying on stochastic simulation and probabilistic model checking and show a possible application on a problem called collective sort taken as a case study. To this end, the PRISM probabilistic model checker is adopted as a concrete tool for analyzing emergent properties of collective sort. Finally, a discussion of the corresponding results is provided.

 @inproceedings{probmodelchecking-cec09,
booktitle = {IEEE Congress on Evolutionary Computation, 2009 (CEC 2009).},
publisher = {IEEE Computer Society Press},
author = {Casadei, Matteo and Viroli, Mirko},
title = {An Experience on Probabilistic Model Checking and Stochastic Simulation to Design Self-Organizing Systems},
isbn = { 978-1-4244-2959-2},
year = 2009,
abstract = {The attention to self-organization as a feasible metaphor for dealing with the growing complexity of today's software systems is constantly growing. In particular, by adopting self-organization, systems can adapt to highly dynamic environments by local interaction among system's components. As a consequence, the global behavior of the system can be regarded as an emergent property since it appears by a process emerging from local interactions among components. The corresponding system dynamics is usually non-linear and complex so that the adoption of simulation and verification techniques in the early design stage becomes essential to carry out an effective design. Accordingly, in this paper we discuss a hybrid approach relying on stochastic simulation and probabilistic model checking and show a possible application on a problem called collective sort taken as a case study. To this end, the PRISM probabilistic model checker is adopted as a concrete tool for analyzing emergent properties of collective sort. Finally, a discussion of the corresponding results is provided.},
status = {Published},
pages = {1538-1545},
venue = {--},
month = {May, 18-21}

Publication

— authors

Matteo Casadei, Mirko Viroli

— status

published

— sort

paper in proceedings

Venue

— volume

IEEE Congress on Evolutionary Computation, 2009 (CEC 2009).

— pages

1538-1545

— publication date

May, 18-21 2009

Identifiers

— print ISBN

 978-1-4244-2959-2

BibTeX

— BibTeX ID
probmodelchecking-cec09
— BibTeX category
inproceedings

Partita IVA: 01131710376 - Copyright © 2008-2022 APICe@DISI Research Group - PRIVACY