Formal modelling and analysis of business information applications with fault tolerant middleware

Distributed information systems are critical to the functioning ofmany businesses; designing them to be dependable is a challenging butimportant task. We report our experience in using formal methods toenhance processes and tools for development of business informationsoftware based on service-oriented architectures. In our work, whichtakes place in an industrial setting, we focus on the configuration ofmiddleware, verifying application-level requirements in the presenceof faults. In pilot studies provided by SAP, we used the Event-Bformalism and the open Rodin tools platform to prove properties ofmodels of business protocols and expose weaknesses of certainmiddleware configurations with respect to particular protocols. Wethen extended the approach to use models automatically generated fromdiagrammatic design tools, opening the possibility of seamlessintegration with current development environments. Increasedautomation in the verification process, through domain-specific modelsand theories, is a goal for future work.