Abstract
Correctness of a system depends on the correct execution of transactions. For large systems, e.g., web-based, these transactions involve more than one component and hence more than one independent entity. Such transactions are called Long Running Transaction(LRT) as they coordinate complex interactions among multiple sub-systems. Well known roll-back mechanism do not suffice to handle faults in LRTs, therefore compensation mechanisms are introduced. However, introduced structures are complex and hard to understand and handle. Formal methods are well known tool for modelling, analysis and synthesis of complex systems. In this chapter we present a technique that allows modelling LRTs using Compensating CSP, then translating them to Promela language and analyzing using SPIN tool. We have modelled and verified the LRTs. We exemplify it using a web service called Air-ticket Reservation System (ATRS).
| Original language | English |
|---|---|
| Title of host publication | IAENG Transactions on Electrical Engineering Volume 1 |
| Subtitle of host publication | Special Issue of the International Multiconference of Engineers and Computer Scientists 2012 |
| Publisher | World Scientific Publishing Co. |
| Pages | 123-136 |
| Number of pages | 14 |
| ISBN (Electronic) | 9789814439084 |
| ISBN (Print) | 9789814439077 |
| DOIs | |
| Publication status | Published - 1 Jan 2012 |
| Externally published | Yes |
Keywords
- Business transaction
- CCSP
- Compensation
- Formal model
- Process Algebra
- SPIN tool