Service Oriented Computing (SOC) is a new paradigm for organising distributed systems by using software units known as services and an architectural style known as the Service Oriented Architecture (SOA). The vision of SOA is to bridge the gap between the business and technology domains, to promote business agility, and to facilitate integration of heterogeneous systems within and across organizational boundaries. Currently, the most promising implementation alternative for SOA is the Web services framework, leveraging on widely accepted standards, such as WSDL, SOAP, and UDDI. Currently, the issues of trust and dependability on third-party Web services have become key challenges to the success of Service Oriented Computing in industrial environments. One major obstacle in addressing these issues is that the current standard for Web service interface description (WSDL) neglects the behavioural aspects, which may lead to incorrect bindings and unpredictable results. As part of a wider research conducted to address certain software engineering challenges in Service Oriented Computing, this presentation summarises an approach to the aforementioned problem. It is based on formally modelling Web services, including behavioural aspects, employing the stream X- machine formalism. This modelling brings about a number of benefits in different possible scenarios. In this presentation the common Web service publication and discovery case demonstrates how behavioural models are used to ensure that the service consumer binds with Web services providing a suitable behaviour, and a verified implementation.