Industrial deployment of system engineering methods providing high dependability and productivity


Formal Modelling and Analysis of Business Information Applications with Fault Tolerant Middleware

Bryans, Jeremy W. and Fitzgerald, John S. and Alexander, Romanovsky and Andreas, Roth (2008) Formal Modelling and Analysis of Business Information Applications with Fault Tolerant Middleware. Newcastle University, Newcastle University TR, accepted to appear in Proceedings of ICECCS 2009. (In Press)


Official URL:


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.

Item Type:Other
Uncontrolled Keywords:Verification, Fault Assumptions, Service-Oriented Architectures, Event-B, Tool Support
Subjects:Methodology > Composition and reuse
Industrial Deployment > Business
Methodology > Resilience
Event-B > Event-B Examples
ID Code:52
Deposited By:Dr Jeremy Bryans
Deposited On:18 Dec 2008 14:43
Last Modified:19 Apr 2010 16:05

Repository Staff Only: item control page

Deploy-Project - All right reserved