Counterexample computation in compositional nonblocking verification
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 a...
| Main Authors: | , |
|---|---|
| Other Authors: | |
| Format: | Journal Article |
| Language: | English |
| Published: |
2018
|
| Subjects: | |
| Online Access: | https://hdl.handle.net/10356/89807 http://hdl.handle.net/10220/47151 |
| _version_ | 1824456875811274752 |
|---|---|
| author | Malik, Robi Ware, Simon |
| author2 | School of Electrical and Electronic Engineering |
| author_facet | School of Electrical and Electronic Engineering Malik, Robi Ware, Simon |
| author_sort | Malik, Robi |
| collection | NTU |
| description | 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. |
| first_indexed | 2025-02-19T04:01:03Z |
| format | Journal Article |
| id | ntu-10356/89807 |
| institution | Nanyang Technological University |
| language | English |
| last_indexed | 2025-02-19T04:01:03Z |
| publishDate | 2018 |
| record_format | dspace |
| spelling | ntu-10356/898072020-03-07T13:57:31Z Counterexample computation in compositional nonblocking verification Malik, Robi Ware, Simon School of Electrical and Electronic Engineering Verification Validation DRNTU::Engineering::Electrical and electronic engineering 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. Published version 2018-12-21T02:21:37Z 2019-12-06T17:33:57Z 2018-12-21T02:21:37Z 2019-12-06T17:33:57Z 2018 Journal Article 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 2405-8963 https://hdl.handle.net/10356/89807 http://hdl.handle.net/10220/47151 10.1016/j.ifacol.2018.06.334 en IFAC-PapersOnLine © IFAC 2018. This work is posted here by permission of IFAC for your personal use. Not for distribution. The original version was published in ifac-papersonline.net, DOI: 10.1016/j.ifacol.2018.06.334 6 p. application/pdf |
| spellingShingle | Verification Validation DRNTU::Engineering::Electrical and electronic engineering Malik, Robi Ware, Simon Counterexample computation in compositional nonblocking verification |
| title | Counterexample computation in compositional nonblocking verification |
| title_full | Counterexample computation in compositional nonblocking verification |
| title_fullStr | Counterexample computation in compositional nonblocking verification |
| title_full_unstemmed | Counterexample computation in compositional nonblocking verification |
| title_short | Counterexample computation in compositional nonblocking verification |
| title_sort | counterexample computation in compositional nonblocking verification |
| topic | Verification Validation DRNTU::Engineering::Electrical and electronic engineering |
| url | https://hdl.handle.net/10356/89807 http://hdl.handle.net/10220/47151 |
| work_keys_str_mv | AT malikrobi counterexamplecomputationincompositionalnonblockingverification AT waresimon counterexamplecomputationincompositionalnonblockingverification |