Abstract
Formal methods play an important part in the development as well as testing stages of software and hardware systems. A significant and often overlooked part of the process is the development of specifications and correctness requirements for the system under test. Traditionally, English has been used as the specification language, which has resulted in verbose and difficult to use specification documents that are usually abandoned during product development. This research focuses on investigating the use of Live Sequence Charts (LSCs), a graphical and intuitive language directly suited for expressing communication behaviors of a system as the specification language for a system under test. The research presents two methods for using LSCs as a specification language: first, by translating LSCs to temporal logic, and second, by translating LSCs to an automaton structure that is directly suited for formal verification of systems. The research first presents the translation for each method and further, identifies the pros and cons for each verification method.
Degree
PhD
College and Department
Physical and Mathematical Sciences; Computer Science
Rights
http://lib.byu.edu/about/copyright/
BYU ScholarsArchive Citation
Kumar, Rahul, "Using Live Sequence Chart Specifications for Formal Verification" (2008). Theses and Dissertations. 1500.
https://scholarsarchive.byu.edu/etd/1500
Date Submitted
2008-07-11
Document Type
Dissertation
Handle
http://hdl.lib.byu.edu/1877/etd2489
Keywords
specification, live sequence chart, scenario, verification, formal, model checking, translation, temporal logic, automata, buchi automata, unwinding, transformation
Language
English