Case Studies
Case Study 1 : Web Application
Description
We present a travel web application that handles two types of requests:
- Requests from users who plan to meet and entertain a visitor arriving by train
- Requests from users looking for a possible destination for a day trip by train
The handling of these requests is modelled by a high level abstract CTMC as shown.
The initial state s1 of the CTMC corresponds to finding the location of the train station. For the first request type, which is expected to occur with probability p1, this is followed by finding the train arrival time (state s2), identifying suitable restaurants in the area (state s4), obtaining a traffic report for the route from the user’s location to the station (state s6), and returning the response to the user (state s7).
For the second request type, which occurs with probability (1 − p1), state s1 is followed by finding a possible destination (state s3), and obtaining a weather forecast for this destination (state s5). With a probability of p2 the weather is unsuitable and a new destination is selected (back to state s3). Once a suitable destination is selected, the traffic report is obtained for travel to the station (state s6 ) and the response is returned to the user (state s7).
The component execution times were obtained by calling web services from a prototype application with p1=0.3 and p2=0.1. The web services called are listed below with the associated rate for use in the high level model:
| Label | Third-party service | rate (/s) |
|---|---|---|
| location | Bing location service | 9.62 |
| arrivals | Thales rail arrivales board | 19.88 |
| departures | Thales rail departures board | 19.46 |
| search | Bing web search | 1.85 |
| weather | WebServiceX.new weather service | 1.11 |
| traffic | Bing traffic service | 2.51 |
Properties
The following properties were defined to evaluate the model:
- P1 The fraction of user requests handled in under T seconds
- P2 The fraction of 'day trip' user requests handled in under T seconds
- P3 The expected profit per request handled, assuming that 1 cent is charged for requests handled within T seconds and a 2 cent penalty is paid for requests not handled within 3 seconds.
Data files
| File | Description |
|---|---|
| High level CTMC model | A CTMC model which can be evaluated in PRISM. The rates are as stated in the table above. |
| CSL Properties | A prism properties file with the three properties listed above. |
| Component timing data | A zip file containing 4 data sets run at seperate times on the example system. Set 1 is contains the timing data which is encoded in the CTMC model |
| OMNI model file | An annotated model file for use in OMNI. |
| OMNI config file | A configuration file set up to generate OMNI models for each data set and property required. (Note that P3 uses the same model as P1). |
Case Study 2 : IT Support System
Description
The data for this case study comes from a real-world IT support system deployed at the Federal Institue of Education, Science and Technology of Rio Grande de Norte (IFRN), Brazil. The system enables the IFRN IT support team to handle user tickets reporting problems with the institute’s computing systems.
A high-level CTMC model of the business process implemented by the IT system is shown. In this model, state s0 corresponds to a ticket being created by a “client” and awaiting allocation to a member of the support team. Once allocated, the ticket is processed (state s1) and, if the issue can be resolved, the client is informed and the ticket awaits sign off (s2) before being marked as complete (s7). The client may choose to reopen (s5) the ticket rather than close it, in which case the ticket is returned to the support team member for further processing. Whilst processing a ticket, the support staff may require additional information from the client (s3) or may need to reallocate the ticket to another member of the IT support team (s4). A ticket may also be abandoned (s6) either during processing or whilst awaiting additional information from the client.
Properties
The following properties were defined to evaluate the model:
- P1 The probability of reaching the complete state within T seconds
- P2 The probability of reaching complete wihtin T seconds assuming that a ticket is not reopened and does not require additional information. i.e. no further action is required from the user who opens the ticket.
Data files
| File | Description |
|---|---|
| High level CTMC model | A CMC model which can be evaluated in PRISM. |
| CSL properties | A prism properties file with the two properties described in CSL |
| Component timing data | A zip file containing the two component timing sets used in the accompanying paper. Set 1 is used as the timing information for the CTMC model given above. |
| OMNI model file | An annotated model file for use in OMNI. |
| OMNI config file | An OMNI configuration file which generates a model data set 1 and each of the properties. |