Here, we list some case studies to show how OCRA can be used:

  • Redundant Sensors. The case study describes a simple redundant sensor that guarantees a correct output under some assumption on the failures of the two basic sensors. Some monitor components try to detect the failures, while a selector component outputs the correct value if possible. This architecture has been taken from a similar case study developed in the FoReVer project. All components have been implemented in SMV. All models and commands can be found here. A description of the case study can be found here.