분산처리 시스템은 기존의 순차시스템과의 많은 차이점으로 인해 개발 과정에서 사용자 요구사항을 정형적으로 기술하고 검증에 도와줄 모델링 기법과 방법의 필요성이 증대하고 있다. 분산객체시스템에 있어 커뮤니케이션의 역할이 중요함에도 불구하고 일반적으로 설계과정에서 통신에 관한 것에 대하여 자세히 정의하는 것이 중요시되지 않았다. 하지만 분산시스템인 경우 비분산시스템에 비해 통신 형태를 결정하는 것이 중요하기 때문에, 이에 대한 것을 설계 단계에서 결정하고 정의하는 것이 중요하다. 따라서 본 논문에서는 분산시스템에 있어 temporal logic과 Petri net를 이용한 정형 명세 기법을 소개하고 있다. Temporal logic에 의한 명세 기법은 정의된 기본 predicates를 이용한 룰을 이용하여 여러 형태의 통신 형태를 정의하며 Petri net방법은 패트리넷의 특성을 이용한 동적인 행위를 표현하는데 도움을 가져다준다.

As distributed computing systems become popular, many modeling techniques and methods have been developed to specify the specification formally and verify the distributed/concurrent systems. In spite of importance of communication in distributed object-oriented systems, specifying of communication method generally has not been emphasized in the design phase. One reason is due to the system designer misunderstanding, that is, a specification needs to be independent on the implementation. However, since defining communication pattern in distributed object-oriented systems is more serious than the required message passing method in the design phase, specifying the communication pattern is necessary instead of postponing until the implementation. In this paper, two formal specification techniques, temporal logic method and Petri nets method, for the communication in distributed systems are discussed. One is based on the temporal logic, which specifies the different patterns of primitive predicates. This method enables to define the underlying mechanism which can be interpreted as constraints. The Petri net method helps to specify the dynamic behavior of communicational patterns using the properties of Petri nets.