计算机科学 ›› 2014, Vol. 41 ›› Issue (6): 193-198.doi: 10.11896/j.issn.1002-137X.2014.06.038
李倩,郁文生
LI Qian and YU Wen-sheng
摘要： 基于动态微分逻辑的混成系统形式化验证理论,分析空间生命支持系统的一个子系统VCCR(Variable Configuration Carbon Dioxide Removal)的安全性。将VCCR系统基于混成程序建模,并给定需验证的安全性性质,使用KeYmaera混成系统形式化验证工具进行验证,证明了空间生命支持系统中VCCR子系统的安全性。
| [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! |
|
||
首页