Research Commons
      • Browse 
        • Communities & Collections
        • Titles
        • Authors
        • By Issue Date
        • Subjects
        • Types
        • Series
      • Help 
        • About
        • Collection Policy
        • OA Mandate Guidelines
        • Guidelines FAQ
        • Contact Us
      • My Account 
        • Sign In
        • Register
      View Item 
      •   Research Commons
      • University of Waikato Research
      • Computing and Mathematical Sciences
      • Computing and Mathematical Sciences Papers
      • View Item
      •   Research Commons
      • University of Waikato Research
      • Computing and Mathematical Sciences
      • Computing and Mathematical Sciences Papers
      • View Item
      JavaScript is disabled for your browser. Some features of this site may not work without it.

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

      Mohajerani, Sahar; Malik, Robi; Fabian, Martin
      Thumbnail
      Files
      wodes2014.pdf
      Accepted version, 175.6Kb
      DOI
       10.3182/20140514-3-FR-4046.00039
      Find in your library  
      Citation
      Export citation
      Mohajerani, S., Malik, R., & Fabian, M. (2014). An algorithm for compositional nonblocking verification of extended finite-state machines. IFAC Proceedsing Volumes, 47(2), 237-382. http://doi.org/10.3182/20140514-3-FR-4046.00039
      Permanent Research Commons link: https://hdl.handle.net/10289/9016
      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 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.
      Date
      2014
      Type
      Conference Contribution
      Publisher
      IFAC
      Rights
      This is an author’s accepted version of a paper published in the Proceedings of the Twelfth International Workshop on Discrete Event Systems. © 2014 IFAC
      Collections
      • Computing and Mathematical Sciences Papers [1454]
      Show full item record  

      Usage

      Downloads, last 12 months
      74
       
       
       

      Usage Statistics

      For this itemFor all of Research Commons

      The University of Waikato - Te Whare Wānanga o WaikatoFeedback and RequestsCopyright and Legal Statement