Design and model checking of timed automata oriented architecture for Internet of thing
The architecture model of the Internet of thing system is the primary foundation for the design and implementation of the Internet of thing system. This article discusses the method and practice of time automaton modeling and model checking for the architecture of the Internet of thing system from t...
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Hindawi - SAGE Publishing
2020-05-01
|
| Series: | International Journal of Distributed Sensor Networks |
| Online Access: | https://doi.org/10.1177/1550147720911008 |
| _version_ | 1797763174649298944 |
|---|---|
| author | Guang Chen Tonghai Jiang Meng Wang Xinyu Tang Wenfei Ji |
| author_facet | Guang Chen Tonghai Jiang Meng Wang Xinyu Tang Wenfei Ji |
| author_sort | Guang Chen |
| collection | DOAJ |
| description | The architecture model of the Internet of thing system is the primary foundation for the design and implementation of the Internet of thing system. This article discusses the method and practice of time automaton modeling and model checking for the architecture of the Internet of thing system from the state and time dimensions. This article introduces the theory and method of modeling using time automata. And then, combined with the actual need of the elderly health cabin Internet of thing system, a dynamic and fault-tolerant time automaton model is established through a relatively complete architecture modeling. The model checking method verifies that the designed Internet of thing system has no deadlock system activity, service correctness, and timeliness correctness. The results of modeling experiments and model validation show that the reference model of time automata Internet of thing architecture established in this article can better reflect the nature of interaction with the physical world, heterogeneity and large-scale, dynamic, and incompleteness of the Internet of thing system. |
| first_indexed | 2024-03-12T19:37:52Z |
| format | Article |
| id | doaj.art-d3404941607e48ec90e33ab4f2256835 |
| institution | Directory Open Access Journal |
| issn | 1550-1477 |
| language | English |
| last_indexed | 2024-03-12T19:37:52Z |
| publishDate | 2020-05-01 |
| publisher | Hindawi - SAGE Publishing |
| record_format | Article |
| series | International Journal of Distributed Sensor Networks |
| spelling | doaj.art-d3404941607e48ec90e33ab4f22568352023-08-02T04:05:12ZengHindawi - SAGE PublishingInternational Journal of Distributed Sensor Networks1550-14772020-05-011610.1177/1550147720911008Design and model checking of timed automata oriented architecture for Internet of thingGuang Chen0Tonghai Jiang1Meng Wang2Xinyu Tang3Wenfei Ji4Research and Development Center for IoT of Chinese Academy of Sciences, Wuxi, ChinaXinjiang Laboratory of Minority Speech and Language Information Processing, Chinese Academy of Sciences, Urumqi, ChinaResearch and Development Center for IoT of Chinese Academy of Sciences, Wuxi, ChinaResearch and Development Center for IoT of Chinese Academy of Sciences, Wuxi, ChinaResearch and Development Center for IoT of Chinese Academy of Sciences, Wuxi, ChinaThe architecture model of the Internet of thing system is the primary foundation for the design and implementation of the Internet of thing system. This article discusses the method and practice of time automaton modeling and model checking for the architecture of the Internet of thing system from the state and time dimensions. This article introduces the theory and method of modeling using time automata. And then, combined with the actual need of the elderly health cabin Internet of thing system, a dynamic and fault-tolerant time automaton model is established through a relatively complete architecture modeling. The model checking method verifies that the designed Internet of thing system has no deadlock system activity, service correctness, and timeliness correctness. The results of modeling experiments and model validation show that the reference model of time automata Internet of thing architecture established in this article can better reflect the nature of interaction with the physical world, heterogeneity and large-scale, dynamic, and incompleteness of the Internet of thing system.https://doi.org/10.1177/1550147720911008 |
| spellingShingle | Guang Chen Tonghai Jiang Meng Wang Xinyu Tang Wenfei Ji Design and model checking of timed automata oriented architecture for Internet of thing International Journal of Distributed Sensor Networks |
| title | Design and model checking of timed automata oriented architecture for Internet of thing |
| title_full | Design and model checking of timed automata oriented architecture for Internet of thing |
| title_fullStr | Design and model checking of timed automata oriented architecture for Internet of thing |
| title_full_unstemmed | Design and model checking of timed automata oriented architecture for Internet of thing |
| title_short | Design and model checking of timed automata oriented architecture for Internet of thing |
| title_sort | design and model checking of timed automata oriented architecture for internet of thing |
| url | https://doi.org/10.1177/1550147720911008 |
| work_keys_str_mv | AT guangchen designandmodelcheckingoftimedautomataorientedarchitectureforinternetofthing AT tonghaijiang designandmodelcheckingoftimedautomataorientedarchitectureforinternetofthing AT mengwang designandmodelcheckingoftimedautomataorientedarchitectureforinternetofthing AT xinyutang designandmodelcheckingoftimedautomataorientedarchitectureforinternetofthing AT wenfeiji designandmodelcheckingoftimedautomataorientedarchitectureforinternetofthing |