A Modeling and Verification Method of CPS Based on Differential-Algebraic Dynamic Logic

Chen Qiaoqiao, Li Bixin, and Ji Shunhui

Journal of Computer Research and Development > 2013 > 50(4): 700-710.

Chen Qiaoqiao, Li Bixin, and Ji Shunhui. A Modeling and Verification Method of CPS Based on Differential-Algebraic Dynamic Logic[J]. Journal of Computer Research and Development, 2013, 50(4): 700-710.

Citation:

PDF (1768 KB)

A Modeling and Verification Method of CPS Based on Differential-Algebraic Dynamic Logic

Chen Qiaoqiao, Li Bixin, and Ji Shunhui

(School of Computer Science and Engineering, Southeast University, Nanjing 211189)

More Information

Published Date: April 14, 2013

Graphical Abstract

Abstract

Abstract

With the wide use of cyber physical systems in industrial control, intelligent transportation system, intelligent medical and other areas, safety has been the core problem of the recent cyber physical systems theory and application research. In this paper, a safety verification method based on differential-algebraic dynamic logic is proposed. The method firstly transforms HybridUML model to differential-algebraic program, then realizes the specification of system safety using differential-algebraic program, and finally the cyber physical systems safety is verified according to differential-algebraic program reasoning rules. Through the case study of airplane collision avoidance system, it is shown that the method can verify the validity of the collision avoidance manoeuver effectively and guarantee the safety of airplane collision avoidance system.
- cyber-physical systems,
- differential-algebraic dynamic logic,
- HybridUML,
- differential-algebraic program,
- verification

FullText(HTML)

References (0)

[1]	Tai Dongzhe, Zhang Ting, Liu Bin. The Pseudo Congestion of TCP in Software-Defined Networking[J]. Journal of Computer Research and Development, 2017, 54(1): 192-201. DOI: 10.7544/issn1000-1239.2017.20150139
[2]	Huang Junjie, Chen Xiaojiang, Liu Chen, Fang Dingyi, Wang Wei, Yin Xiaoyan, Wu Yueshan. A Source Data Congestion Control Based on Sleep Schedule[J]. Journal of Computer Research and Development, 2015, 52(8): 1852-1861. DOI: 10.7544/issn1000-1239.2015.20140668
[3]	Chen Shuping, Lu Deping, Chen Zhongping. Optimizing All_to_All Communication in Infiniband[J]. Journal of Computer Research and Development, 2014, 51(8): 1863-1870. DOI: 10.7544/issn1000-1239.2014.20121117
[4]	Wang Jian, Liu Yanheng, Mei Fang, and Zhang Cheng. Modeling Cascading Failures for Internet Based on Congestion Effects[J]. Journal of Computer Research and Development, 2010, 47(5): 772-779.
[5]	Dong Yongqiang, Yang Lu, and Dai Jiangpeng. Network Pricing Mechanism with Congestion Charge and Compensation[J]. Journal of Computer Research and Development, 2008, 45(8): 1322-1329.
[6]	Sun Limin, Li Bo, Zhou Xinyun. A Survey of Congestion Control Technology for Wireless Sensor Networks[J]. Journal of Computer Research and Development, 2008, 45(1): 63-72.
[7]	Li Shanshan, Liao Xiangke, Zhu Peidong, and Xiao Nong. Congestion Avoidance, Detection and Mitigation in Wireless Sensor Networks[J]. Journal of Computer Research and Development, 2007, 44(8): 1348-1356.
[8]	Li Shining, Guan Junming, Qin Zheng. KIR：A New Algorithm to Improve the Fairness of TCP Congestion Avoidance[J]. Journal of Computer Research and Development, 2006, 43(12): 2048-2055.
[9]	He Yanxiang, Xiong Naixue, Yang Yan. An Enhanced TCP Congestion Control Algorithm[J]. Journal of Computer Research and Development, 2005, 42(12): 2070-2076.
[10]	Ye Xiaoguo, Jiang Aiquan, and Wu Jiagao. ANLMCC—An Active Network-Based Layered Multicast Congestion Control Scheme[J]. Journal of Computer Research and Development, 2005, 42(2): 273-279.