Using Probabilistic Model Checking and Simulation for Designing Self-Organizing Systems