Home
    • Login
    View Item 
    •   TDL DSpace Home
    • Federated Electronic Theses and Dissertations
    • University of Texas at Austin
    • View Item
    •   TDL DSpace Home
    • Federated Electronic Theses and Dissertations
    • University of Texas at Austin
    • View Item
    JavaScript is disabled for your browser. Some features of this site may not work without it.

    Modeling and formal verification of gaming storylines

    Thumbnail
    Date
    2016-05
    Author
    Holloway, Lane Thomas
    0000-0002-1564-228X
    Metadata
    Show full item record
    Abstract
    Video games are becoming more and more interactive with increasingly complex plots. These plots typically involve multiple parallel storylines that may converge and diverge based on player actions. This may lead to situations that are inconsistent or impassable. Current techniques for planning and testing game plots involve naive means such as text documents, spreadsheets, and critical path testing. Recent academic research [1] [2] [3] examines the design planning problems, but neglect testing and verification of the possible plot lines. These complex plots have thus until now been handled inadequately due to a lack of a formal methodology and tools to support them. In this dissertation, we describe how we develop methods to 1) characterize storylines (SChar), 2) define a storyline description language (SDL), and 3) create a storyline verification tool based in formal verification techniques (StoCk) that use our SDL as input. SChar (Storyline Characterization) help game developers characterize the category of story line they are working on (e.g. linear, branching and plot) through a tool that give a set of guided questions. Our SDL allows its users to describe storylines in a consistent format similar to how they reason about storylines, but in such a way that it can be used for formal verification. StoCk accepts storylines, described in SDL, to be formally verified using SPIN for errors. StoCk is also examined in three common use cases found in the gaming industry used as a tool 1) during storyline creation 2) during quality assurance and 3) during storyline implementation. The combination of SChar, SDL, and StoCk provides designers, writers, and developers a novel methodology and tools to verify consistency in large and complex game plots.
    URI
    http://hdl.handle.net/2152/41455
    Collections
    • University of Texas at Austin

    DSpace software copyright © 2002-2016  DuraSpace
    Contact Us | Send Feedback
    TDL
    Theme by @mire NV
     

     

    Browse

    All of DSpaceCommunities & CollectionsBy Issue DateAuthorsTitlesSubjectsThis CollectionBy Issue DateAuthorsTitlesSubjects

    My Account

    Login

    DSpace software copyright © 2002-2016  DuraSpace
    Contact Us | Send Feedback
    TDL
    Theme by @mire NV