Modelling and verifying contract-oriented systems in Maude