{"id":{"repo_id":"wvu","oai_identifier":"oai:researchrepository.wvu.edu:etd-2107"},"canonical_url":"https://search.dev.ndltd.org/etd/wvu/oai:researchrepository.wvu.edu:etd-2107","repository":{"repo_id":"wvu","name":"West Virginia University","base_url":"https://researchrepository.wvu.edu/do/oai/"},"display":{"title":"Message sequence chart specifications with cross verification","abstract":"Current software specification verification methods are usually performed within the context of the specification method. There is little cross verification, pitting one type of specification against another, taking place. The most common techniques involve syntax checks across specifications or doing specification transformations and running verification within the new context. Since viewpoints of a system are different even within programming teams we concentrate on producing an efficient way to run cross verification on specifications, particularly specifications written with Message Sequence Charts and State Transition Diagrams.;In this work an algorithm is proposed in which all conditional MSCs are transformed into an algebraic representations, Message Flow Graphs and by stepwise refinement, a Global State Transition Graph is created. This GSTG has all the properties of a State Transition Diagram and therefore can be analyzed in conjunction with the original STD.","abstract_html":"Current software specification verification methods are usually performed within the context of the specification method. There is little cross verification, pitting one type of specification against another, taking place. The most common techniques involve syntax checks across specifications or doing specification transformations and running verification within the new context. Since viewpoints of a system are different even within programming teams we concentrate on producing an efficient way to run cross verification on specifications, particularly specifications written with Message Sequence Charts and State Transition Diagrams.;In this work an algorithm is proposed in which all conditional MSCs are transformed into an algebraic representations, Message Flow Graphs and by stepwise refinement, a Global State Transition Graph is created. This GSTG has all the properties of a State Transition Diagram and therefore can be analyzed in conjunction with the original STD.","abstract_has_math":false,"creators":["Boles, Timothy Shawn"],"institution":null,"degree_name":"MS","degree_level":"Thesis","degree_discipline":"Lane Department of Computer Science and Electrical Engineering","degree_department":null,"school":null,"contributors":["Bojan Cukic."],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2001,"date_issued":"2001-05-01T07:00:00Z","date_published":"2001-05-01T07:00:00Z","updated_at":"2026-07-24T06:15:16Z","subjects":["Computer science"],"languages":[],"rights":[],"rights_urls":[],"identifier_entries":[{"key":"dc:identifier","label":"Identifier","values":["https://researchrepository.wvu.edu/etd/1104"],"render_values":[{"text":"https://researchrepository.wvu.edu/etd/1104","href":"https://researchrepository.wvu.edu/etd/1104","code":true}]}]},"links":{"outbound_url":"https://doi.org/10.33915/etd.1104","outbound_label":"DOI","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Bojan Cukic."]},{"key":"dc:creator","label":"Author","values":["Boles, Timothy Shawn"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.available","label":"Dc Date Available","values":["2019-01-17T08:00:00Z"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Lane Department of Computer Science and Electrical Engineering"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["MS"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Computer science"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://doi.org/10.33915/etd.1104","https://researchrepository.wvu.edu/etd/1104"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["Current software specification verification methods are usually performed within the context of the specification method. There is little cross verification, pitting one type of specification against another, taking place. The most common techniques involve syntax checks across specifications or doing specification transformations and running verification within the new context. Since viewpoints of a system are different even within programming teams we concentrate on producing an efficient way to run cross verification on specifications, particularly specifications written with Message Sequence Charts and State Transition Diagrams.;In this work an algorithm is proposed in which all conditional MSCs are transformed into an algebraic representations, Message Flow Graphs and by stepwise refinement, a Global State Transition Graph is created. This GSTG has all the properties of a State Transition Diagram and therefore can be analyzed in conjunction with the original STD."]},{"key":"dc:title","label":"Title","values":["Message sequence chart specifications with cross verification"]}]}],"canonical_facts":{"dc:contributor":["Bojan Cukic."],"dc:creator":["Boles, Timothy Shawn"],"dc:date.available":["2019-01-17T08:00:00Z"],"dc:description.abstract":["Current software specification verification methods are usually performed within the context of the specification method. There is little cross verification, pitting one type of specification against another, taking place. The most common techniques involve syntax checks across specifications or doing specification transformations and running verification within the new context. Since viewpoints of a system are different even within programming teams we concentrate on producing an efficient way to run cross verification on specifications, particularly specifications written with Message Sequence Charts and State Transition Diagrams.;In this work an algorithm is proposed in which all conditional MSCs are transformed into an algebraic representations, Message Flow Graphs and by stepwise refinement, a Global State Transition Graph is created. This GSTG has all the properties of a State Transition Diagram and therefore can be analyzed in conjunction with the original STD."],"dc:identifier":["https://doi.org/10.33915/etd.1104","https://researchrepository.wvu.edu/etd/1104"],"dc:subject":["Computer science"],"dc:title":["Message sequence chart specifications with cross verification"],"thesis:degree_discipline":["Lane Department of Computer Science and Electrical Engineering"],"thesis:degree_level":["Thesis"],"thesis:degree_name":["MS"]},"updated_at":"2026-07-24T06:15:16Z"}