Concurrent software fine‐coarse‐grained automatic modelling by Coloured Petri Nets for model checking
Abstract The state space explosion restricts the error detection of concurrent software. The abstraction can provide a solution to avoid state space explosion, but it is easy to ignore important details, resulting in inaccurate detection results. This paper proposes a methodology of fine‐coarse‐grai...
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Wiley
2023-02-01
|
| Series: | IET Software |
| Subjects: | |
| Online Access: | https://doi.org/10.1049/sfw2.12084 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1832547396286939136 |
|---|---|
| author | Wenjie Zhong Jian‐tao Zhou Tao Sun |
| author_facet | Wenjie Zhong Jian‐tao Zhou Tao Sun |
| author_sort | Wenjie Zhong |
| collection | DOAJ |
| description | Abstract The state space explosion restricts the error detection of concurrent software. The abstraction can provide a solution to avoid state space explosion, but it is easy to ignore important details, resulting in inaccurate detection results. This paper proposes a methodology of fine‐coarse‐grained automatic modelling for Java source programs. By the principle that the execution details of property‐unchecked, non‐interactive, and unrelated statements do not affect the model checking results, we model coarse‐grained model fragments for such statements, while fine‐grained model fragments for property‐checked, interactive, and related statements. Our method reduces the model and state space and ensures the error detection of the source program based on model checking. Moreover, we prove the equivalence of the fine‐grained model, the coarse‐grained model, and the program. Finally, this paper gives an experiment to verify the effectiveness of the proposed method. |
| format | Article |
| id | doaj-art-df743275d7bc442ea74abb803b925254 |
| institution | Kabale University |
| issn | 1751-8806 1751-8814 |
| language | English |
| publishDate | 2023-02-01 |
| publisher | Wiley |
| record_format | Article |
| series | IET Software |
| spelling | doaj-art-df743275d7bc442ea74abb803b9252542025-02-03T06:45:06ZengWileyIET Software1751-88061751-88142023-02-01171557510.1049/sfw2.12084Concurrent software fine‐coarse‐grained automatic modelling by Coloured Petri Nets for model checkingWenjie Zhong0Jian‐tao Zhou1Tao Sun2College of Computer Science Inner Mongolia University Hohhot Inner Mongolia ChinaCollege of Computer Science Inner Mongolia University Hohhot Inner Mongolia ChinaCollege of Computer Science Inner Mongolia University Hohhot Inner Mongolia ChinaAbstract The state space explosion restricts the error detection of concurrent software. The abstraction can provide a solution to avoid state space explosion, but it is easy to ignore important details, resulting in inaccurate detection results. This paper proposes a methodology of fine‐coarse‐grained automatic modelling for Java source programs. By the principle that the execution details of property‐unchecked, non‐interactive, and unrelated statements do not affect the model checking results, we model coarse‐grained model fragments for such statements, while fine‐grained model fragments for property‐checked, interactive, and related statements. Our method reduces the model and state space and ensures the error detection of the source program based on model checking. Moreover, we prove the equivalence of the fine‐grained model, the coarse‐grained model, and the program. Finally, this paper gives an experiment to verify the effectiveness of the proposed method.https://doi.org/10.1049/sfw2.12084concurrency (computers)formal specificationpetri nets |
| spellingShingle | Wenjie Zhong Jian‐tao Zhou Tao Sun Concurrent software fine‐coarse‐grained automatic modelling by Coloured Petri Nets for model checking IET Software concurrency (computers) formal specification petri nets |
| title | Concurrent software fine‐coarse‐grained automatic modelling by Coloured Petri Nets for model checking |
| title_full | Concurrent software fine‐coarse‐grained automatic modelling by Coloured Petri Nets for model checking |
| title_fullStr | Concurrent software fine‐coarse‐grained automatic modelling by Coloured Petri Nets for model checking |
| title_full_unstemmed | Concurrent software fine‐coarse‐grained automatic modelling by Coloured Petri Nets for model checking |
| title_short | Concurrent software fine‐coarse‐grained automatic modelling by Coloured Petri Nets for model checking |
| title_sort | concurrent software fine coarse grained automatic modelling by coloured petri nets for model checking |
| topic | concurrency (computers) formal specification petri nets |
| url | https://doi.org/10.1049/sfw2.12084 |
| work_keys_str_mv | AT wenjiezhong concurrentsoftwarefinecoarsegrainedautomaticmodellingbycolouredpetrinetsformodelchecking AT jiantaozhou concurrentsoftwarefinecoarsegrainedautomaticmodellingbycolouredpetrinetsformodelchecking AT taosun concurrentsoftwarefinecoarsegrainedautomaticmodellingbycolouredpetrinetsformodelchecking |