Formal Verification of Distributed Transaction Management in a SOA Based Control System

In large scale, heavy workload systems, managing distributed transactions on multiple datasets becomes challenging and error prone task. Software systems based on service oriented architecture principles that manage critical infrastructures are typical environments where robust transaction management is one of the essential goals to achieve. The aim of this paper is to provide a formal description of the solution for transaction management and individual service component behavior in a SOA-based control system, and prove the correctness of the proposed design with the SMV formal verification tool. Atomic commitment protocol is used as a basis for solving distributed transaction management problem. SMV language and verification tool are utilized for formal description of the problem and verification of the necessary properties. The case study describes an application of the proposed approach in commercial software system for electrical power distribution management. Verification of given model properties has shown that suggested solution is suitable for the described class of SOA-based systems.