Fault Modeling and Detection Capabilities for EFSM Models

摘要

Inherent timing variables and constraints in communication protocols require new extended finite-state machine (EFSM) models to formally represent their behavior, particularly 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 activation and expiration of concurrent timers complicate the test generation process. In a test measurement laboratory, such timers, if not properly taken into account by formal methods at the test generation step, can generate false results by failing correct implementations or, worse, passing faulty implementations. This paper analyzes the fault detection capability of the timed EFSM models introduced in our earlier work in the presence of multiple timing faults. It is proven that, for a class of timing faults, test sequences generated from our models can detect multiple occurrences of pairwise combinations of such faults. A simplified version of the Session Initiation Protocol (SIP) registration process, which is widely used by Voice over IP (VoIP) telephones, has been used as a working example throughout this paper.