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.

      A framework for compositional nonblocking verification of extended finite-state machines

      Mohajerani, Sahar; Malik, Robi; Fabian, Martin
      Thumbnail
      Files
      jdeds2014.pdf
      Accepted version, 474.8Kb
      DOI
       10.1007/s10626-015-0217-y
      Find in your library  
      Citation
      Export citation
      Mohajerani, S., Malik, R., & Fabian, M. (2016). A framework for compositional nonblocking verification of extended finite-state machines. DISCRETE EVENT DYNAMIC SYSTEMS-THEORY AND APPLICATIONS, 26(1), 33–84. http://doi.org/10.1007/s10626-015-0217-y
      Permanent Research Commons link: https://hdl.handle.net/10289/10146
      Abstract
      This paper presents a framework for compositional nonblocking verification of discrete event systems modelled as extended finite-state machines (EFSM). Previous results are improved to consider general conflict-equivalence based abstractions of EFSMs communicating both via shared variables and events. Performance issues resulting from the conversion of EFSM systems to finite-state machine systems are avoided by operating directly on EFSMs, deferring the unfolding of variables into state machines as long as possible. Several additional methods to abstract EFSMs and remove events are also presented. The proposed algorithm has been implemented in the discrete event systems tool Supremica, and the paper presents experimental results for several large EFSM models that can be verified faster than by previously used methods.
      Date
      2016-03-01
      Type
      Journal Article
      Publisher
      Springer
      Rights
      This is an accepted version of an article published in the journal: Discrete Event Dynamic Systems: Theory and Applications © 2015 Springer
      Collections
      • Computing and Mathematical Sciences Papers [1454]
      Show full item record  

      Usage

      Downloads, last 12 months
      163
       
       
       

      Usage Statistics

      For this itemFor all of Research Commons

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