Static verification of indirect data sharing in loosely-coupled component systems (SC2006)

Abstract:

To maintain loose coupling and facilitate dynamic composition, components in a uniform pipe-and-filter architecture have a very limited syntactic interface and often communicate indirectly by means of a shared data repository. This severely limits the possibilities for compile time compatibility checking. Even static type checking is made largely irrelevant due to the very general types given in the interfaces. The combination of uniform pipe-and-filter and a shared data repository is widely used, and in this paper we study this problem in the context of the Struts framework.

We propose simple, but formally specified, behavioural contracts for components in such frameworks and show that automated formal verification of certain semantical compatibility properties is feasible. In particular, our verification guarantees that indirect data sharing through the shared data repository is performed consistently.

Overview:

Prerequisite

In order to verify the code examples, ESC/Java2, Simplify and Java 2 must be installed on your system. Furthermore, the correct path and classpath has to be used.

Click here to see more info.

Composition example for the simplified application model

Click here to see the full specification of the composition example used in the paper, some additional specification decisions and a short verification howto.

Specification of the GatorMail webmail application

Click here to see the GatorMail source-code, the full specification of the GatorMail experiment and some additional specification decisions.

Publications:

Dependency analysis of the GatorMail webmail application

L. Desmet, F. Piessens, W. Joosen, and P. Verbaeten. Dependency analysis of the GatorMail webmail application, Report 427, Department of Computer Science, K.U.Leuven, Leuven, Belgium, September 2005. [Download full report] - [Download report without appendices] - [bibtex]

Static verification of indirect data sharing in loosely-coupled component systems

L. Desmet, F. Piessens, W. Joosen, and P. Verbaeten, Static Verification of Indirect Data Sharing in Loosely-coupled Component Systems. In SC 2006, (W. Löwe and M. Südholt, eds.), vol. 4089/2006, Lecture Notes in Computer Science, Springer-Verlag Berlin Heidelberg, 2006, pp.34-49. [Download] - [LNCS springerlink] - [bibtex]