首页> 外文会议>International Symposium on Automated Technology for Verification and Analysis(ATVA 2005); 20051004-07; Taibei(CT) >State Space Exploration of Object-Based Systems Using Equivalence Reduction and the Sweepline Method
【24h】

State Space Exploration of Object-Based Systems Using Equivalence Reduction and the Sweepline Method

机译:基于等价约简和扫描线方法的基于对象系统的状态空间探索

获取原文
获取原文并翻译 | 示例

摘要

Object-based systems present particular challenges for state space exploration. Objects can be dynamically created and discarded, and can be referenced via object identifiers. Consistent relabelling of object identifiers in a state leads to a state that is superficially different but behaviourally equivalent to the original. Similarly, object-based systems can include garbage which has no effect on subsequent behaviour but which results in unnecessary differentiation of states. Both of these factors can lead to state space explosion. This paper considers state space exploration for object-based systems based on the Petri Net formalism. It addresses the above issues by using both equivalence reduction and the sweep-line technique. Experimental results are presented for a simple case study of a communication protocol.
机译:基于对象的系统对状态空间探索提出了特殊的挑战。可以动态创建和丢弃对象,并且可以通过对象标识符进行引用。状态中对象标识符的一致重新标记导致表面上不同但行为上与原始状态等效的状态。同样,基于对象的系统可能包含垃圾,该垃圾不会影响后续行为,但会导致不必要的状态区分。这两个因素都可能导致状态空间爆炸。本文考虑了基于Petri网形式主义的基于对象系统的状态空间探索。它通过使用等效减少和扫掠线技术来解决上述问题。给出了针对通信协议的简单案例研究的实验结果。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号