Semester
Spring
Date of Graduation
2001
Document Type
Thesis
Degree Type
MS
College
Statler College of Engineering and Mineral Resources
Department
Lane Department of Computer Science and Electrical Engineering
Committee Chair
Bojan Cukic.
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.
Recommended Citation
Boles, Timothy Shawn, "Message sequence chart specifications with cross verification" (2001). Graduate Theses, Dissertations, and Problem Reports. 1104.
https://researchrepository.wvu.edu/etd/1104