Temporal Specification and Deductive Verification of a Distributed Component Model and Its Environment

In this paper we investigate the formalisation of distributed and long-running stateful systems using our normative temporal specification framework. We analyse aspects of a component-oriented Grid system, and the benefits of having a logic-based tool to perform automated and safe dynamic reconfiguration of its components. We describe which parts of this Grid system are involved in the reconfiguration process and detail the translation procedure into a state-based formal specification. Subsequently, we apply deductive verification to test whether dynamic reconfiguration can be performed. Finally, we analyse the procedure required to update our model for reconfiguration and justify the validity and the advantages of our methodology.