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.