An Approach to Formal Specification and Formal Validation of Facilities of a Mobile Middleware Architecture

Formal specification, verification, modeling of distributed software systems including middleware is an important area of research [4], [5], [6], [8]. Even then, as of now, no universally accepted standard method for formalization of middleware exists. Mobile middleware systems are increasingly gaining importance due to cheap and highly efficient mobile computing and networking hardware, and also due to the fact that complexities of heterogeneous networking environment and context-aware adaptation must be handled at the application layer [1], [2]. [1] presents a novel middleware architecture that satisfies the requirements of multimedia communication in mobile environment. [2] has extended and refined the idea of multimedia object model introduced in [1] and validated robustness of design by help of unit sequence diagrams. Little has been done to formalize mobile middleware systems, and as of now, no universally accepted standard method for formalization exists. In this paper, we aim to provide formal statements for the concepts sketched in [1] and [2]. We have introduced and used the idea of configuration, and used predicate calculus as the tool of formalization. The contributions of this paper are: (i) introducing the generic idea of configuration to express the static and dynamic behavior of the middleware, (ii) formally expressing the definitions (such as interoperability, service adaptability) and facilities of a proposed middleware [1], [2], (iii) using the formal definitions to validate the design, two key facilities in particular - namely Interoperability facility and service adaptability facility.