To conduct model checking, explained in [35], the system was fully described as state diagrams. Figure 5 shows the main system diagrams and Figure 6 depicts the failure handling diagram.