ASIA unversity:Item 310904400/4773
English  |  正體中文  |  简体中文  |  全文笔数/总笔数 : 90570/105786 (86%)
造访人次 : 16363127      在线人数 : 337
RC Version 6.0 © Powered By DSPACE, MIT. Enhanced by NTU Library IR team.
搜寻范围 查询小技巧:
  • 您可在西文检索词汇前后加上"双引号",以获取较精准的检索结果
  • 若欲以作者姓名搜寻,建议至进阶搜寻限定作者字段,可获得较完整数据
  • 进阶搜寻


    jsp.display-item.identifier=請使用永久網址來引用或連結此文件: http://asiair.asia.edu.tw/ir/handle/310904400/4773


    题名: Model and Algorithm for Verification of High-Assurance Properties of Real-Time Systems
    作者: Jeffrey J. P. Tsai;E. Juan;A. Sahay
    日期: 2003-03
    上传时间: 2009-12-02 09:04:08 (UTC+8)
    出版者: Asia University
    摘要: 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.
    關聯: IEEE Transactions on Knowledge and Data Engineering 15(2):405-422
    显示于类别:[生物資訊與醫學工程學系 ] 期刊論文

    文件中的档案:

    档案 描述 大小格式浏览次数
    0KbUnknown355检视/开启
    310904400-4773.doc35KbMicrosoft Word193检视/开启


    在ASIAIR中所有的数据项都受到原著作权保护.


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