Trace analysis of protocols based on formal concurrent specifications

To increase the probability of computers communicating reliably with one another, protocol implementations must be tested for conformance to the standards on which they are based. Test case generation and trace analysis are two important topics in protocol testing research. Most of the work so far has focused on test case generation rather than trace analysis. Furthermore, most of the work has dealt only with the sequential aspects of the protocol specifications. In this thesis, a model that combines the two functions of test case generation and trace analysis in a unified framework is presented. The model, which is based on single module extended finite state machines, handles both control and data flows for single module specifications. Symbolic evaluation is used to detect and delete infeasible paths that may be generated. Practical considerations which may occur in a real test environment, such as out of order message sequences, are also addressed. A prototype implementation of the unified model was completed. The application of this method to X.25 LAPB shows that it can manage frame collision and control and data flows of the protocol rigorously. The model is extended to study the trace analysis of concurrent specifications based on multi-module extended finite state machines. This is done by introducing two additional models- concurrency and traceability. The concurrency model deals with concurrent properties such as concurrent events, concurrency blocks, global states, concurrency measures, deadlocks and data races which do not arise in sequential or single module specifications. The concurrency model allows a high-level abstraction to be used for understanding and analyzing concurrent behaviors. We also show how concurrency measures can be computed efficiently based on the concept of concurrency blocks. The traceability concept is needed to obtain the precise order of input/output messages of a module without state space explosion. This model for the trace analysis of concurrent specifications without translating them into their sequential equivalence is formalized and proposed for application to multi-module specification, multi-party testing and interoperability testing. The viability of the proposed methodology which can be applied to any specifications based on extended finite state machines is demonstrated using Estelle specifications in the thesis.Science, Faculty ofComputer Science, Department ofGraduat