This case study models a simple embedded system, as described in [KNP04c].
It is closely based on the example of [MCT94].

For more information, see: http://www.prismmodelchecker.org/casestudies/embedded.php

=====================================================================================

[KNP04c]
M. Kwiatkowska, G. Norman and D. Parker
Controller Dependability Analysis By Probabilistic Model Checking
In Proc. 11th IFAC Symposium on Information Control Problems in Manufacturing (INCOM'04), 2004

[MCT94]
J. Muppala, G. Ciardo and K. Trivedi
Stochastic reward nets for reliability prediction
Communications in Reliability, Maintainability and Serviceability 1(2):9-20, 1994