Data and Control Flow Analysis of VDMµ Specifications

Authors: Mubina Nazmeen, Iram Rubab

Abstract:

Formal Specification languages are being widely used for system specification and testing. Highly critical systems such as real time systems, avionics, and medical systems are represented using Formal specification languages. Formal specifications based testing is mostly performed using black box testing approaches thus testing only the set of inputs and outputs of the system. The formal specification language such as VDMµ can be used for white box testing as they provide enough constructs as any other high level programming language. In this work, we perform data and control flow analysis of VDMµ class specifications. The proposed work is discussed with an example of SavingAccount.

Keywords: VDM-SL, VDMµ, data flow graph, control flowgraph, testing, formal specification.

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1079488

References:

[1] Cliff B. Jones. "Systematic Software Development Using VDM" Prentice-Hall International, Englewood Cliffs, New Jersey, second edition, 1990.
[2] Elmstrom.R, Larsen.P.G and Lassen.P.B "The IFAD VDM-SL Toolbox: A Practical Approach to Formal Specification" ACM SIGPLAN Notices, Volume 29,September 1994.
[3] Sten Agerholm, Pierre-Jean Lecoeur, and Etienne Reichert.H. "Formal specification and validation at work: A case study using VDM-SL" In Proceedings of Second Workshop on Formal Methods in Software Practice, Florida, Marts. ACM, 1998.
[4] Nadeem, A., Rehman, M. J. "Framework for Automated Testing from VDM-SL Specifications" In proceedings of the 8th IEEE-INMIC Conference (INMIC 2004), Lahore, Pakistan, December 2004.
[5] Nadem.A and Rehman.M.J."TESTAF: A Test automation Framework for class testing using object oriented formal specifications".Journal of universal computer science vol 11issue 6, 2005.
[6] Georg Droschl. "Design and Application of a Test Case Generator for VDM-SL" Austrian Research Center Scibcrsdorf and IST - Techniscal University of Graz a Austria. 1999.
[7] Bernhard K. Aichering."Automated Black-Box Testing with Abstract VDM Oracles".In M. Felici, K. Kanoun and A. Pasquini Editors, Computer Safety,reliability and security: proceedings of the 18th international conference, SAFECOMP-1999, Toulouse, France, September 1999, volume 1698 of lecture notes in computer science, pages 250-259. Springer, 1999.
[8] J. S. Fitzgerald, P. G. Larsen, S. Tjell, and M. Werhoef."Validation Support for Real- Time Embedded Systems in VDM++".Technical Report CS-TR-1017, School of computing Science, Newcastle University, April 2007. Revised Version to appear in Proc. 10th IEEE High Assurance System Engineering Symposium, November, 2007, Dallas, Texas, IEEE .
[9] Nadeem. A, Micheal R. Lyu. "A Framework for inheritance testing From VDM++ Specifications".12th Pacific Rim International Symposium on Dependable Computing (PRDC-06). IEEE, 2006.
[10] Nadeem. A, Malik.Z Micheal R. Lyu. "A Framework for inheritance and polymorphic Testing using a VDM++ Specifications"12th Pacific Rim International Symposium on Dependable Computing (PRDC-06). IEEE, 2006.
[11] J. Dick and A. Faivre."Automating the Generation and Sequencing of test cases from model-based specifications"In J. C. P. Woodcock and P. G. Larsen, editors, FME-93: Industrial-strength formal methods, pages 268-284. Formal Methods Europe, Springer Verlag, April 1993. Lecture Notes in Computer Science 670.
[12] G. T Scullard."Test Case Selection using VDM" In R. Bloomfield, L. Marshall, and R. Jone, editors, VDM88:VDM-The way ahead, number 328 in lecture notes in computer sciences pages 718-186 VDM Europe, Springer Verlag, September 1988.
[13] J. Offut, R. Alexander, Y. Wu, Q. Xiao, C. Hutchinson. A Fault Model for Subtype Inheritance and Polymorphism. The Twelfth IEEE International Symposium on Software Reliability Engineering (ISSRE-01), pages 89-95, Hong Kong PRC, November 2001.
[14] J. M. Wing. "A Specifier-s Introduction to Formal Methods".IEEE Computer, vol.7, No.5,. Pages 8-4 September 1990.
[15] Verhoef. M, Larsen. P.G and Hooman.J."Modeling and Validating Distributed Embedded Real-Time Systems with VDM++" Proceeding of FN 2006; Formal Methods, August, 2006. Springer, LNCS 4085, pp 147-162.
[16] Fitzgerald, J., Larsen, P.G., Mukherjee, P., Plat,N., Verhoef, M., Validated Designs for ObjectorientedSystems, Springer-Verlag, 2005, ISBN 1-85233-881-4.
[17] VDMTools: The VDM++ Language, version 6.8.1, CSK Corporation, 2005.
[18] Rapps and E. J. Weyuker, "Selecting Software Test Data Using Data Flow Information," IEEE Trans. Software Engineering, vol. SE-11, no. 4, April, 1985, pp. 367-375.
[19] Macedu.H.D, Larsen.P.G and Fitzgerald.J. "Incremental Development of a distributed Real-Time model of a cardiac pacing system using VDM" University of New Castle upon Tyne, computing Science, Technical Report Series, No. CS-TR-1059, November 2007.
[20] J.-R. Abrial. "The B-Book, Assigning programs to meanings". Cambridge UniversityPress, 1996. ISBN 0521 49619 5(hardback).
[21] J. M. Spivey. The Z Notation. Series in Computer Science. Prentice- Hall, 1989.
[22] Glenford , J. Myers. "The art of software testing" Wiley series in business data processing, John Willey and sons,1979.
[23] Singh.H, M.Conrad and S. Sadeghipour. "Test case design based on Z and the classification-tree method" .IEEE, 1997