K.Bogdanov's Ph.D. thesis

The work attempts to provide a flexible method to improve the quality of software development, by improvement in testing. It shows how a formal testing method can be applied to the statechart notation widely used in industry. The method focuses on testing implementations against statechart designs and, subject to certain specific requirements, allows us to prove that the implementation is behaviourally equivalent to the design, by testing. The described testing method is based on the X-machine testing method and utilises the `divide and conquer' strategy to testing different features of statecharts.

A design of a software system can be built top-down in a sequence of refinements, i.e. constrained additions of some detail. If the implementation is developed in parallel, certain faults become impossible. This allows us to reduce the size of a test set dramatically.

The prototype implementation of the testing method has been built and case studies evaluating its applicability to parts of real systems were successful.

The thesis is available as gzipped postscript or as pdf.

Errata:

What was wrong Where corrected

The first phase of the Wp method was not using the united Wi sets. FATES'2002 paper.

Missing requirement for interlevel transitions entering AND-states to either terminate at an AND-state boundary or contain a substate of each substate of those AND-states in that transition's set of target states. SFEDL'2002 paper

K.Bogdanov (replace _ in the email address with @)

Last modified: Mon Dec 30 22:40:40 GMT 2002

What was wrong	Where corrected
The first phase of the Wp method was not using the united Wi sets.	FATES'2002 paper.
Missing requirement for interlevel transitions entering AND-states to either terminate at an AND-state boundary or contain a substate of each substate of those AND-states in that transition's set of target states.	SFEDL'2002 paper