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.

      Counterexample Computation in Compositional Nonblocking Verification

      Malik, Robi; Ware, Simon
      Thumbnail
      Files
      counterex.pdf
      Accepted version, 144.3Kb
      DOI
       10.1016/j.ifacol.2018.06.334
      Find in your library  
      Citation
      Export citation
      Malik, R., & Ware, S. (2018). Counterexample Computation in Compositional Nonblocking Verification. In IFAC PapersOnLine (Vol. 51, pp. 416–421). Elsevier. https://doi.org/10.1016/j.ifacol.2018.06.334
      Permanent Research Commons link: https://hdl.handle.net/10289/12563
      Abstract
      This paper describes algorithms to compute a counterexample when compositional nonblocking verification determines that a discrete event system is blocking. Counterexamples are an important feature of model checking that explains the cause of a detected problem, greatly helping users to understand and fix faults. In compositional verification, counterexamples are difficult to compute due to the large state space and the loss of information after abstraction. The paper explains the difficulties and proposes a solution, and experimental results show that counterexamples can be computed successfully for several industrial-scale systems.
      Date
      2018
      Type
      Conference Contribution
      Publisher
      Elsevier
      Rights
      This is the author's accepted version. © 2018, IFAC (International Federation of Automatic Control) Hosting by Elsevier Ltd.
      Collections
      • Computing and Mathematical Sciences Papers [1454]
      Show full item record  

      Usage

      Downloads, last 12 months
      76
       
       
       

      Usage Statistics

      For this itemFor all of Research Commons

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