# Railway Cloud Resource Management as a Service
## 4 Performance Management of Railway Cloud Resources
### Formal Verification of the CRPM API
In this state, the CRPM service may start default PM jobs (_DefaultPMjobsStarted_ event) and report to the CM application about its status (_DefaultPMjobStatus_ action), or the CRPM service may receive from the CM application a request to create an additional PM job (_PMjobCreateReq_ event) and may inform the CM application about the result of the operation (_PMjobCreateReq_ action). In the _Active_ state, the PM job is active and measurements are performed. In this state, the CRPM service may receive a request from the CM application to suspend the PM job (_PMjobSuspendReq_ event), and then it may inform the CM application about the result of the operation (_PMjobSuspendRes_ action). In the _Suspended_ state, the PM job is suspended. In this state, the CRPM service may receive a request from the CM application to resume the PM job (_PMjobResumeReq_ event), and may inform the CM application about the result of the operation (_PMjobResumeRes_ action). In the same state, the CRPM service may receive a request from the CM application to terminate the PM job (_PMjobTerminateReq_ event), and may inform the CM application about the result of the operation (_PMjobTerminateRes_ action). In the _Terminated_ state, the PM job is terminated. Both models are formally described to prove that the views of the CM application and the CRPM service on the PM job status are synchronized in time. **Definition 4**. : _Let \(M^{\text{MPp}}=(S^{\text{MPp}},\Sigma^{\text{MPp}},\rightarrow^{\text{MPp}},s_{ 0}{}^{\text{MPp}})\) be a formal description of the model representing the PM job status, supported by the CM application, where:_  
\(S^{\text{MPp}}=\) _[App.Null [\(s^{a}\)], App.Active [\(s^{a}\)], Suspending [\(s^{a}\)], App.Suspended [\(s^{a}\)], Resuming [\(s^{a}\)], Terminating [\(s^{a}\)], App.Terminated [\(s^{a}\)]];_  
\(\Sigma^{\text{MPp}}=\) _[DefaultPMJobsStatus [\(a\)], AddPMJob [\(b\)], PMJobCreateRes [\(c\)], SuspendPMJob [\(d\)], PMJobSuspendRes [\(e\)], ResumePMJob [\(f\)], PMJobResumeRes [\(g\)], TerminatePMJob [\(h\)], PMJobTemplateRes [\(i\)]];_  
\(\rightarrow^{\text{MPp}}=\) _[(\(s^{a}\)\({}^{a}\)\({}^  
In the _App.Unsubscribed_ state, the CM application is not subscribed to PM reports. In this state, the cloud operator may define criteria for PM reporting (_NotificationCriteria_ event), and the CM application requests to subscribe to PM reports (_PMSubscriptionReq_ action). In the _Subscribing_ state, the CM application waits for a response of its PM subscription request. In this state, a reachability check (connectivity and authorization check) may be performed (_RachabilityCheckReq_ event), and when the reachability test has passed successfully (reachable event), the CM application response is _ReachabilityCheckRes(suc)_, otherwise (unreachable event), the CM application responses with _ReachabilityCheckRes(fail)_. In the _Unreachable_ state, the reachability check has failed. In this state, the CM application's subscription request may be rejected (_PMSubscriptionRes(rej)_ event), and the CM application notifies the cloud operator about the subscription status (_SubscriptionStatus(fail)_ action). In the _Reachable_ state, the reachability check has passed. In this state, the CM application's subscription requests may be accepted (_PMSubscriptionRes(ack)_ event), and the CM application notifies the cloud operator about the subscription status (_SubscriptionStatus(suc)_ action). In the _App.Subscribed_ state, the CM application has active subscription to PM reports. In this state, the CM application may open the connection to receive PM reports (_OpenConnectionReq_ event). In the _ConnectionSetup_ state, a connection to the subscription endpoint is attempted. In case the connection was open successfully (_setupSuccess_ event), a success response is given to the CRPM service (_OpenConnectionRes(suc)_ action), otherwise (_setupFailure_ event), the CM application sends _OpenConnectionRes(fail)_.