A framework for compositional nonblocking verification of extended finite-state machines
详细信息 查看全文
- 作者：Sahar Mohajerani ; Robi Malik ; Martin Fabian
- 关键词：Extended finite ; state machines ; Model checking ; Nonblocking ; Compositional verification ; Supervisory control theory
- 刊名：Discrete Event Dynamic Systems
- 出版年：2016
- 出版时间：March 2016
- 年：2016
- 卷：26
- 期：1
- 页码：33-84
- 全文大小：2,421 KB
- 参考文献：Åkesson K, Fabian M, Flordal H, Malik R (2006) Supremica—an integrated environment for verification, synthesis and simulation of discrete event systems. In: Proceedings of the 8th international workshop on discrete event systems, WODES’06. IEEE, Ann Arbor, pp 384–385
Aloul FA, Markov IL, Sakallah KA (2003) FORCE: A fast & easy-to-implement variable-ordering heuristic. In: Proceedings of the 13th ACM great lakes symposium on VLSI, pp. 116–119. Washington, DC, USA
Baier C, Katoen JP (2008) Principles of model checking. MIT Press
Bryant RE (1992) Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Comput Surv 24(3):293–318CrossRef
Chen Y, Lin F (2000) Modeling of discrete event systems using finite state machines with parameters. In: Proceedings of 2000 IEEE international conference on control applications (CCA). Anchorage, Alaska, pp 941–946
Cheng KT, Krishnakumar AS (1993) Automatic functional test generation using the extended finite state machine model.. In: Proceedings of the 30th ACM/IEEE design automation conference. doi:10.1145/157485.164585 , Dallas, pp 86–91
Dams D, Grumberg O, Gerth R (1994) Abstract interpretation of reactive systems: Abstractions preserving ∀CTL ∗, ∃CTL ∗ and CTL ∗. In: Olderog ER (ed) Proceedings of IFIP WG2.1/WG2.2/WG2.3 working conference on programming concepts, methods and calculi (PROCOMET), IFIP transactions. Elsevier, Amsterdam, pp 573–592
Fabian M, Fei Z, Miremadi S, Lennartson B, Åkesson K (2014). In: Campos J, Seatzu C, Xie X (eds) Supervisory control of manufacturing systems using extended finite automata, CRC Press
Flordal H, Malik R (2009) Compositional verification in supervisory control. SIAM J Control Optim 48(3):1914–1938. doi:10.1137/070695526 CrossRef MathSciNet MATH
Gohari P, Wonham WM (2000) On the complexity of supervisory control design in the RW framework. IEEE Trans Syst Man Cybern 30(5):643–652. doi:10.1109/3477.875441 CrossRef
Graf S, Steffen B (1990) Compositional minimization of finite state systems. In: Proceedings of the 1990 workshop on computer-aided verification, LNCS, vol 531. Springer, NJ, pp 186–196
Hoare CAR (1985) Communicating sequential processes. Prentice-Hall
Huth M, Ryan M (2004) Logic in computer science. University Press, CambridgeCrossRef MATH
Malik R, Leduc R (2013) Compositional nonblocking verification using generalised nonblocking abstractions. IEEE Trans Autom Control 58(8):1–13. doi:10.1109/TAC.2013.2248255 CrossRef MathSciNet
Malik R, Mühlfeld R (2003) A case study in verification of UML statecharts: the PROFIsafe protocol. Journal of Universal Computer Science 9(2):138–151
Malik R, Streader D, Reeves S (2006) Conflicts and fair testing. Int J Found Comput Sci 17(4):797–813. doi:10.1142/S012905410600411X CrossRef MathSciNet MATH
McMillan KL (1993) Symbolic model checking. Kluwer Academic Publishers, BostonCrossRef MATH
Milner R (1989) Communication and concurrency. Series in Computer Science. Prentice-Hall
Mohajerani S, Malik R, Fabian M (2013) Compositional nonblocking verification for extended finite-state automata using partial unfolding. In: Proceedings of the 9th international conference on automation science and engineering, CASE. Wisconsin Press, Madison, pp 942–947
Mohajerani S, Malik R, Fabian M (2013) Partial unfolding for compositional nonblocking verification of extended finite-state machines. Working Paper 01/2013, Department of Computer Science, University of Waikato. Hamilton, New Zealand. http://hdl.handle.net/10289/7140
Mohajerani S, Malik R, Fabian M (2014) An algorithm for compositional nonblocking verification of extended finite-state machines. In: Proceedings of the 12th international workshop on discrete event systems, WODES’14, pp. 376–382. Paris, France
Parsaeian S (2014) Implementation of a framework for restart after unforeseen errors in manufacturing systems. Master’s thesis, Chalmers University of Technology. Göteborg, Sweden
Pena PN, Cury JER, Lafortune S (2009) Verification of nonconflict of supervisors using abstractions. IEEE Trans Autom Control 54(12):2803–2815CrossRef MathSciNet
Ramadge PJG, Wonham WM (1989) The control of discrete event systems. Proc IEEE 77(1):81–98CrossRef
Sköldstam M, Åkesson K, Fabian M (2007) Modeling of discrete event systems using finite automata with variables. In: Proceedings of the 46th IEEE conference on decision and control, CDC ’07, pp. 3387– 3392
Su R, van Schuppen JH, Rooda JE, Hofkamp AT (2010) Nonconflict check by using sequential automaton abstractions based on weak observation equivalence. Automatica 46(6):968–978. doi:10.1016/j.automatica.2010.02.025 CrossRef MathSciNet MATH
Teixeira M, Malik R, Cury JER, de Queiroz MH (2013) Variable abstraction and approximations in supervisory control synthesis. In: 2013 American Control Conference, pp. 120–125. Washington, DC, USA
Vahidi A (2004) Efficient analysis of discrete event systems—supervisor synthesis with binary decision diagrams. Ph.D. thesis. Chalmers University of Technology, Göteborg
Wonham WM Supervisory control of discrete-event systems. http://www.control.utoronto.edu/
Zhaoa J, Chen YL, Chen Z, Lin F, Wang C, Zhang H (2012) Modeling and control of discrete event systems using finite state machines with variables and their applications in power grids. Syst Control Lett 61(1):212–222CrossRef - 作者单位：Sahar Mohajerani (1)
Robi Malik (2)
Martin Fabian (3)
1. Vehicle Dynamics and Active Safety Center, Volvo Cars Corporation, Göteborg, Sweden
2. Department of Computer Science, University of Waikato, Hamilton, New Zealand
3. Department of Signals and Systems, Chalmers University of Technology, Göteborg, Sweden - 刊物类别：Mathematics and Statistics
- 刊物主题：Mathematics
Systems Theory and Control
Operation Research and Decision Theory
Convex and Discrete Geometry
Electronic and Computer Engineering
Manufacturing, Machines and Tools - 出版者：Springer Netherlands
- ISSN：1573-7594
文摘
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.