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

Safety Verification for VCCR Subsystem of Space Life Support System

作　　者：李倩[1] 郁文生[1] 

机构地区：[1]华东师范大学上海高可信计算重点实验室,上海200062

出　　处：《计算机科学》2014年第6期193-198,共6页Computer Science

基　　金：国家自然科学基金(61370176;61070048);国家自然科学基金委员会创新研究群体科学基金(61021004);国家"863"计划(2011AA010101);国家"973"计划(2011CB302802);上海市重点学科建设项目(B412);上海市教育委员会科研创新项目(11ZZ37)资助

摘　　要：基于动态微分逻辑的混成系统形式化验证理论,分析空间生命支持系统的一个子系统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.

关 键 词：混成系统 生命支持系统 VCCR系统 形式化验证 KeYmaera工具 

分 类 号：TP302.2[自动化与计算机技术—计算机系统结构]