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
      • Computer Science Working Paper Series
      • 2013 Working Papers
      • View Item
      •   Research Commons
      • University of Waikato Research
      • Computing and Mathematical Sciences
      • Computer Science Working Paper Series
      • 2013 Working Papers
      • View Item
      JavaScript is disabled for your browser. Some features of this site may not work without it.

      Partial unfolding for compositional nonblocking verification of extended finite-state machines

      Mohajerani, Sahar; Malik, Robi; Fabian, Martin
      Thumbnail
      Files
      uow-cs-wp-2013-01.pdf
      288.5Kb
      Find in your library  
      Citation
      Export citation
      Mohajerani, S., Malik, R. & Fabian, M. (2012). Partial unfolding for compositional nonblocking verification of extended finite-state machines. (Working paper 01/2013). Hamilton, New Zealand: University of Waikato, Department of Computer Science.
      Permanent Research Commons link: https://hdl.handle.net/10289/7140
      Abstract
      This working paper describes a framework for compositional nonblocking verification of reactive systems modelled as extended finite-state machines. The nonblocking property can capture the absence of livelocks and deadlocks in concurrent systems. Compositional verification is shown in previous work to be effective to verify this property for large discrete event systems. Here, these results are applied to extended finite-state machines communicating via shared memory.

      The model to be verified is composed gradually, simplifying components through abstraction at each step, while conflict equivalence guarantees that the final verification result is the same as it would have been for the non-abstracted model. The working paper concludes with an example showing the potential of compositional verification to achieve substantial state-space reduction.
      Date
      2013-01-30
      Type
      Working Paper
      Series
      Computer Science Working Papers
      Report No.
      01/2013
      Publisher
      University of Waikato, Department of Computer Science
      Rights
      © 2013 Sahar Mohajerani, Robi Malik, Martin Fabian
      Collections
      • 2013 Working Papers [13]
      Show full item record  

      Usage

      Downloads, last 12 months
      25
       
       

      Usage Statistics

      For this itemFor all of Research Commons

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