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.

    Integration of model checking into software development processes

    Thumbnail
    Date
    2004
    Author
    Xie, Fei
    Metadata
    Show full item record
    Abstract
    Testing has been the dominant method for validation of software systems. As software systems become complex, conventional testing methods have become inadequate. Model checking is a powerful formal verification method. It supports systematic exploration of all states or execution paths of the system being verified. There are two major challenges in practical and scalable application of model checking to software systems: (1) the applicability of model checking to software systems and (2) the intrinsic complexity of model checking. In this dissertation, we have developed a comprehensive approach to integration of model checking into two emerging software development processes: ModelDriven Development (MDD) and Component-Based Development (CBD), and a combination of MDD and CBD. This approach addresses the two major challenges under the following framework: (1) bridging applicability gaps through automatic translation of software representations to directly model-checkable formal representations, (2) seamless integration of state space reduction algorithms in the translation through static analysis, and (3) scaling model checking capability and achieving state space reduction by systematically exploring compositional structures of software systems. We have integrated model checking into MDD by applying mature model checking techniques to industrial design-level software representations through automatic translation of these representations to the input formal representations of model checkers. We have developed a translation-based approach to compositional reasoning of software systems, which simplifies the proof, implementation, and application of compositional reasoning rules at the software system level by reusing the proof and implementation of existing compositional reasoning rules for directly model-checkable formal representations. We have developed an integrated state space reduction framework which systematically conducts a top-down decomposition of a large and complex software system into directly model-checkable components by exploring domain-specific knowledge. We have designed, implemented, and applied a bottom-up approach to model checking of component-based software systems, which composes verified systems from verified components and integrates model checking into CBD. We have further scaled model checking of componentbased systems by exploring the synergy between MDD and CBD, i.e., specifying components in executable design languages, and realizing the bottom-up approach based on model checking of software designs through translation.
    URI
    http://hdl.handle.net/2152/1458
    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