Data and Control Flow Analysis of VDMµ Specifications
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.
[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
[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
@article{"International Journal of Information, Control and Computer Sciences:61616", author = "Mubina Nazmeen and Iram Rubab", title = "Data and Control Flow Analysis of VDMµ Specifications", 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.", volume = "4", number = "4", pages = "806-6", }
