This paper gives a verification method of a service specification in a communication system by utilizing Petri net. We define a service specification and clarify the feature of the specification. And we discuss a relation between a service specification and Petri net which represents the specification. Furthermore, this paper describes some kinds of verification for the specification and shows several examples. We are now developing a software support system-EXPRESS (EXPeRt system for ESS). EXPRESS designs automatically the service specification from user's requirements. In EXPRESS, each requirement is converted into ISG (Individual Service Graph) and all ISGs are integrated into TSG (Total Service Graph). TSG is the final service specification. ISG and TSG are described by using Petri net. Petri net is used for modeling a communication protocol and an asynchronous system. A service starts from an idle state and returns to the same idle state in a communication system. This means that a service specification should have a t-invariant. And a t-invariant which can not be decomposed is called a prime service. The followings are needed for verification of the specification: verification of ISG, detection of ISG from TSG and detection of other prime services than ISG. These are verified by utilizing an analysis of Petri net.