Using weak bisimulation for enterprise integration architecture formal verification - I

Weak Bisimulation is a process calculus equivalence relation, applied for the verification of communicating concurrent systems [26]. In this paper we propose the application of Weak Bisimulation for Enterprise Application Integration verification. Formal verification is carried out by taking the system specification and design models of an integrated system and converting them into value passing CCS (Calculus of Communicating Systems) processes. If a Weak Bisimulation relation is found F between the two models, then it could be concluded that the EI Architecture is a valid one. The formal verification of an EI Architecture would give value to an EI project framework, allowing the challenge of cumbersome and complex testing typically faced by El projects [18], to be alleviated and thus increasing the possibility of a successful EI project, delivered on time and within the stipulated budgeted costs. This paper shows the applicability; of value passing CCS (or equivalent) formal notation to model the EI systems characteristics, as well as investigates into the computation complexity of available weak bisimulation algorithms, in order to analyze the applicability of this proposition in real life.