Message sequence chart specifications with cross verification

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.

Name thesis:degree_name

MS

Level thesis:degree_level

Thesis

Discipline thesis:degree_discipline

Lane Department of Computer Science and Electrical Engineering

Year dc:date.available

2001

Author dc:creator

• Boles, Timothy Shawn

Contributors dc:contributor

• Bojan Cukic.

• Computer science

Identifier

https://researchrepository.wvu.edu/etd/1104

OAI identifier oai:identifier

oai:researchrepository.wvu.edu:etd-2107