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].http://symbolaris.com/info/KeYmaera.html,2013-05-13
[8] Guide for KeYmaera Hybrid Systems Verification Tool [EB/OL].http://symbolaris.com/info/KeYmaera-guide.html.,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!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!