• About
    • Login
    View Item 
    •   Institutional Repository Home
    • Electronic Theses and Dissertations
    • Electronic Theses and Dissertations
    • View Item
    •   Institutional Repository Home
    • Electronic Theses and Dissertations
    • Electronic Theses and Dissertations
    • View Item
    JavaScript is disabled for your browser. Some features of this site may not work without it.

    Browse

    All of Institutional RepositoryCommunities & CollectionsBy Issue DateAuthorsTitlesSubjectsDepartmentThis CollectionBy Issue DateAuthorsTitlesSubjectsDepartment

    My Account

    LoginRegister

    Behavioral Semantics of Modeling Languages: A Pragmatic Approach

    Balasubramanian, Daniel Allen
    : https://etd.library.vanderbilt.edu/etd-04082011-145057
    http://hdl.handle.net/1803/12061
    : 2011-04-18

    Abstract

    Domain-specific modeling languages (DSMLs) are specialized languages tailored with concepts and features of a particular domain. The abstractions offered by DSMLs allow designers of software systems to ignore implementation details and instead focus on the system at a high level. While higher levels of abstraction can offer many advantages, there are still unresolved issues with DSMLs. One of these is the difficulty of applying formal verification methods. This dissertation presents two contributions that assist with the formal verification of domain-specific models. The first is a unified framework in which Statechart models of different semantic variants can be defined, simulated and verified. The key idea is that the user describes only the structure of a model, and then selects the semantics from a set of pluggable components. This allows a single model to be executed using multiple semantics, and a system comprised of interacting models using different semantics can be simulated and verified in a single environment. A lightweight method for specifying properties based on a pattern system was also developed. To perform analysis, the framework is integrated with Java Pathfinder, a software model checker, and Symbolic Pathfinder, its symbolic execution engine. Symbolic execution allows both test-vector generation and reachability analysis. The second major contribution is an extension to Formula, a modeling language and analysis tool from Microsoft Research, that calculates execution traces of models. The behavioral semantics are defined as a set of model transformations, each of which represents an atomic step of execution. The trace computing extension consists of three components. The first is a component that applies all applicable transformations to an input model at a given step and creates a separate trace for each application. The second component is used to create a separate trace for each non-deterministic choice of the input parameters that are passed to a transformation, making non-determinism inside a single execution step explicit to the trace computing module. The third component stores execution traces efficiently by computing and storing only the differences between consecutive steps in a trace when possible.
    Show full item record

    Files in this item

    Icon
    Name:
    DanielDissertation.pdf
    Size:
    5.654Mb
    Format:
    PDF
    View/Open

    This item appears in the following collection(s):

    • Electronic Theses and Dissertations

    Connect with Vanderbilt Libraries

    Your Vanderbilt

    • Alumni
    • Current Students
    • Faculty & Staff
    • International Students
    • Media
    • Parents & Family
    • Prospective Students
    • Researchers
    • Sports Fans
    • Visitors & Neighbors

    Support the Jean and Alexander Heard Libraries

    Support the Library...Give Now

    Gifts to the Libraries support the learning and research needs of the entire Vanderbilt community. Learn more about giving to the Libraries.

    Become a Friend of the Libraries

    Quick Links

    • Hours
    • About
    • Employment
    • Staff Directory
    • Accessibility Services
    • Contact
    • Vanderbilt Home
    • Privacy Policy