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.
Grid Component Model Grid IDE Automated Reconfiguration Formal Specification Deductive Reasoning
Alessandro Basso Alexander Bolotov Vladimir Getov
School of Electronics and Computer Science University of Westminster Watford Road, Northwick Park Harrow HA1 3TP, London, U.K.
国际会议
上海
英文
379-386
2009-07-08（万方平台首次上网日期，不代表论文的发表时间）