TY - GEN
T1 - Formalization and verification of RTPS StatefulWriter module using CSP
AU - Yin, Jiaqi
AU - Zhu, Huibiao
AU - Fei, Yuan
AU - Xu, Qiwen
AU - Wu, Ruobiao
N1 - Publisher Copyright:
© 2019 Knowledge Systems Institute Graduate School. All rights reserved.
PY - 2019
Y1 - 2019
N2 - The Real Time Publish Subscribe protocol (RTPS), as a Data Distribution Service (DDS) protocol for computer systems, is composed of several modules. We focus on RTPS StatefulWriter Module which has two patterns, reliable pattern and best-effort pattern. As the main module of sending and receiving messages, its security and reliability are of great concern. The formal method can analyze whether it is a highly credible model from the mathematical point of view. Our research pays attention to the reliable pattern. Thus it is of great importance to model and verify whether the pattern is reliable through formal methods. In this paper, we model seven components of the module using Communicating Sequential Processes (CSP). By feeding the models into the model checker Process Analysis Toolkit (PAT), we verify four properties, divergence free, acknowledgement mechanism, data consistency and sequentiality. Consequently, it can be apparently concluded that the pattern of this module is reliable, which totally caters for its specification.
AB - The Real Time Publish Subscribe protocol (RTPS), as a Data Distribution Service (DDS) protocol for computer systems, is composed of several modules. We focus on RTPS StatefulWriter Module which has two patterns, reliable pattern and best-effort pattern. As the main module of sending and receiving messages, its security and reliability are of great concern. The formal method can analyze whether it is a highly credible model from the mathematical point of view. Our research pays attention to the reliable pattern. Thus it is of great importance to model and verify whether the pattern is reliable through formal methods. In this paper, we model seven components of the module using Communicating Sequential Processes (CSP). By feeding the models into the model checker Process Analysis Toolkit (PAT), we verify four properties, divergence free, acknowledgement mechanism, data consistency and sequentiality. Consequently, it can be apparently concluded that the pattern of this module is reliable, which totally caters for its specification.
KW - CSP
KW - Modeling
KW - PAT
KW - RTPS statefulwriter module
KW - Verification
UR - http://www.scopus.com/inward/record.url?scp=85071367142&partnerID=8YFLogxK
U2 - 10.18293/SEKE2019-060
DO - 10.18293/SEKE2019-060
M3 - 会议稿件
AN - SCOPUS:85071367142
T3 - Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE
SP - 147
EP - 152
BT - Proceedings - SEKE 2019
PB - Knowledge Systems Institute Graduate School
T2 - 31st International Conference on Software Engineering and Knowledge Engineering, SEKE 2019
Y2 - 10 July 2019 through 12 July 2019
ER -