An algorithm for compositional nonblocking verification using special events
详细信息 查看全文
- 作者：Colin Pilbrow cgp5@students.waikato.ac.nz" class="auth_mail" title="E-mail the corresponding author ; Robi Malik ; robi@waikato.ac.nz" class="auth_mail" title="E-mail the corresponding author
- 关键词：Discrete event systems ; Finite-state machines ; Model checking ; Compositional verification ; Nonblocking
- 刊名：Science of Computer Programming
- 出版年：2015
- 出版时间：1 December 2015
- 年：2015
- 卷：113
- 期：part_P2
- 页码：119-148
- 全文大小：1202 K
文摘
- •
The performance of compositional nonblocking verification is improved with special events.
- •
Special events help with abstraction by providing some information about the context.
- •
Conflict-preserving abstraction rules from previous work are generalised with special events.
- •
The proposed algorithm can verify several industrial-scale discrete event system models.