Specilfication and Verilfication of Rleconfiguration Protocols in Grid Comnponent Systemns

In this work we present an approach for the formal specification and verification of the reconfiguration protocols in grid component systems. We consider fractal, a modular and extensible component model. As a specification tool we invoke a specific temporal language, separated clausal normal form, which has been shown to be capable of expressing any ECTiL⁺ expression, thus, we are able to express the complex fairness properties of a component system. The structure of the normal enables us to directly apply the deductive verification technique, temporal resolution defined in the framework of branching-time temporal logic