On the basis of the research findings on service-oriented architecture(SOA),this paper presents a formal systematic SOA analysis,verification and validation methodology called SOARM(SOA reference model) which is the ESB (enterprise service bus)-centric model based on Petri nets and temporal logic.SOARM is consumer-centric,in which the consumers can publish their application specifications/requirements for the service providers to follow when producing or customizing services to support the application.Service interface and enterprise service bus for service realization in service-oriented design are two key parts.When a service is provided or required via the Internet,the semantic consistency becomes the critical issue in the virtualized computing environments.This architecture model tackles the issue by proposing a novel scheme:Petri nets are used to visualize the structure and model the behavior of service architectures while temporal logic is used to specify the required semantic consistency of a service.It is suggested to introduce compositionality in SOA model checking and refinement checking based on the idea of divide-and-conquer,by which the verification task of the whole system is decomposed to several smaller subtasks on the subsystems and shown how to apply it to specify an integrated front-banking system and to analyze its constraints.