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

Verification of Supervisory Control Properties of Finite Automata Extended with Variables

Alexey Voronov (Institutionen för signaler och system, Automation) ; Knut Åkesson (Institutionen för signaler och system, Automation)
Göteborg : Chalmers University of Technology, 2009. - 6 s.
[Rapport]

Verification and synthesis of control logic programs using Supervisory Control Theory (SCT) is an important topic. Most SCT methods are based on finite state automata (FA). FA extended with variables (EFA) are a compact, but otherwise equivalent to FA notation, proven to be beneficial in modeling control logic systems. To use existing SCT methods with EFA, it is necessary to convert EFA to FA. In certain cases this conversion can be very time-consuming, even if the number of resulting reachable states is very small compared to the total state-set of the system. In this paper we present a way to do verification of SCT properties of EFA models without converting them to FA. Instead, we convert them to the models for Symbolic Model Verification tool NuSMV. The conversion is performed in polynomial time. Experimental results show that NuSMV effectively utilizes small reachable state-set of the system to do verification.

Nyckelord: formal verification, supervisory control, finite automata, manufacturing systems, control logic, model checking



Denna post skapades 2009-05-26. Senast ändrad 2010-01-19.
CPL Pubid: 94442