Using Live Sequence Chart Specifications for Formal Verification

<p>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.</p>

Name thesis:degree_name

PhD

Grantor dc:publisher

Brigham Young University - Provo

Author dc:creator

• Kumar, Rahul

• specification
• live sequence chart
• scenario
• verification
• formal
• model checking
• translation
• temporal logic
• automata
• buchi automata
• unwinding
• transformation
• Computer Sciences

Language dc:language

English

Repository record dc:identifier

https://scholarsarchive.byu.edu/etd/1500

OAI identifier oai:identifier

oai:scholarsarchive.byu.edu:etd-2499