Cargando…
Exact acceleration of complex real-time model checking based on overlapping cycle
When real-time systems are modeled as timed automata, different time scales may lead to substantial fragmentation of the symbolic state space. Exact acceleration solves the fragmentation problem without changing system reachability. The relatively mature technology of exact acceleration has been use...
Autores principales: | , , , , , |
---|---|
Formato: | Online Artículo Texto |
Lenguaje: | English |
Publicado: |
PeerJ Inc.
2020
|
Materias: | |
Acceso en línea: | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7924618/ https://www.ncbi.nlm.nih.gov/pubmed/33816923 http://dx.doi.org/10.7717/peerj-cs.272 |
_version_ | 1783659126814932992 |
---|---|
author | Wang, Guoqing Zhuang, Lei Song, Yu He, Mengyang Ma, Ding Ma, Ling |
author_facet | Wang, Guoqing Zhuang, Lei Song, Yu He, Mengyang Ma, Ding Ma, Ling |
author_sort | Wang, Guoqing |
collection | PubMed |
description | When real-time systems are modeled as timed automata, different time scales may lead to substantial fragmentation of the symbolic state space. Exact acceleration solves the fragmentation problem without changing system reachability. The relatively mature technology of exact acceleration has been used with an appended cycle or a parking cycle, which can be applied to the calculation of a single acceleratable cycle model. Using these two technologies to develop a complex real-time model requires additional states and consumes a large amount of time cost, thereby influencing acceleration efficiency. In this paper, a complex real-time exact acceleration method based on an overlapping cycle is proposed, which is an application scenario extension of the parking-cycle technique. By comprehensively analyzing the accelerating impacts of multiple acceleratable cycles, it is only necessary to add a single overlapping period with a fixed length without relying on the windows of acceleratable cycles. Experimental results show that the proposed timed automaton model is simple and effectively decreases the time costs of exact acceleration. For the complex real-time system model, the method based on an overlapping cycle can accelerate the large scale and concurrent states which cannot be solved by the original exact acceleration theory. |
format | Online Article Text |
id | pubmed-7924618 |
institution | National Center for Biotechnology Information |
language | English |
publishDate | 2020 |
publisher | PeerJ Inc. |
record_format | MEDLINE/PubMed |
spelling | pubmed-79246182021-04-02 Exact acceleration of complex real-time model checking based on overlapping cycle Wang, Guoqing Zhuang, Lei Song, Yu He, Mengyang Ma, Ding Ma, Ling PeerJ Comput Sci Real-Time and Embedded Systems When real-time systems are modeled as timed automata, different time scales may lead to substantial fragmentation of the symbolic state space. Exact acceleration solves the fragmentation problem without changing system reachability. The relatively mature technology of exact acceleration has been used with an appended cycle or a parking cycle, which can be applied to the calculation of a single acceleratable cycle model. Using these two technologies to develop a complex real-time model requires additional states and consumes a large amount of time cost, thereby influencing acceleration efficiency. In this paper, a complex real-time exact acceleration method based on an overlapping cycle is proposed, which is an application scenario extension of the parking-cycle technique. By comprehensively analyzing the accelerating impacts of multiple acceleratable cycles, it is only necessary to add a single overlapping period with a fixed length without relying on the windows of acceleratable cycles. Experimental results show that the proposed timed automaton model is simple and effectively decreases the time costs of exact acceleration. For the complex real-time system model, the method based on an overlapping cycle can accelerate the large scale and concurrent states which cannot be solved by the original exact acceleration theory. PeerJ Inc. 2020-05-04 /pmc/articles/PMC7924618/ /pubmed/33816923 http://dx.doi.org/10.7717/peerj-cs.272 Text en ©2020 Wang et al. https://creativecommons.org/licenses/by/4.0/ This is an open access article distributed under the terms of the Creative Commons Attribution License (https://creativecommons.org/licenses/by/4.0/) , which permits unrestricted use, distribution, reproduction and adaptation in any medium and for any purpose provided that it is properly attributed. For attribution, the original author(s), title, publication source (PeerJ Computer Science) and either DOI or URL of the article must be cited. |
spellingShingle | Real-Time and Embedded Systems Wang, Guoqing Zhuang, Lei Song, Yu He, Mengyang Ma, Ding Ma, Ling Exact acceleration of complex real-time model checking based on overlapping cycle |
title | Exact acceleration of complex real-time model checking based on overlapping cycle |
title_full | Exact acceleration of complex real-time model checking based on overlapping cycle |
title_fullStr | Exact acceleration of complex real-time model checking based on overlapping cycle |
title_full_unstemmed | Exact acceleration of complex real-time model checking based on overlapping cycle |
title_short | Exact acceleration of complex real-time model checking based on overlapping cycle |
title_sort | exact acceleration of complex real-time model checking based on overlapping cycle |
topic | Real-Time and Embedded Systems |
url | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7924618/ https://www.ncbi.nlm.nih.gov/pubmed/33816923 http://dx.doi.org/10.7717/peerj-cs.272 |
work_keys_str_mv | AT wangguoqing exactaccelerationofcomplexrealtimemodelcheckingbasedonoverlappingcycle AT zhuanglei exactaccelerationofcomplexrealtimemodelcheckingbasedonoverlappingcycle AT songyu exactaccelerationofcomplexrealtimemodelcheckingbasedonoverlappingcycle AT hemengyang exactaccelerationofcomplexrealtimemodelcheckingbasedonoverlappingcycle AT mading exactaccelerationofcomplexrealtimemodelcheckingbasedonoverlappingcycle AT maling exactaccelerationofcomplexrealtimemodelcheckingbasedonoverlappingcycle |