English  |  正體中文  |  简体中文  |  Items with full text/Total items : 92958/108462 (86%)
Visitors : 20436925      Online Users : 195
RC Version 6.0 © Powered By DSPACE, MIT. Enhanced by NTU Library IR team.
Scope Tips:
  • please add "double quotation mark" for query phrases to get precise results
  • please goto advance search for comprehansive author search
  • Adv. Search
    HomeLoginUploadHelpAboutAdminister Goto mobile version

    Please use this identifier to cite or link to this item: http://asiair.asia.edu.tw/ir/handle/310904400/4773

    Title: Model and Algorithm for Verification of High-Assurance Properties of Real-Time Systems
    Authors: Jeffrey J. P. Tsai;E. Juan;A. Sahay
    Date: 2003-03
    Issue Date: 2009-12-02 09:04:08 (UTC+8)
    Publisher: Asia University
    Abstract: In this paper, we present a new compositional verification methodology for efficiently verifying high-assurance properties such as reachability and deadlock freedom of real-time systems. In this methodology, each component of real-time systems is initially specified as a timed automaton and it communicates with other components via synchronous and/or asynchronous communication channels. Then, each component is analyzed by a generation of its state-space graph which is formalized as a new state-space representation model called Multiset Labeled Transition Systems (MLTSs). Afterward, the state spaces of the components are hierarchically composed and simplified through a composition algorithm and a set of condensation rules, respectively, to get a condensed state space of the system. The simplified state spaces preserve equivalence with respect to deadlock and reachable states. Such equivalence is assured by our reduction theories called IOT-failure equivalence and IOT-state equivalence. To show the performance of our methodology, we developed a verification tool RT-IOTA and carried out experiments on some benchmarks such as CSMA/CD protocol, a rail-road crossing, an alternating bit-protocol, etc. Specifically, we look at the time taken to generate the statespace, the size of the state space, and the amount of reduction achieved by our condensation rules. The results demonstrate the strength of our new technique in dealing with the state-explosion problem.
    Relation: IEEE Transactions on Knowledge and Data Engineering 15(2):405-422
    Appears in Collections:[生物資訊與醫學工程學系 ] 期刊論文

    Files in This Item:

    File Description SizeFormat
    310904400-4773.doc35KbMicrosoft Word210View/Open

    All items in ASIAIR are protected by copyright, with all rights reserved.

    DSpace Software Copyright © 2002-2004  MIT &  Hewlett-Packard  /   Enhanced by   NTU Library IR team Copyright ©   - Feedback