# Railway Cloud: Management and Orchestration Functionality Designed as Microservices
## 5 Microservices for Railway Cloud Orchestration
### Verification of Microservices
The transition to the ResourceAllocationAndSWinstallation state is triggered upon a command to install the new software version. In this state, the CRM microservice ensures that the update conditions are met, requests resource allocation and software version installation, then marks the CFM services' software as modified. The triggering of a testing procedure moves the software update process to the SWversionTesting state. In the SWcatalogueUpdate state, the CRM microservice updates its software catalogue and moves to the final SWupdated state. If the software test fails, the CRM service requests roll-back to the previously running CFM services' software version (the RollingBackSWversion state) and moves to the SWnotUpdated state. A transition to the SWnotUpdated state is also triggered when the pre-checking procedure fails. To prove mathematically that both software update models are correct and synchronised, it is necessary to describe the models formally, for which the Labelled Transition System (LTS) concept is used. An LTS is a tuple (S, L, T, s0), where S is a finite set of states, L is a finite set of labels that trigger the state transitions, T is a state transition relation, and s0 is an initial state. In the following definitions, the names of the states and labels are denoted by short notations in brackets. Definition 1: Let \(M^{\text{APP}}\) = (\(S^{\text{APP}}\), \(L^{\text{APP}}\), \(T^{\text{APP}}\), \(s^{\text{APP}}\), \(s^{\text{APP}}\)) be an LTS representing the model of the CFM services' software update process, supported by an orchestration application, where:  
\(S^{\text{APP}}\) = {CFMsuvUpdateStart [s\({}^{a}\)1], CFMsuvImagesQuery [s\({}^{a}\)2], CFMsuvImageSynchronization [s\({}^{a}\)3], CFMsuvPrecheck [s\({}^{a}\)4], CFMsoftwareUpdate [s\({}^{a}\)5], CFMsuvUpdateCompleted [s\({}^{a}\)6], CFMsuvUpdateFailed [s\({}^{a}\)7]]  
Figure 7: CFM services’ software update model is supported by the CRM microservice. \(L^{app}\) = {cloudSWupdateReq [\(l^{n}\)], getCloudSWcatalogRes(available) [\(l^{n}\)], getCloudSWcatalogRes(unavailable) [\(l^{n}\)], swVersionAvailable [\(l^{n}\)], swVersionUnavailable [\(l^{n}\)], swPrecheckRes(ok) [\(l^{n}\)], swPrecheckRes(nok) [\(l^{n}\)], swPrecheckRes(nok) [\(l^{n}\)], installSWversionAck [\(l^{n}\)], installSWversionErr [\(l^{n}\)]]  
\(T^{app}\) = {(\(s^{a}\)] \(u^{a}\)] \(s^{a}\)] \(s^{a}\)] \(s^{a}\)]  
A respective CFM microservice also participates in the process of CFM services' software update. Figure 8 shows the model representing the software update process from the CFM service's point of view. The SWupdate state is the initial state of the software update process. In the ResourceAllocation state, cloud resources are assigned. In the SWinstallation state, the new software version is installed. The testing of the newly installed SW version takes place in the SWtesting state; the new software version is activated in the SWactivation state, and in the UpdatedSW state, the CFM services' software is successfully updated. In the SWversionRollback state, the previously running SW version is rolled back, and the process moves to the NotUpdatedSW state.