计算机科学 ›› 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! |
|