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.

      Compositional nonblocking verification with always enabled and selfloop-only events

      Pilbrow, Colin
      Thumbnail
      Files
      uow-cs-wp-2013-07.pdf
      259.5Kb
      Find in your library  
      Citation
      Export citation
      Pilbrow, C. (2013). Compositional nonblocking verification with always enabled and selfloop-only events. (Working paper 07/2013). Hamilton, New Zealand: University of Waikato, Department of Computer Science.
      Permanent Research Commons link: https://hdl.handle.net/10289/8187
      Abstract
      This report proposes to improve compositional nonblocking verification through the use of two special event types: always enabled and selfloop-only events. Compositional verification involves abstraction to simplify parts of a system during verification. Normally, this abstraction is based on the set of events not used in the remainder of the system. Here, it is proposed to exploit more knowledge about the system and abstract events even though they are used in the remainder of the system. This can lead to more simplification than was previously possible. Abstraction rules from previous work are extended to respect the new special events and proofs show these rules still preserve nonblocking. The rules have been implemented in Waters and experimental results demonstrate that these extended simplification rules help verify several industrial-scale discrete event system models while achieving better state-space reduction than before.
      Date
      2013-11-19
      Type
      Working Paper
      Series
      Computer Science Working Papers
      Report No.
      07/2013
      Publisher
      University of Waikato, Department of Computer Science
      Rights
      © 2013 Colin Pilbrow
      Collections
      • 2013 Working Papers [13]
      Show full item record  

      Usage

      Downloads, last 12 months
      51
       
       

      Usage Statistics

      For this itemFor all of Research Commons

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