Formal analysis of timing behavior in test generation for computer and communication system

Inherent timing variables and constraints in typical communication protocols require new extended finite-state machine (EFSM) models to formally represent their behavior especially for test generation purposes. However, infeasible paths due to the conflicts among the timing condition and action variables in the timed EFSM models with the start and expiration of concurrent timers complicate the test generation process. In a test measurement laboratory, such timers, if not taken into account properly by formal methods at the test generation step, can generate false results by failing correct implementations, or worse, passing faulty ones. Multiple concurrent timers in communication protocols increase the complexity of conformance test generation due to conflicts imposed by the timing requirements for such timers.;A set of graph augmentation algorithms are introduced to model a class of timing faults in timed EFSM models. It is shown that the test sequences generated based on these models can detect 1-clock and n-clock timing faults, and incorrect timer setting faults for an implementation under test (IUT) in a test laboratory. The size of the augmented graph resulting from the algorithms introduced in this thesis is in the same order of magnitude as of the original graph. It is proven in this thesis that, the augmentations for single timing faults can also detect the presence of multiple faults occurring simultaneously.;Detection of multiple timing faults is a challenging task because these faults, although may be detectable individually, can mask each other's faulty behavior making a faulty IUT indistinguishable from a non-faulty one. This phenomenon called the fault masking problem, is formally defined in this thesis. Graph augmentation algorithms introduced to augment a timed EFSM with multiple timers for detection of a class of single timing faults can also be used for detecting multiple occurrences of these timing faults in the IUT. It is proven in this thesis that pairwise occurrences of these timing faults can be detected within the framework of the EFSM model.