Residential College | false |
Status | 已發表Published |
Formal Modelling and Verification of the RTPS Behavior Module | |
Jiaqi Yin1; Huibiao Zhu1; Yuan Fei2; Qiwen Xu3 | |
2021-08-01 | |
Conference Name | 15th International Symposium on Theoretical Aspects of Software Engineering (TASE) |
Source Publication | Proceedings - 2021 International Symposium on Theoretical Aspects of Software Engineering, TASE 2021 |
Pages | 127-134 |
Conference Date | 25-27 August 2021 |
Conference Place | Shanghai, China |
Publisher | IEEE |
Abstract | With the popularization and development of 5G, it is vital to guarantee the security of the whole data while transmitting them at high speed. Data Distribution Service (DDS), as the core technology of network data communication, is one of the most significant protocols. The Real Time Publish Subscribe (RTPS) protocol is part of DDS, which emphasizes data publishing and receiving.In this paper, we focus on the Behavior module of the RTPS protocol, where the reliable modes are always to ensure the reliability of data. Thus, we adopt CSP to model eight core components and add corresponding intruders to attack the model in order to verify and detect the potential risks of the design. Specifically, we also improve our model by utilizing digital signature and digital certificate. Five properties abstracted from the specification have been verified through the model checker PAT. The result shows that once adding the digital signature and digital certificate together, there is no situation that publisher and subscriber are unauthorized; in addition, due to multiple encryption, data cannot be faked or intercepted. However, the history-cache still can be faked for it has no identity authentication. That is to say, to be highly trustworthy, developers need to ensure mutual authentication between modules as much as possible. Consequently, we hope this method makes sense for researches on security of data distribution protocol and gives a meaningful guide for DDS middleware development. |
Keyword | Csp Rtps Behavior Module Modeling Verification |
DOI | 10.1109/TASE52547.2021.00028 |
URL | View the original |
Indexed By | CPCI-S |
Language | 英語English |
WOS Research Area | Computer Science |
WOS Subject | Computer Science, Software Engineering ; Computer Science, Theory & Methods |
WOS ID | WOS:000722620300018 |
Scopus ID | 2-s2.0-85116869362 |
Fulltext Access | |
Citation statistics | |
Document Type | Conference paper |
Collection | DEPARTMENT OF COMPUTER AND INFORMATION SCIENCE |
Corresponding Author | Huibiao Zhu |
Affiliation | 1.Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China 2.Shanghai Normal University, Shanghai, China 3.University of Macau, Macao |
Recommended Citation GB/T 7714 | Jiaqi Yin,Huibiao Zhu,Yuan Fei,et al. Formal Modelling and Verification of the RTPS Behavior Module[C]:IEEE, 2021, 127-134. |
APA | Jiaqi Yin., Huibiao Zhu., Yuan Fei., & Qiwen Xu (2021). Formal Modelling and Verification of the RTPS Behavior Module. Proceedings - 2021 International Symposium on Theoretical Aspects of Software Engineering, TASE 2021, 127-134. |
Files in This Item: | There are no files associated with this item. |
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment