A Scheme of Model Verification of the Concurrent Discrete Wavelet Transform (DWT) for Image Compression
The scientific community has invested a great deal of effort in the fields of discrete wavelet transform in the last few decades. Discrete wavelet transform (DWT) associated with the vector quantization has been proved to be a very useful tool for the compression of image. However, the DWT is very computationally intensive process requiring innovative and computationally efficient method to obtain the image compression. The concurrent transformation of the image can be an important solution to this problem. This paper proposes a model of concurrent DWT for image compression. Additionally, the formal verification of the model has also been performed. Here the Symbolic Model Verifier (SMV) has been used as the formal verification tool. The system has been modeled in SMV and some properties have been verified formally.
[1] Jayant, N. and Noll, P., "Digital Coding of Waveforms: Principles and
Applications to Speech and Video", NJ: Prentice-Hall, 1984.
[2] Polikar, R. B. "Wavelet Tutorial Part I, II, III, IV",
http://users.rowan.edu/~polikar/WAVELETS/WTtutorial.html, 2003.
[3] David Salomon, "Data Compression: the Complete Reference", 2nd Ed.
Springer, 2002.
[4] Michael B.Martin, "Application of Wavelets to image Compression",
M.S. Thesis, Blacksburg Virigina, 1999.
[5] Jayant, N., Johnston, J., and Safranek, R., "Signal compression based on
models of human perception", in Proc. IEEE, Vol. 81, October 1993, pp.
1385-1422.
[6] Rao, K. R. and Yip, P., "Discrete Cosine Transform: Algorithms,
Advantages and Applications", San Diego, CA: Academic, 1990.
[7] Gortler. S., Schröder, P., Cohen, M., and Hanrahan, P., "Wavelet
Radiosity", in Proc. SIGGRAPH, 1993, pp. 221-230.
[8] Berman, D., Bartell, J. and Salesin, D., "Multiresolution Painting and
Compositing", in Proc. SIGGRAPH, 1994, pp. 85-90.
[9] Finkelstein. A. and Salesin, D., "Multiresolution Curves", in Proc.
SIGGRAPH, 1994, pp. 261-268.
[10] Eck, M., DeRose, T., Duchamp, T., Hoppe, H., Lounsberry, M. and
Stuetzle, W., "Multiresolution Analysis of Arbitrary Meshes", in Proc.
SIGGRAPH, 1995, pp. 173-182.
[11] Lippert, L. and Gross, M., "Fast Wavelet Based Volume Rendering by
Accumulation of Transparent Texture Maps", in Proc.
EUROGRAPHICS, 1995, pp. 431-443.
[12] Jacobs, C., Finkelstein, A. and Salesin, D., "Fast Multiresolution Image
Querying", in Proc. SIGGRAPH, 1995, pp. 277-286.
[13] Myers, Glenford J. "The Art of Software Testing", John Wiley and Sons.
ISBN 0-471-04328-1, 1979.
[14] Edmund M. Clakre, Jr. Oma FrumBerg and Doron A. Paled, "Model
Checking", The MIT Press, Second Printing, 2000.
[15] Kamrul Hasan Talukder and Koichi Harada, "Development and
Performance Analysis of an Adaptive and Scalable Image Compression
Scheme with Wavelets", Published in the Proc. of ICICT, BUET, Dhaka,
Bangladesh, ISBN: 984-32-3394-8, March 2007, pp. 250-253.
[16] Eric J. Stollnitz, Tony D. Derose and David H. Salesin, "Wavelets for
Computer Graphics", Morgan Kaufmann Publishers, Inc., San Francisco.
1996.
[17] Robert L. Cook and Tony DeRose, "Wavelet Noise", ACM Transactions
on Graphics, Volume 24, Number 3, Proc. of ACM SIGGRAPH 2005,
July 2005, pp. 803-811.
[18] Vetterli, M. and Kovacevic, J., "Wavelets and Subband Coding",
Englewood Cliffs, NJ, Prentice Hall, 1995, http://cm.belllabs.
com/who/jelena/Book/home.html
[19] G. Beylkin, R. Coifman, and V. Rokhlin, "Fast wavelet transforms and
numerical algorithms", I. Communications on Pure and Applied
Mathematics, 44(2), March 1991, pp. 141-183.
[20] Colm Mulcahy, "Image compression using the Haar Wavelet
transforms", Spelman Science and Math Journal, Vol 1, No 1, April
1997, pp. 22-31.
[21] Fred B. Schneider, "On Concurrent Programming" Inside Risks 94,
CACM 41, 4, Apr 1998.
[22] Michael Huth, "Logic in Computer Science: tool based modeling and
reasoning about systems", Proceedings of the International Conference
on Frontiers in Education 2000, Kansas City, October 2000.
[23] Cadence Berkeley Laboratories, Free download from the website:
http://www.kenmcmil.com/smv.html, Califonia, USA. SMV Model
Checker, 1999.
[1] Jayant, N. and Noll, P., "Digital Coding of Waveforms: Principles and
Applications to Speech and Video", NJ: Prentice-Hall, 1984.
[2] Polikar, R. B. "Wavelet Tutorial Part I, II, III, IV",
http://users.rowan.edu/~polikar/WAVELETS/WTtutorial.html, 2003.
[3] David Salomon, "Data Compression: the Complete Reference", 2nd Ed.
Springer, 2002.
[4] Michael B.Martin, "Application of Wavelets to image Compression",
M.S. Thesis, Blacksburg Virigina, 1999.
[5] Jayant, N., Johnston, J., and Safranek, R., "Signal compression based on
models of human perception", in Proc. IEEE, Vol. 81, October 1993, pp.
1385-1422.
[6] Rao, K. R. and Yip, P., "Discrete Cosine Transform: Algorithms,
Advantages and Applications", San Diego, CA: Academic, 1990.
[7] Gortler. S., Schröder, P., Cohen, M., and Hanrahan, P., "Wavelet
Radiosity", in Proc. SIGGRAPH, 1993, pp. 221-230.
[8] Berman, D., Bartell, J. and Salesin, D., "Multiresolution Painting and
Compositing", in Proc. SIGGRAPH, 1994, pp. 85-90.
[9] Finkelstein. A. and Salesin, D., "Multiresolution Curves", in Proc.
SIGGRAPH, 1994, pp. 261-268.
[10] Eck, M., DeRose, T., Duchamp, T., Hoppe, H., Lounsberry, M. and
Stuetzle, W., "Multiresolution Analysis of Arbitrary Meshes", in Proc.
SIGGRAPH, 1995, pp. 173-182.
[11] Lippert, L. and Gross, M., "Fast Wavelet Based Volume Rendering by
Accumulation of Transparent Texture Maps", in Proc.
EUROGRAPHICS, 1995, pp. 431-443.
[12] Jacobs, C., Finkelstein, A. and Salesin, D., "Fast Multiresolution Image
Querying", in Proc. SIGGRAPH, 1995, pp. 277-286.
[13] Myers, Glenford J. "The Art of Software Testing", John Wiley and Sons.
ISBN 0-471-04328-1, 1979.
[14] Edmund M. Clakre, Jr. Oma FrumBerg and Doron A. Paled, "Model
Checking", The MIT Press, Second Printing, 2000.
[15] Kamrul Hasan Talukder and Koichi Harada, "Development and
Performance Analysis of an Adaptive and Scalable Image Compression
Scheme with Wavelets", Published in the Proc. of ICICT, BUET, Dhaka,
Bangladesh, ISBN: 984-32-3394-8, March 2007, pp. 250-253.
[16] Eric J. Stollnitz, Tony D. Derose and David H. Salesin, "Wavelets for
Computer Graphics", Morgan Kaufmann Publishers, Inc., San Francisco.
1996.
[17] Robert L. Cook and Tony DeRose, "Wavelet Noise", ACM Transactions
on Graphics, Volume 24, Number 3, Proc. of ACM SIGGRAPH 2005,
July 2005, pp. 803-811.
[18] Vetterli, M. and Kovacevic, J., "Wavelets and Subband Coding",
Englewood Cliffs, NJ, Prentice Hall, 1995, http://cm.belllabs.
com/who/jelena/Book/home.html
[19] G. Beylkin, R. Coifman, and V. Rokhlin, "Fast wavelet transforms and
numerical algorithms", I. Communications on Pure and Applied
Mathematics, 44(2), March 1991, pp. 141-183.
[20] Colm Mulcahy, "Image compression using the Haar Wavelet
transforms", Spelman Science and Math Journal, Vol 1, No 1, April
1997, pp. 22-31.
[21] Fred B. Schneider, "On Concurrent Programming" Inside Risks 94,
CACM 41, 4, Apr 1998.
[22] Michael Huth, "Logic in Computer Science: tool based modeling and
reasoning about systems", Proceedings of the International Conference
on Frontiers in Education 2000, Kansas City, October 2000.
[23] Cadence Berkeley Laboratories, Free download from the website:
http://www.kenmcmil.com/smv.html, Califonia, USA. SMV Model
Checker, 1999.
@article{"International Journal of Information, Control and Computer Sciences:54573", author = "Kamrul Hasan Talukder and Koichi Harada", title = "A Scheme of Model Verification of the Concurrent Discrete Wavelet Transform (DWT) for Image Compression", abstract = "The scientific community has invested a great deal of effort in the fields of discrete wavelet transform in the last few decades. Discrete wavelet transform (DWT) associated with the vector quantization has been proved to be a very useful tool for the compression of image. However, the DWT is very computationally intensive process requiring innovative and computationally efficient method to obtain the image compression. The concurrent transformation of the image can be an important solution to this problem. This paper proposes a model of concurrent DWT for image compression. Additionally, the formal verification of the model has also been performed. Here the Symbolic Model Verifier (SMV) has been used as the formal verification tool. The system has been modeled in SMV and some properties have been verified formally.
", keywords = "Computation Tree Logic, Discrete WaveletTransform, Formal Verification, Image Compression,Symbolic Model Verifier.", volume = "3", number = "11", pages = "2594-10", }
