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

@incollection{citeulike:3993231, 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.}, author = {Cai, L. and Bradbury, Jeremy and Dingel, Juergen}, citeulike-article-id = {3993231}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/978-3-540-72952-5_3}, citeulike-linkout-1 = {http://www.springerlink.com/content/b5471u714138331m}, doi = {10.1007/978-3-540-72952-5_3}, journal = {Formal Methods for Open Object-Based Distributed Systems}, keywords = {2007, concurrent, event, modelchecking, verification}, pages = {44--58}, posted-at = {2009-02-02 06:37:10}, priority = {2}, title = {Verifying Distributed, Event-Based Middleware Applications Using Domain-Specific Software Model Checking}, url = {http://dx.doi.org/10.1007/978-3-540-72952-5_3}, year = {2007} }

TY - CHAP ID - citeulike:3993231 L3 - citeulike-article-id:3993231 N2 - 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. JF - Formal Methods for Open Object-Based Distributed Systems EP - 58 TI - Verifying Distributed, Event-Based Middleware Applications Using Domain-Specific Software Model Checking SP - 44 KW - 2007 KW - concurrent KW - event KW - modelchecking KW - verification AU - Cai, L AU - Bradbury, Jeremy AU - Dingel, Juergen PY - 2007/// UR - http://dx.doi.org/10.1007/978-3-540-72952-5_3 ER -