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...

Descripción completa

Detalles Bibliográficos
Autores principales: Wang, Guoqing, Zhuang, Lei, Song, Yu, He, Mengyang, Ma, Ding, Ma, Ling
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