Analysis and Verification of Web Services Resource Framework (WSRF) Specifications Using Timed Automata

摘要

Throughout the history of computing, engineers have used various formal methods to improve the quality of software and hardware. The next natural step is trying to exploit their advantages in the so-called new era of computing: Cloud Computing. In this paper, we present a first approximation about how to simulate and check the behaviour of these systems using timed automata through the model checking tool UPPAAL. We use Web Services Resource Framework (WSRF) as a standard intended to the modelling of distributed resources using Web services, and we apply formal techniques to WSRF specifications in order to analyse and verify these specifications.