Formalization and verification of RTPS StatefulWriter module using CSP

Jiaqi Yin, Huibiao Zhu, Yuan Fei, Qiwen Xu, Ruobiao Wu

科研成果: 书/报告/会议事项章节会议稿件同行评审

4 引用 (Scopus)

摘要

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.

源语言英语
主期刊名Proceedings - SEKE 2019
主期刊副标题31st International Conference on Software Engineering and Knowledge Engineering
出版商Knowledge Systems Institute Graduate School
147-152
页数6
ISBN(电子版)1891706489
DOI
出版状态已出版 - 2019
已对外发布
活动31st International Conference on Software Engineering and Knowledge Engineering, SEKE 2019 - Lisbon, 葡萄牙
期限: 10 7月 201912 7月 2019

出版系列

姓名Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE
2019-July
ISSN(印刷版)2325-9000
ISSN(电子版)2325-9086

会议

会议31st International Conference on Software Engineering and Knowledge Engineering, SEKE 2019
国家/地区葡萄牙
Lisbon
时期10/07/1912/07/19

指纹

探究 'Formalization and verification of RTPS StatefulWriter module using CSP' 的科研主题。它们共同构成独一无二的指纹。

引用此