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.

• Train Gate Controller. This example represents the train crossing problem. The example is composed of a system component, a Train component, a Gate component and a Controller component. The model's behavior is the following: When a train reaches the gate the controller raises the gate. When the gate is open the train passes through the gate. When the train passes the gate the controller brings down the gate. This example is encoded in hybrid time giving the possibility to consider continuous time events. All models and commands can be found here.

• Air Traffic Control. The main objective of an air traffic control system is to avoid aircraft collisions.In air traffic management, a Loss of Separation (LOS) between two aircraft occurs when they are predicted to pass too close to each other. One of the major goals of the next generation of air traffic control is to minimize the number of times that a LOS ever occurs. This task is called Separation Assurance. In This case study, we are interested in studying the separation assurance provided by different designs when splitting the functionality between components on-board airplanes and on-ground. In particular, aircraft that always rely on the ground for separation assurance are called Ground Separated (GSEP), while air-craft with on-board separation assurance capabilities are called Self-Separating(SSEP). The main distinction between the two types of aircraft is the ability of SSEP to perform self-separation, without the need of contacting the ground. The Goal of distributing the responsibility for separation assurance across different components is to increase efficiency and improve fault tolerance. A further description of the case study can be found here. This case study is part of this project. To run the experimental evaluation xSAP and nuXmv are needed. All models, commands and scripts can be found here.