Message Sequence Charts to Specify the Communicating Threads for Concurrent Discrete Wavelet Transform Based Image Compression and a Verification Analysis

Message sequence charts (MSCs) are an appealing visual formalism mainly used in the early stages of system design to capture the system requirements. However, to move towards an implementation, an executable specifications related in some fashion to the MSC-based requirements must be obtained. The MSCs can be used effectively to specify the communicating threads in the way where high-level transition systems is used to capture the control flow of the system components and MSCs to describe the non-atomic component interactions. This specification is amenable to formal verification. We present the way how to specify the communicating threads using MSCs and how to verify the correctness of the concurrent wavelet transform used for image compression. Symbolic model verifier (SMV) is used for formal verification. Firstly, the use of wavelet transform for image compression is presented. Secondly, the MSC based specification is presented. Thirdly, the concurrency in the threads for concurrent wavelet transform along with the grammar of the syntax formulated is accessed. Finally, we present the verification result of the system using the SMV program.