Generating Counterexamples for Model Checking by Transformation
Counterexamples explain why a desired temporal logic property fails to hold. The generation of counterexamples is considered to be one of the primary advantages of model checking as a verification technique. Furthermore, when model checking does succeed in verifying a property, there is typically no...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2016-07-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1607.02227v1 |
| _version_ | 1818016758680780800 |
|---|---|
| author | G. W. Hamilton |
| author_facet | G. W. Hamilton |
| author_sort | G. W. Hamilton |
| collection | DOAJ |
| description | Counterexamples explain why a desired temporal logic property fails to hold. The generation of counterexamples is considered to be one of the primary advantages of model checking as a verification technique. Furthermore, when model checking does succeed in verifying a property, there is typically no independently checkable witness that can be used as evidence for the verified property. Previously, we have shown how program transformation techniques can be used for the verification of both safety and liveness properties of reactive systems. However, no counterexamples or witnesses were generated using the described techniques. In this paper, we address this issue. In particular, we show how the program transformation technique distillation can be used to facilitate the construction of counterexamples and witnesses for temporal properties of reactive systems. Example systems which are intended to model mutual exclusion are analysed using these techniques with respect to both safety (mutual exclusion) and liveness (non-starvation), with counterexamples being generated for those properties which do not hold. |
| first_indexed | 2024-04-14T07:17:03Z |
| format | Article |
| id | doaj.art-ae6a11c1e63a4361af6711a6ae723a7b |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-04-14T07:17:03Z |
| publishDate | 2016-07-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-ae6a11c1e63a4361af6711a6ae723a7b2022-12-22T02:06:16ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802016-07-01216Proc. VPT 2016658210.4204/EPTCS.216.4:9Generating Counterexamples for Model Checking by TransformationG. W. Hamilton0 School of Computing, Dublin City University, Republic of Ireland Counterexamples explain why a desired temporal logic property fails to hold. The generation of counterexamples is considered to be one of the primary advantages of model checking as a verification technique. Furthermore, when model checking does succeed in verifying a property, there is typically no independently checkable witness that can be used as evidence for the verified property. Previously, we have shown how program transformation techniques can be used for the verification of both safety and liveness properties of reactive systems. However, no counterexamples or witnesses were generated using the described techniques. In this paper, we address this issue. In particular, we show how the program transformation technique distillation can be used to facilitate the construction of counterexamples and witnesses for temporal properties of reactive systems. Example systems which are intended to model mutual exclusion are analysed using these techniques with respect to both safety (mutual exclusion) and liveness (non-starvation), with counterexamples being generated for those properties which do not hold.http://arxiv.org/pdf/1607.02227v1 |
| spellingShingle | G. W. Hamilton Generating Counterexamples for Model Checking by Transformation Electronic Proceedings in Theoretical Computer Science |
| title | Generating Counterexamples for Model Checking by Transformation |
| title_full | Generating Counterexamples for Model Checking by Transformation |
| title_fullStr | Generating Counterexamples for Model Checking by Transformation |
| title_full_unstemmed | Generating Counterexamples for Model Checking by Transformation |
| title_short | Generating Counterexamples for Model Checking by Transformation |
| title_sort | generating counterexamples for model checking by transformation |
| url | http://arxiv.org/pdf/1607.02227v1 |
| work_keys_str_mv | AT gwhamilton generatingcounterexamplesformodelcheckingbytransformation |