%A Jeremy W. Bryans
%A John S. Fitzgerald
%A Romanovsky Alexander
%A Roth Andreas
%T Formal Modelling and Analysis of Business Information
Applications with Fault Tolerant Middleware 


%X Distributed information systems are critical to the functioning of
many businesses; designing them to be dependable is a challenging but
important task. We report our experience in using formal methods to
enhance processes and tools for development of business information
software based on service-oriented architectures. In our work, which
takes place in an industrial setting, we focus on the configuration of
middleware, verifying application-level requirements in the presence
of faults. In pilot studies provided by SAP, we used the Event-B
formalism and the open RODIN tools platform to prove properties of
models of business protocols and expose weaknesses of certain
middleware configurations with respect to particular protocols. We
then extended the approach to use models automatically generated from
diagrammatic design tools, opening the possibility of seamless
integration with current development environments. Increased
automation in the verification process, through domain-specific models
and theories, is a goal for future work.   
%C Newcastle University TR, accepted to appear in Proceedings of ICECCS 2009
%D 2008
%K Verification, Fault Assumptions, Service-Oriented Architectures, Event-B, Tool Support  
%I Newcastle University
%L deploy52

<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>