Paper Info
Title
An Algorithm for Compositional Nonblocking Verification of Extended Finite-State Machines.
Abstract
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 Abstract:ion. 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.
Year
DOI
Venue
2014
10.3182/20140514-3-FR-4046.00039
IFAC Proceedings Volumes
Keywords
DocType
Volume
Discrete event systems,extended finite-state machines,compositional verification,nonblocking,Abstraction
Conference
47
Issue
ISSN
Citations 
2
1474-6670
2
PageRank 
References 
Authors
0.40
9
3
Name
Order
Citations
PageRank
Sahar Mohajerani1375.18
Robi Malik225326.13
Martin Fabian320427.91