Please use this identifier to cite or link to this item:
Title: Counterexample computation in compositional nonblocking verification
Authors: Malik, Robi
Ware, Simon
Keywords: Verification
DRNTU::Engineering::Electrical and electronic engineering
Issue Date: 2018
Source: Malik, R., & Ware, S. (2018). Counterexample computation in compositional nonblocking verification. IFAC-PapersOnLine, 51(7), 416-421. doi: 10.1016/j.ifacol.2018.06.334
Series/Report no.: IFAC-PapersOnLine
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.
ISSN: 2405-8963
DOI: 10.1016/j.ifacol.2018.06.334
Rights: © IFAC 2018. This work is posted here by permission of IFAC for your personal use. Not for distribution. The original version was published in, DOI: 10.1016/j.ifacol.2018.06.334
Fulltext Permission: open
Fulltext Availability: With Fulltext
Appears in Collections:EEE Journal Articles

Files in This Item:
File Description SizeFormat 
Counterexample computation in compositional nonblocking verification.pdf435.18 kBAdobe PDFThumbnail

Citations 50

Updated on Sep 7, 2020

Citations 20

Updated on Mar 4, 2021

Page view(s)

Updated on Jun 26, 2022

Download(s) 50

Updated on Jun 26, 2022

Google ScholarTM




Items in DR-NTU are protected by copyright, with all rights reserved, unless otherwise indicated.