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 using special events

      Pilbrow, Colin; Malik, Robi
      Thumbnail
      Files
      Science of Computer Programming 113.pdf
      Accepted version, 422.5Kb
      DOI
       10.1016/j.scico.2015.05.010
      Find in your library  
      Citation
      Export citation
      Pilbrow, C., & Malik, R. (2015). An algorithm for compositional nonblocking verification using special events. Science of Computer Programming, 113, 119–148. http://doi.org/10.1016/j.scico.2015.05.010
      Permanent Research Commons link: https://hdl.handle.net/10289/10586
      Abstract
      This paper proposes to improve compositional nonblocking verification of discrete event systems through the use of special 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, i.e., in the part of the system not being simplified. Here, it is proposed to exploit more knowledge about the remainder of the system and check how events are being used. Always enabled events, selfloop-only events, failing events, and blocked events are easy to detect and often help with simplification even though they are used in the remainder of the system. Abstraction rules from previous work are generalised, and experimental results demonstrate the applicability of the resulting algorithm to verify several industrial-scale discrete event system models, while achieving better state-space reduction than before.
      Date
      2015-12-01
      Type
      Journal Article
      Publisher
      Elsevier Science
      Rights
      This is an author’s accepted version of an article published in the journal: Science of Computer Programming. © 2015 Elsevier.
      Collections
      • Computing and Mathematical Sciences Papers [1455]
      Show full item record  

      Usage

      Downloads, last 12 months
      93
       
       
       

      Usage Statistics

      For this itemFor all of Research Commons

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