Modelling and Verifying Contract-Oriented Systems in Maude