空间生命支持系统中VCCR子系统的安全性验证

Safety Verification for VCCR Subsystem of Space Life Support System

基于动态微分逻辑的混成系统形式化验证理论,分析空间生命支持系统的一个子系统VCCR(Variable Configuration Carbon Dioxide Removal)的安全性。将VCCR系统基于混成程序建模,并给定需验证的安全性性质,使用KeYmaera混成系统形式化验证工具进行验证,证明了空间生命支持系统中VCCR子系统的安全性。

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.