Publications » Class » ProbmodelcheckingCec09

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

Matteo Casadei, Mirko Viroli
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.
IEEE Congress on Evolutionary Computation, 2009 (CEC 2009)., pages 1538-1545, May, 18-21 2009, IEEE Computer Society Press
@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}}