The 1st Workshop on Model-Based Verification Validation 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 statebased 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.