{"id":{"repo_id":"ubc","oai_identifier":"oai:circle.library.ubc.ca:2429/1866"},"canonical_url":"https://search.dev.ndltd.org/etd/ubc/oai:circle.library.ubc.ca:2429/1866","repository":{"repo_id":"ubc","name":"University of British Columbia","base_url":"http://circle.library.ubc.ca/oai/request"},"display":{"title":"Trace analysis of protocols based on formal concurrent specifications","abstract":"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.","abstract_html":"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.","abstract_has_math":false,"creators":["Kim, Myungchul"],"institution":"University of British Columbia","degree_name":"Doctor of Philosophy - PhD","degree_level":"doctoral","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":[],"advisors":[],"committee_chairs":[],"committee_members":[],"year":1993,"date_issued":"1993","date_published":"1993","updated_at":"2026-07-24T05:07:28Z","subjects":[],"languages":["eng"],"rights":["For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use."],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2429/1866","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:creator","label":"Author","values":["Kim, Myungchul"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["1993"]},{"key":"dc:publisher","label":"Institution","values":["University of British Columbia"]},{"key":"dc:type","label":"Dc Type","values":["Text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["doctoral"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Doctor of Philosophy - PhD"]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of British Columbia"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use."]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2429/1866","http://circle.library.ubc.ca/bitstream/2429/1866/1/ubc_1993_spring_phd_kim_myungchul.pdf"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["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."]},{"key":"dc:format","label":"Dc Format","values":["5592946","application/pdf"]},{"key":"dc:title","label":"Title","values":["Trace analysis of protocols based on formal concurrent specifications"]}]}],"canonical_facts":{"dc:creator":["Kim, Myungchul"],"dc:date":["1993"],"dc:description":["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."],"dc:format":["5592946","application/pdf"],"dc:identifier":["http://hdl.handle.net/2429/1866","http://circle.library.ubc.ca/bitstream/2429/1866/1/ubc_1993_spring_phd_kim_myungchul.pdf"],"dc:language":["eng"],"dc:publisher":["University of British Columbia"],"dc:rights":["For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use."],"dc:title":["Trace analysis of protocols based on formal concurrent specifications"],"dc:type":["Text"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["doctoral"],"thesis:degree_name":["Doctor of Philosophy - PhD"],"thesis:institution_name":["University of British Columbia"]},"updated_at":"2026-07-24T05:07:28Z"}