电子科技大学学报2011,Vol.40Issue(3):406-410,5.DOI:10.3969/j.issn.1001-0548.2011.03.016
基于动作细化的握手扩展
Handshaking Expansion Based on Action Refinement
摘要
Abstract
Handshaking expansion is a main procedure in the design of asynchronous circuits. At present,there is not description and definition for the refinement of handshaking expansion formality. Through investigating formal semantics of the handshaking expansion of asynchronous circuits, a refinement model for handshaking expansion is presented based on a powerful strategy of action refinement in the hierarchical design of concurrent systems. The proposed semantics employs wait event structures and then derives a true concurrency model with maximum parallelism. The refined system conforms to the original specification with respect to a vertical bisimulation relation. Furthermore, the refinement function preserves correctness and deadlock-freeness of the behavior in the refined system.关键词
并发系统/无死锁/握手扩展/真并发模型/等待事件结构Key words
concurrent system/ deadlock-freeness/ handshaking expansion/ true concurrency model/wait event structure分类
信息技术与安全科学引用本文复制引用
杨昕梅,孙秀莉,李绍荣..基于动作细化的握手扩展[J].电子科技大学学报,2011,40(3):406-410,5.基金项目
国家863计划(2007AA01Z143) (2007AA01Z143)