A framework for compositional nonblocking verification of extended finite-state machines

被引：0
作者：
Sahar Mohajerani
Robi Malik
Martin Fabian
机构：
[1] Volvo Cars Corporation,Vehicle Dynamics and Active Safety Center
[2] University of Waikato,Department of Computer Science
[3] Chalmers University of Technology,Department of Signals and Systems
来源：
Discrete Event Dynamic Systems | 2016年 / 26卷
关键词：
Extended finite-state machines; Model checking; Nonblocking; Compositional verification; Supervisory control theory;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
This paper presents a framework for compositional nonblocking verification of discrete event systems modelled as extended finite-state machines (EFSM). Previous results are improved to consider general conflict-equivalence based abstractions of EFSMs communicating both via shared variables and events. Performance issues resulting from the conversion of EFSM systems to finite-state machine systems are avoided by operating directly on EFSMs, deferring the unfolding of variables into state machines as long as possible. Several additional methods to abstract EFSMs and remove events are also presented. The proposed algorithm has been implemented in the discrete event systems tool Supremica, and the paper presents experimental results for several large EFSM models that can be verified faster than by previously used methods.
引用
收藏
页码：33 / 84
页数：51
相关论文
共 27 条
[1]  
Bryant RE(1992)Symbolic Boolean manipulation with ordered binary-decision diagrams ACM Comput Surv 24 293-318
[2]  
Flordal H(2009)Compositional verification in supervisory control SIAM J Control Optim 48 1914-1938
[3]  
Malik R(2000)On the complexity of supervisory control design in the RW framework IEEE Trans Syst Man Cybern 30 643-652
[4]  
Gohari P(2013)Compositional nonblocking verification using generalised nonblocking abstractions IEEE Trans Autom Control 58 1-13
[5]  
Wonham WM(2003)A case study in verification of UML statecharts: the PROFIsafe protocol Journal of Universal Computer Science 9 138-151
[6]  
Malik R(2006)Conflicts and fair testing Int J Found Comput Sci 17 797-813
[7]  
Leduc R(2009)Verification of nonconflict of supervisors using abstractions IEEE Trans Autom Control 54 2803-2815
[8]  
Malik R(1989)The control of discrete event systems Proc IEEE 77 81-98
[9]  
Mühlfeld R(2010)Nonconflict check by using sequential automaton abstractions based on weak observation equivalence Automatica 46 968-978
[10]  
Malik R(2012)Modeling and control of discrete event systems using finite state machines with variables and their applications in power grids Syst Control Lett 61 212-222
123