Page 255 - 《软件学报》2021年第6期

芦倩 等:面向数据流的 ROS2 数据分发服务形式建模与分析 1829

[5] He F, Baresi L, Ghezzi C, et al. Formal analysis of publish-subscribe systems by probabilistic timed automata. In: Proc. of the Int’l
Conf. on Formal Techniques for Networked and Distributed Systems. Berlin, Heidelberg: Springer, 2007. 247−262.
[6] Liu Y, Guan Y, Li X, et al. Formal analysis and verification of DDS in ROS2. In: Proc. of the 2018 16th ACM/IEEE Int’l Conf. on
Formal Methods and Models for System Design (MEMOCODE). IEEE, 2018. 1−5.
[7] Yin J, Zhu H, Fei Y, et al. Formalization and verification of RTPS StatefulWriter module using CSP. In: Proc. of the 31st Int’l
Conf. on Software Engineering and Knowledge Engineering. 2019.
[8] Maruyama Y, Kato S, Azumi T. Exploring the performance of ROS2. In: Proc. of the 13th Int’l Conf. on Embedded Software.
ACM, 2016. 5.
[9] Inglés-Romero JF, Romero-Garcés A, Vicente-Chicote C, et al. A model-driven approach to enable adaptive QoS in DDS-based
middleware. IEEE Trans. on Emerging Topics in Computational Intelligence, 2017,1(3):176−187.
[10] Casini D, Blaß T, Lütkebohle I, et al. Response-Time analysis of ROS 2 processing chains under reservation-based scheduling. In:
Proc. of the 31st Euromicro Conf. on Real-Time Systems (ECRTS 2019). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2019.
[11] Kim J, Smereka JM, Cheung C, et al. Security and performance considerations in ROS 2: A balancing act. 2018.
[12] Schlesselman JM, Pardo-Castellote G, Farabaugh B. OMG data-distribution service (DDS): Architectural update. In: Proc. of the
IEEE MILCOM 2004 Military Communications Conf. IEEE, 2004. 961−967.
[13] Guesmi T, Rekik R, Hasnaoui S, et al. Design and performance of DDS-based middleware for real-time control systems. IJCSNS,
2007,7(12):188−200.
[14] Corsaro A, Schmidt DC. The data distribution service—The communication middleware fabric for scalable and extensible
systems-of-systems. System of Systems, 2012.
[15] Chen C. Design and implementation of data distribution system based on DDS [Master. Thesis]. Shamghai: Fudan University, 2008
(in Chinese with English abstract).
[16] Norman G, Parker D, Sproston J. Model checking for probabilistic timed automata. Formal Methods in System Design, 2013,43(2):
164−190.
[17] Kwiatkowska M, Norman G, Parker D. PRISM: Probabilistic symbolic model checker. In: Proc. of the Int’l Conf. on Modelling
Techniques and Tools for Computer Performance Evaluation. Berlin, Heidelberg: Springer, 2002. 200−204.
[18] Kwiatkowska M, Norman G, Parker D. PRISM: Probabilistic model checking for performance and reliability analysis. ACM
SIGMETRICS Performance Evaluation Review, 2009,36(4):40−45.
附中文参考文献:
[4] 董威,王戟,齐治昌.并发和实时系统的模型检验技术.计算机研究与发展,2001,38(6):698−705.
[15] 陈春甫.基于 DDS 的数据分发系统的设计与实现[硕士学位论文].上海:复旦大学,2008.

芦倩(1993－),女,硕士,主要研究领域为嵌 王瑞(1981－),女,博士,教授,博士生导师,
入式系统形式建模与验证,网络协议分析. 主要研究领域为形式化方法,软件安全
验证.

李晓娟(1968－),女,博士,教授,博士生导 施智平(1974－),男,博士,教授,博士生导
师,主要研究领域为嵌入式系统形式建模 师 , 主要 研究领 域为形 式化方 法 , 人工
与验证,网络协议分析. 智能.

关永(1966－),男,博士,教授,博士生导师,
主要研究领域为形式化验证,高可靠嵌入
式系统,机器人.