Z based Framework for Networked System Specification and Verification

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. Z . Z Z . Z 2 . Z Z . , .