Title of paper: Modelling and Analysing the Finance Case Study in UMC

Abstract

We describe a UMC model of the credit request scenario from SENSORIA's Finance case study and verify a number of properties expressed in the service-oriented logic SocL. The UMC model is a faithful translation of the scenario's specification in UML4SOA, which is a profile for UML that defines a high-level domain-specific modelling language for behavioural service specifications.