UPPAAL SMC tutorial

Abstract

This tutorial paper surveys the main features of Uppaal SMC, amodel checking approach in Uppaal family that allows us to reason on networks of complex real-timed systemswith a stochastic semantic.We demonstrate the modeling features of the tool, new verification algorithms and ways of applying them to potentially complex case studies.