# An Approach to Designing Critical Railway Voice Communication
## 6 Verification of the Critical Voice Application Design  
To verify the application design, models illustrating the views of the critical communication application and the network on the state of the voice call are synthesized. Figure 15 shows the state model of the originating leg supported by the critical application. Figure 14: Services interaction flow for arbitration and invite-a-user messaging. In the null state, there is no call attempt. In the CommAuthorization state, the FRMCS network checks the authority/ability of the party to place a voice call to the called party with the given properties, e.g., based on the calling and called parties' functional identity user profiles and locations. In the active state, the call leg connection to the calling party exists. It is a composite state that encompasses the setup, established, assured, arbitration, and QoSClassNegotiation substates. In the setup substate, the call leg connection to the called party is built. In the established substate, the call is established. In the assured state, link-quality supervision is activated. In the QoSClassNegotiation substate, the application waits for a response to its request to dynamically set the QCI of the ongoing connection. In the arbitration substate, there is a new incoming call and the application waits for the decision from the FRMCS about the further treatment of the new incoming call. In the release state, the call is released but information about the call can be received for some time afterward and the resource representing the assured voice call is later deleted. Figure 16 shows the originating leg state model supported by the network. In the Null&AuthorizedCallAttempt state, there is no call, the calling party's right to make a call is checked, and the destination number is received. In the analyzing state, the collected information is analyzed and/or translated and the routing address and call type are determined. In the CallRouting state, the routing address and call type are interpreted, a path is selected, and the call is routed. In the ringing state, the call processing continues for the called party and an indication is expected that the called party has answered. In the connected state, the connection between the calling party and the called party is established and call data are collected. In the releasing state, the resources assigned to the call are released. Figure 15: Critical application view on the state of the originating call leg. Both models must run as parallel processes and their communication must be synchronized so that the processes exhibit equivalent behavior. Bisimilarity is a well-established and powerful proof technique that is usually referred to as a behavioral equivalence for processes. It is defined as the union of all bisimulation relations on terms as pairs [35]. The most common notation used to study bisimilarity is the Labelled Transition System (LTS), which is essentially a labeled directed graph. To verify the models representing the critical application and network views on the call state, both models are formally described as LTSs. An LTS is a quadruple consisting of a set of states, a set of inputs, a set of transitions, and an initial state [36]. In the following definitions, the notations in brackets represent short notations for the names of states and inputs. **Definition 1**.