Abstract:
The rapidly growing applications of software in critical systems such as railways,
aviation, automobiles, and medicine, demand a much higher level of reliability and error-
free operation. The use of formal methods in such applications not only helps avoid
specification errors, ambiguities, and inconsistencies in early phases of software life
cycle, but also provides a sound basis for generation of an effective set of test cases.
However, the existing research on formal specification based testing has focused on unit
level testing only.
This research is aimed at automating the generation of class level as well as integration
level test cases for an object-oriented system using formal specifications. We use
VDM++ formal specification language for this purpose. As a result of our research, we
present a framework, called SpecTGS, that automatically generates specification based
test cases for object-oriented systems using VDM++ as the specification language. For
class testing, the SpecTGS uses the trace structure definition of a VDM++ class
specification to derive allowable method call sequences, and partition analysis to generate
test data. For integration testing, we have proposed a novel idea that extracts testing
information from the VDM++ specification and UML communication diagrams. The
SpecTGS derives message sequences from a UML communication diagram, and uses the
VDM++ specification to construct state invariants for the states in which a class can
receive a message. A new strategy for constructing sub-states from a state invariant called
partitioned boundary state coverage that combines two existing strategies, i.e. partition
ivanalysis strategy and the boundary state coverage strategy. Each message sequence
generated from the UML communication diagrams is combined with the sub-states to
construct a test model. The test model is then used to derive the test paths under various
coverage criteria. A proof-of-concept tool has been developed to implement and evaluate
the SpecTGS framework. The results for the integration testing approach have been
shown for a real-life case study selected from the literature.
