You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 
 
 
 
 
Dave Parker 5c1bb43a2f Code tidy (function return types). 18 years ago
..
README Updated URLs in case study READMEs. 18 years ago
auto Renaming examples directory to prism-examples. 20 years ago
embedded.csl Tidied up embedded example. 19 years ago
embedded.sm Renaming examples directory to prism-examples. 20 years ago

README

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.html

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

[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