정형명세 언어인 Z는 상태기반의 명세언어로써 시스템의 기능성을 명세 및 검증하는데 사용되고 있다. Z를 사용하여 시스템 명세 시 Z에서 제공하는 스키마를 이용하여 복잡한 구조의 상태를 나타내기에 용이하다. 하지만 Z에서 커버하는 명세 대상이 단일 시스템이기 때문에 2개 이상의 시스템으로 구성된 네트워크 상의 통신을 나타내기가 힘든 단점이 있다. 본 논문에서는 Z를 이용하여 네트워크 환경의 시스템들의 기능 및 통신을 명세하기 위한 프레임워크를 제시하고 사례연구를 통해 Z를 통해 시스템의 기능성 및 통신을 모두 명세하여 프레임워크의 적용가능성을 살펴본다. 또한 두 가지 측면을 모두 포함하는 검증 속성을 나타냄으로써 네트워크 환경 시스템의 속성을 프레임워크를 통해 명세, 검증 가능함을 보인다.
Formal specification language Z is a state-based language and used for specifying and verifying system functionalities. By using Z for specifying system, developer can easily describe a complex state through a schema in Z but, the communication in network including more than two systems is not possible to be specified. In this paper, we propose the Z framework for representing communication and functionality of systems in a networked environment and show applicability of the framework by specifying both communication and functionality of safety critical real system, hydrogen monitoring system. The many properties which system must hold have functionality and communication simultaneously so in case study, we describe verification property including two aspects and show possibility of specifying and verifying properties in networked environment using framework.
