# Railway Cloud Resource Management as a Service
## 3 Fault Management of Railway Cloud Resources
### Formal Verification of CRFM API  
To verify the proposed approach to the design of cloud resource FM API, models representing the alarm status maintained by a CM application and by the CRFM service are developed. Figure 7 shows the UML (Unified Modeling language) state diagram of a simplified alarm status model maintained by a CM application. The model includes subscription to and notification of alarms. Being notified of an alarm event, the CM application may query alarm information, request alarm acknowledgement or clearance, or request alarm suppression, or resume. In the _AppNull_ state, the alarm does not exist. In this state, the cloud operator may define the alarm notification criteria (_setNotifCriteria_ event), and the CM application requests to subscribe to the alarm notifications (_AlarmSubscriptionReq_ action). In the _AppNull_ state, the CRFM service may accept a subscription (_AlarmSubscriptionRes(ack)_ event) or may  
Figure 6: Flow of creating the subscription, retrieving the subscription information, notifying of the alarm occurrence, and deleting the subscription. Figure 7: A simplified model representing the alarm status supported by a CM application. reject it (_AlarmSubscriptionRes(fail)_ event) and, in either case, the cloud operator is notified (_subscribed_ action or _notsubscribed_ action). In the _AppNull_ state, the CRFM service may notify the CM application about an alarm (_AlarmNotification(raised)_ event), and the CM application notifies the cloud operator (_alarmRaised_ action). In the _AppActive_ state, the alarm is active. In the _AppActive_ state, the cloud operator may query the alarm (_queryAlarm_ event), and the CM application requests information about the alarm (_AlarmQueryReq_ action). In the _AppActive_ state, the CRFM service provides information about the alarm (_AlarmQueryRes_ event), and the CM application sends information to the cloud operator (_alarmInfo_ action). In the _AppActive_ state, the cloud operator may request alarm suppression (_suppressAlarm_ event), and the CM application sends a request to the CRFM service to suppress the alarm (_AlarmSuppressReq_ action). In the _AppActive_ state, the cloud operator may request alarm acknowledgment (_acknowledgeAlarm_ event), and the CM application sends a request from the CRFM service to acknowledge the alarm (_AlarmAckReq_ action). In the _AppActive_ state, the cloud operator may request alarm clearance (_clearAlarm_ event) and the CM application sends a request from the CRFM service to clear the alarm (_AlarmClearReq_ action). In the _Acknowledge_ state, the CM application waits for alarm acknowledgement. In this state, the CRFM service may acknowledge the alarm (_AlarmAckRes_ event), and the CM application notifies the cloud operator (_alarmAcknowledge_ action). In the _Suppressing_ state, the CM application waits for alarm suppression. In this state, the CRFM service may inform the CM application that the alarm is suppressed (_AlarmSuppressRes_ event), and the CM application notifies the cloud operator (_alarmSuppressed_ action). In the _AppSuppressed_ state, the alarm is suppressed. In this state, the cloud operator may request to resume the alarm processing (_resumeAlarm_ event), and the CM application requests the CRFM service to resume to the alarm (_AlarmResumeReq_ action). In the _Resuming_ state, the CM application waits for alarm resumption. In this state, the CRFM service may inform the CM application that the alarm is resumed (_AlarmResumeRes_ event), and the CM application notifies the cloud operator (_alarmResumed_ action). In the _Clearing_ state, the CM application waits for alarm clearance. In this state, the CRFM service may inform the CM application that the alarm is cleared (_AlarmClearRes_ event), and the CM application notifies the cloud operator (_alarmCleared_ action). In the _AppCleared_ state, the alarm is cleared. Figure 8 shows the UML state diagram of a simplified alarm status model maintained by the CRFM service. In the _Null_ state, the alarm does not exist.