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.

      Compositional nonblocking verification with always enabled events and selfloop-only events

      Pilbrow, Colin; Malik, Robi
      Thumbnail
      Files
      ftscs2013.pdf
      Accepted version, 172.8Kb
      DOI
       10.1007/978-3-319-05416-2_11
      Find in your library  
      Citation
      Export citation
      Pilbrow, C., & Malik, R. (2013). Compositional nonblocking verification with always enabled events and selfloop-only events. In C. Artho & P. C. Olveczky (Eds.), Preliminary Proceedings Second International Workshop on Formal Techniques for Safety-Critical Systems, Queenstown, NZ(pp. 147–162). Springer. http://doi.org/10.1007/978-3-319-05416-2_11
      Permanent Research Commons link: https://hdl.handle.net/10289/9201
      Abstract
      This paper proposes to improve compositional nonblocking verification through the use of 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, i.e., in the part of the system not being simplified. 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. 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
      2013-10-29
      Type
      Conference Contribution
      Publisher
      Springer
      Rights
      © 2013 Springer.
      Collections
      • Computing and Mathematical Sciences Papers [1455]
      Show full item record  

      Usage

      Downloads, last 12 months
      47
       
       
       

      Usage Statistics

      For this itemFor all of Research Commons

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