Computer Science ›› 2014, Vol. 41 ›› Issue (6): 193-198.doi: 10.11896/j.issn.1002-137X.2014.06.038

Previous Articles     Next Articles

Safety Verification for VCCR Subsystem of Space Life Support System

LI Qian and YU Wen-sheng   

  • Online:2018-11-14 Published:2018-11-14

Abstract: This paper applied the differential-dynamic logic theory to analyze and verify the safety properties of a hybrid system named Variable Configuration Carbon Dioxide Removal (VCCR),which is a subsystem of space life support system.Based on the hybrid program,a model of the hybrid system VCCR with its safety properties was built.Using the hybrid system verification tool KeYmaera,it was formally proved that the system satisfies the safety properties under all possible scenarios.

Key words: Hybrid system,Life support system,VCCR system,Formal verification,KeYmaera tool

[1] Astrom A J,Wittenmark B.Computer Controller Systems-Theo-ry and Design(Third Edition)[M].Prentice Hall/Pearson,2001
[2] Platzer A,Quesel J D.European Train Control System:A Case Study in Formal Verification [R].SFB/TR 14AVACS 54.2009
[3] Platzer A.Logical Analysis of Hybrid Systems:Proving Theorems for Complex Dynamics [M].Springer,2010
[4] Platzer A.The complete proof of theory of hybrid systems [C]∥ACM/IEEE Symposium on Logic in Computer Science,LICS 2012.2012:541-550
[5] Schaft A,Schumacher H.An introduction to Hybrid Dynamical Systems [M].Springer-Verlag,2000
[6] Subramanian D,Ariyur K,Lamba N,et al.Control design for a hybrid dynamical system:A NASA life support system [C]∥LNCS 2993.Springer-Verlag,2004:570-584
[7] KeYmaera:A Hybrid Theorem Prover for Hybrid Systems [EB/OL].,2013-05-13
[8] Guide for KeYmaera Hybrid Systems Verification Tool [EB/OL].,2012-10-27
[9] Monin J F,Hinchey M G.Understanding Formal Methods[M].Springer,2003
[10] Malin J,Nieten J,Schreckenghost D,et al.Multi-agent diagnosis and control of an air revitalization system for life support in space [C]∥Proceedings of the IEEE Aerospace Conference.2000:309-326
[11] Edmund M C,Orna G,Doron P.Model Checking [M]. Cambridge,MA:MIT Press,2000
[12] Alur R,Dang T,Ivancic F.Progress on reachability analysis of hybrid systems using predicate abstraction [C]∥LNCS 2623.Springer-Verlag,2003:4-19
[13] Horowitz R,Varaiya P.Control design of an automated highway system [J].Proceedings of the IEEE,2000,88(7):913-925
[14] Glavaski S,Papachristodoulou A,Ariyur K.Safety verificationof controlled advanced life support system using barrier certificates [C]∥Hybrid Systems:Computation and Control,Lecture Notes in Computer Science.2005:3414:306-321
[15] Loos S M,Renshaw D W,Platzer A.Formal verification of distributed aircraft controllers [C]∥Hybrid Systems:Computation and Control.Philadelphia,PA,USA,2013:125-130
[16] Prajna S.Optimization-based Methods for Nonlinear and Hybrid Systems Verification [D].California Institute of Technology,2005
[17] Glover W,Lygeros J.A stochastic hybrid model for air trafficcontrol simulation.LNCS 2993[C]∥Hybrid Systems:Computation and Control.Heidelberg:Springer-Verlag,2004:372-386
[18] Kouskoulas Y,Renshaw D W,Platzer A.Certifying the safe design of a virtual fixture control algorithm for a surgical robot [C]∥Hybrid Systems:Computation and Control.Philadelphia,PA,USA,2013
[19] Manna Z,Pnueli A.Temporal Verification of Reactive Systems[M].Springer-Verlag,1995

No related articles found!
Full text



[1] LEI Li-hui and WANG Jing. Parallelization of LTL Model Checking Based on Possibility Measure[J]. Computer Science, 2018, 45(4): 71 -75, 88 .
[2] XIA Qing-xun and ZHUANG Yi. Remote Attestation Mechanism Based on Locality Principle[J]. Computer Science, 2018, 45(4): 148 -151, 162 .
[3] LI Bai-shen, LI Ling-zhi, SUN Yong and ZHU Yan-qin. Intranet Defense Algorithm Based on Pseudo Boosting Decision Tree[J]. Computer Science, 2018, 45(4): 157 -162 .
[4] WANG Huan, ZHANG Yun-feng and ZHANG Yan. Rapid Decision Method for Repairing Sequence Based on CFDs[J]. Computer Science, 2018, 45(3): 311 -316 .
[5] SUN Qi, JIN Yan, HE Kun and XU Ling-xuan. Hybrid Evolutionary Algorithm for Solving Mixed Capacitated General Routing Problem[J]. Computer Science, 2018, 45(4): 76 -82 .
[6] ZHANG Jia-nan and XIAO Ming-yu. Approximation Algorithm for Weighted Mixed Domination Problem[J]. Computer Science, 2018, 45(4): 83 -88 .
[7] WU Jian-hui, HUANG Zhong-xiang, LI Wu, WU Jian-hui, PENG Xin and ZHANG Sheng. Robustness Optimization of Sequence Decision in Urban Road Construction[J]. Computer Science, 2018, 45(4): 89 -93 .
[8] LIU Qin. Study on Data Quality Based on Constraint in Computer Forensics[J]. Computer Science, 2018, 45(4): 169 -172 .
[9] ZHONG Fei and YANG Bin. License Plate Detection Based on Principal Component Analysis Network[J]. Computer Science, 2018, 45(3): 268 -273 .
[10] SHI Wen-jun, WU Ji-gang and LUO Yu-chun. Fast and Efficient Scheduling Algorithms for Mobile Cloud Offloading[J]. Computer Science, 2018, 45(4): 94 -99, 116 .