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

An algorithm for compositional nonblocking verification of extended finite-state machines

Sahar Mohajerani (Institutionen för signaler och system, Automation) ; Robi Malik ; Martin Fabian (Institutionen för signaler och system, Automation)
12th IFAC/IEEE Workshop on Discrete Event Systems, WODES 2104, Cachan, France, 14-16 May 2014 (0065-3438). Vol. 12 (2014), p. 376-382.
[Konferensbidrag, refereegranskat]

This paper describes an approach for compositional nonblocking verification of discrete event systems modelled as extended finite-state machines (EFSM). Previous results about finite-state machines in lock-step synchronisation are generalised and applied to EFSMs communicating via shared variables. This gives rise to an EFSM-based conflict check algorithm that composes EFSMs gradually and partially unfolds variables as needed. At each step, components are simplified using conflict-equivalence preserving abstraction. The algorithm has been implemented in the discrete event systems tool Supremica. The paper presents experimental results for the verification of two scalable manufacturing system models, and shows that the EFSM-based algorithm verifies some large models faster than previously used methods.

Nyckelord: Abstraction, Compositional verification, Discrete event systems, Extended finite-state machines, Nonblocking

Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2016-01-18. Senast ändrad 2017-09-14.
CPL Pubid: 230846


Läs direkt!

Lokal fulltext (fritt tillgänglig)

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

Institutioner (Chalmers)

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



Chalmers infrastruktur