CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Compositional Verification in Supervisory Control

Hugo Flordal (Institutionen för signaler och system, Automation) ; R. Malik
SIAM Journal on Control and Optimization (0363-0129). Vol. 48 (2009), 3, p. 1914-1938.
[Artikel, refereegranskad vetenskaplig]

This paper proposes a compositional approach to verifying whether a large discrete event system is nonblocking. The new approach avoids computing the synchronous product of a large set of finite-state machines. Instead, the synchronous product is computed gradually, and intermediate results are simplified using conflict-preserving abstractions based on process-algebraic results about fair testing. Heuristics are used to choose between different possible abstractions. By translating the problem representation, the same method can also be applied to verify safety properties, in particular, controllability. Experimental results show that the method is applicable to finite-state machine models of industrial scale and brings considerable improvements in performance over other methods for nonblocking verification.

Nyckelord: discrete-event systems, supervisory control, nonblocking, model checking, discrete-event systems

Denna post skapades 2010-02-24.
CPL Pubid: 114658


Läs direkt!

Länk till annan sajt (kan kräva inloggning)

Institutioner (Chalmers)

Institutionen för signaler och system, Automation (2005-2017)



Chalmers infrastruktur