TY  - INPR
CY  - Newcastle University TR, accepted to appear in Proceedings of ICECCS 2009
ID  - deploy52
UR  - http://www.cs.ncl.ac.uk/publications/techreports/trs/papers/1131.pdf
A1  - Bryans, Jeremy W.
A1  - Fitzgerald, John S.
A1  - Alexander, Romanovsky
A1  - Andreas, Roth
Y1  - 2008/12/15/
N2  - 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.   
PB  - Newcastle University
KW  - Verification
KW  -  Fault Assumptions
KW  -  Service-Oriented Architectures
KW  -  Event-B
KW  -  Tool Support  
TI  - Formal Modelling and Analysis of Business Information
Applications with Fault Tolerant Middleware 


AV  - public
ER  -

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