Progressive events in supervisory control and compositional verification
Simon Ware
Robi Malik
摘要:This paper investigates some limitations of the nonblocking property when used for supervisor synthesis in discrete event systems. It is shown that there are cases where synthesis with the nonblocking property gives undesired results. To address such cases, the paper introduces progressive events as a means to specify more precisely how a synthesised supervisor should complete its tasks. The nonblocking property is modified to take progressive events into account, and appropriate methods for verification and synthesis are proposed. Experiments show that progressive events can be used in the analysis of industrial-scale systems, and can expose issues that remain undetected by standard nonblocking verification.
机标关键词:discrete event systemsmethods forused in
论文发表日期:2014-01-01
在线出版日期:2025-08-15(本平台首次上网日期,不代表文献的发表时间)
页数:13( 317-329 )
英文信息
