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...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Hindawi-IET
2023-02-01
|
| Series: | IET Software |
| Subjects: | |
| Online Access: | https://doi.org/10.1049/sfw2.12084 |
| _version_ | 1797429179004747776 |
|---|---|
| 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. |
| first_indexed | 2024-03-09T09:09:27Z |
| format | Article |
| id | doaj.art-df743275d7bc442ea74abb803b925254 |
| institution | Directory Open Access Journal |
| issn | 1751-8806 1751-8814 |
| language | English |
| last_indexed | 2024-03-09T09:09:27Z |
| publishDate | 2023-02-01 |
| publisher | Hindawi-IET |
| record_format | Article |
| series | IET Software |
| spelling | doaj.art-df743275d7bc442ea74abb803b9252542023-12-02T09:20:18ZengHindawi-IETIET 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 |