Context Aware Specification and Verification of Distributed Systems

Distributed and mobile systems are typically composed of heterogeneous computational units that interact with each other following a predefined protocol. Process algebras and modal logics have been largely used as tools for specifying and verifying such kind of systems. However, to use these tools a complete system description has to be provided. This is not always possible. Indeed, even if the protocol governing the interactions among the system components is completely specified, the precise implementation of each component, as well as the number of network elements, is generally unknown. In this paper we present a set of formal tools that permits specifying systems by means of mixed specifications: a system is not considered in isolation, but under the assumption that the enclosing environment satisfies a given set of properties. A model-checking algorithm is also defined to verify whether considered specifications satisfy or not the expected properties. In the former case, it is also guaranteed that whenever the context is instantiated with components satisfying the assumptions, property satisfaction is preserved.