KUKU

KU ScholarWorks

  • myKU
  • Email
  • Enroll & Pay
  • KU Directory
    • Login
    View Item 
    •   KU ScholarWorks
    • Engineering
    • Electrical Engineering and Computer Science Scholarly Works
    • View Item
    •   KU ScholarWorks
    • Engineering
    • Electrical Engineering and Computer Science Scholarly Works
    • View Item
    JavaScript is disabled for your browser. Some features of this site may not work without it.

    A formal specification and verification framework for Time Warp-based parallel simulation

    Thumbnail
    View/Open
    00979989.pdf (512.8Kb)
    Issue Date
    2002-01
    Author
    Frey, Peter
    Radhakrishnan, Radharamanan
    Carter, Harold. W.
    Wilsey, Philip A.
    Alexander, Perry
    Publisher
    IEEE COMPUTER SOC
    Type
    Article
    Metadata
    Show full item record
    Abstract
    This paper describes a formal framework developed using the Prototype Verification System (PVS) to model and verify distributed simulation kernels based on the Time Warp paradigm. The intent is to provide a common formal base from which domain specific simulators can be modeled, verified, and developed. PVS constructs are developed to represent basic Time Warp constructs. Correctness conditions for Time Warp simulation are identified describing causal ordering of event processing and correct rollback processing. The PVS theorem prover and type-check condition system are then used to verify all correctness conditions. In addition, the paper discusses the framework's reusability and extensibility properties in support of specification and verification of Time Warp extensions and optimizations.
    URI
    http://hdl.handle.net/1808/1591
    Collections
    • Electrical Engineering and Computer Science Scholarly Works [302]
    Citation
    Frey, P; Radhakrishnan, R; Carter, HW; Wilsey, PA; Alexander, P. A formal specification and verification framework for Time Warp-based parallel simulation. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING. January 2002. 28(1) : 58-78

    Items in KU ScholarWorks are protected by copyright, with all rights reserved, unless otherwise indicated.


    We want to hear from you! Please share your stories about how Open Access to this item benefits YOU.


    Contact KU ScholarWorks
    785-864-8983
    KU Libraries
    1425 Jayhawk Blvd
    Lawrence, KS 66045
    785-864-8983

    KU Libraries
    1425 Jayhawk Blvd
    Lawrence, KS 66045
    Image Credits
     

     

    Browse

    All of KU ScholarWorksCommunities & CollectionsThis Collection

    My Account

    LoginRegister

    Statistics

    View Usage Statistics

    Contact KU ScholarWorks
    785-864-8983
    KU Libraries
    1425 Jayhawk Blvd
    Lawrence, KS 66045
    785-864-8983

    KU Libraries
    1425 Jayhawk Blvd
    Lawrence, KS 66045
    Image Credits
     

     

    The University of Kansas
      Contact KU ScholarWorks
    Lawrence, KS | Maps
     
    • Academics
    • Admission
    • Alumni
    • Athletics
    • Campuses
    • Giving
    • Jobs

    The University of Kansas prohibits discrimination on the basis of race, color, ethnicity, religion, sex, national origin, age, ancestry, disability, status as a veteran, sexual orientation, marital status, parental status, gender identity, gender expression and genetic information in the University’s programs and activities. The following person has been designated to handle inquiries regarding the non-discrimination policies: Director of the Office of Institutional Opportunity and Access, IOA@ku.edu, 1246 W. Campus Road, Room 153A, Lawrence, KS, 66045, (785)864-6414, 711 TTY.

     Contact KU
    Lawrence, KS | Maps