Recently service orientation is becoming a mainstream approach for building large scale software systems. A key requirement in service-oriented design is the dependability of service. It stipulates that the behavior of services is controllable. Formal models can aid in constructing software in a dependable manner. They can describe services precisely and compose them together consistently. This paper presents a strategy for service realization based on a novel layered formal model. When a service is provided or required via internet, the semantic consistency becomes critical issue. Our architecture tackles the issue by proposing a novel scheme: defining contract of a service to keep semantic information. Although service-oriented design is our prime target, the contract models, to a large extent, are independent of the framework of design and therefore applicable to large scale software design in general.