Residential Collegefalse
Status已發表Published
Formal Modelling and Verification of the RTPS Behavior Module
Jiaqi Yin1; Huibiao Zhu1; Yuan Fei2; Qiwen Xu3
2021-08-01
Conference Name15th International Symposium on Theoretical Aspects of Software Engineering (TASE)
Source PublicationProceedings - 2021 International Symposium on Theoretical Aspects of Software Engineering, TASE 2021
Pages127-134
Conference Date25-27 August 2021
Conference PlaceShanghai, China
PublisherIEEE
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.

KeywordCsp Rtps Behavior Module Modeling Verification
DOI10.1109/TASE52547.2021.00028
URLView the original
Indexed ByCPCI-S
Language英語English
WOS Research AreaComputer Science
WOS SubjectComputer Science, Software Engineering ; Computer Science, Theory & Methods
WOS IDWOS:000722620300018
Scopus ID2-s2.0-85116869362
Fulltext Access
Citation statistics
Document TypeConference paper
CollectionDEPARTMENT OF COMPUTER AND INFORMATION SCIENCE
Corresponding AuthorHuibiao Zhu
Affiliation1.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.
Related Services
Recommend this item
Bookmark
Usage statistics
Export to Endnote
Google Scholar
Similar articles in Google Scholar
[Jiaqi Yin]'s Articles
[Huibiao Zhu]'s Articles
[Yuan Fei]'s Articles
Baidu academic
Similar articles in Baidu academic
[Jiaqi Yin]'s Articles
[Huibiao Zhu]'s Articles
[Yuan Fei]'s Articles
Bing Scholar
Similar articles in Bing Scholar
[Jiaqi Yin]'s Articles
[Huibiao Zhu]'s Articles
[Yuan Fei]'s Articles
Terms of Use
No data!
Social Bookmark/Share
All comments (0)
No comment.
 

Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.