Distributed Event-Based System Features: Representation and Reasoning

Several middleware systems have been recently proposed for the development of distributed, pervasive, and ubiquitous applications where heterogeneous components interact asynchronously via events. While most of the research in the area has focused on the efficient operation of the middleware, the prediction and verification of the behaviour exhibited by these systems is still an open problem. In this paper we present models formalizing the event-related features commonly found in Distributed Event-Based Systems (DEBSs). DEBSs are one of the kinds of middleware that enable the interaction of components via events. The models here presented are based on a process algebra for which a model checking tool encoding the semantics of the algebra has been developed. From the models, and based on the semantics of the process algebra and associated tool, it is possible to specify and check properties not verifiable with prior work in the area.