Verifying Distributed, Event-Based Middleware Applications using Domain-Specific Software Model Checking

by L. Ruhai Cai, Jeremy S. Bradbury, Juergen Dingel

Abstract

The success of distributed event-based infrastructures such as SIENA and Elvin is partially due to their ease of use. Even novice users of these infrastructures not versed in distributed programming can quickly comprehend the small and intuitive interfaces that these systems typically feature. However, if these users make incorrect assumptions about how the infrastructure services work, a mismatch between the infrastructure and its client applications occurs, which may manifest itself in erroneous client behaviour. We propose a framework for automatically model checking distributed event-based systems in order to discover mismatch between the infrastructure and its clients. Using the SIENA event service as an example, we implemented and evaluated our framework by customizing the Bandera/Bogor tool pipeline. Two realistic Java applications are implemented to test and evaluate the framework.

Bibliographic Information [Bibtex format]

@inproceedings{CBD07,
Author = {L. Ruhai Cai AND Jeremy S. Bradbury AND Juergen Dingel},
Booktitle = {Proc. of the 9th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS'07), Springer Verlag. Lecture Notes in Computer Science 4468},
Month = {Jun.},
Pages = {44-58},
Title = {Verifying Distributed, Event-Based Middleware Applications using Domain-Specific Software Model Checking},
Year = {2007}}

Paper: [PDF]   Technical Report: [PDF]

Share: