微信服务号

微信订阅号

2025年3月24日 13:06 星期一
首页 > 过刊浏览>2014年第25卷第2期 >219-233. DOI:10.13328/j.cnki.jos.004535
PDF HTML阅读 XML下载 导出引用 引用提醒
混成系统形式化验证
作者:
基金项目:

国家自然科学基金（61100036, 91318301, 61321491）；国家高技术研究发展计划（863）（2012AA011205）；江苏省自然科学基金（BK2011558）


Formal Verification of Hybrid System
Author:
  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [95]
    • |
  • 相似文献 [20]
    • |
  • 引证文献
    • | |
  • 文章评论
    摘要:

    混成系统是实时嵌入式系统的一种重要子类，其行为中广泛存在离散控制逻辑跳转与连续实时行为交织混杂的情况，因此行为复杂，难以掌握与控制.由于此类系统广泛出现在工控、国防、交通等与国计民生密切相关的安全攸关的领域，因此，如何对相关系统进行有效的分析与理解，从而保障系统安全运营，是一项具有重要意义的工作.常规的系统安全性分析手段，如测试、仿真等仅能在一定输入的情况下运行系统来观测系统行为，无法穷尽地检测复杂混成系统在所有可能输入下的行为，因此并不足以保证系统的安全性.区别于测试等方法，形式化方法通过求解系统模型状态取值范围等方法来确认系统模型中一定不会出现相关错误.因此，其对于保障安全攸关混成系统的安全性具有十分重要的意义.形式化方法由形式化规约与形式化验证两个方面构成.因此从以上两个角度分别对形式化规约方向上现有混成系统建模语言、关注性质以及形式化验证方向的混成系统模型检验、定理证明的现有主要技术与方法进行了综述性的回顾与总结.在此基础上，针对现阶段实时嵌入式系统复杂化、网络化的特性，对混成系统形式化验证的重要关注问题与研究方向进行了探索与讨论.

    Abstract:

    Hybrid System is a very important subclass of real time embedded system. The behavior of hybrid system is tangled with discrete control mode transformation and continuous real time behavior, therefore very complex and difficult to control. As hybrid system is widely used in safety-critical areas like industry, defense and transportation system, it is very important to analyze and understand the system effectively to guarantee the safe operation of the system. Ordinary techniques like testing and simulation can only observe the behavior of the system under given input. As they cannot exhaust all the possible inputs and scenarios, they are not enough to guarantee the safety of the system. In contrast to testing based techniques, formal method can answer questions like if the system will never violate certain specification by traversing the complete state space of the system. Therefore, it is very important to pursue the direction of formal verification of safety-critical hybrid system. Formal method consists of formal specification and formal verification. This paper reviews the modeling language and specification of hybrid system as well as techniques in model checking and theorem proving. In addition, it discusses the potential future directions in the related area.

    参考文献
    [1] Henzinger TA. The theory of hybrid automata. In: Proc. of the 11th Annual IEEE Symp. on Logic in Computer Science (LICS’96). New Brunswick: IEEE, 1996. 278-292. [doi: 10.1109/LICS.1996.561342]
    [2] Myers GJ. Art of Software Testing. 2nd ed., New York: John Wiley & Sons, Inc., 1979.
    [3] Bertolino A. Software testing research: Achievements, challenges, dreams. In: Briand LC, ed. Proc. of the 2007 Future of Software Engineering (FOSE 2007). Washington: IEEE Computer Society, 2007. 85-103. [doi: 10.1109/FOSE.2007.25]
    [4] Peled DA. Software Reliability Methods. New York: Springer-Verlag, 2001.
    [5] Jr. Clarke EM, Grumberg O, Peled DA. Model Checking. Cambridge: The MIT Press, 1999.
    [6] Hoare CAR. Communicating Sequential Processes. Hertfordshire: Prentice-Hall Int’l, 1985.
    [7] Harel D. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 1987,8(3):231-274. [doi: 10. 1016/0167-6423(87)90035-9]
    [8] Rushby JM. Automated deduction and formal methods. In: Alur R, Henzinger TA, eds. Proc. of the 8th Int’l Conf. on Computer Aided Verification (CAV’96). London: Springer-Verlag, 1996. 169-183. [doi: 10.1007/3-540-61474-5_67]
    [9] Hoare CAR, He J. Unifying Theories of Programming. Hertfordshire: Prentice-Hall Int’l, 1998.
    [10] Alur R. Formal verification of hybrid systems. In: Chakraborty S, Jerraya A, Baruah SK, Fischmeister S, eds. Proc. of the 11th Int’l Conf. on Embedded Software (EMSOFT 2011). New York: ACM Press, 2011. 273-278. [doi: 10.1145/2038642.2038685]
    [11] He J. From CSP to hybrid systems. In: Roscoe AW, ed. A Classical Mind: Essays in Honour of C.A.R. Hoare. Hertfordshire: Prentice-Hall Int’l, 1994. 171-189.
    [12] Zhou C, Wang J, Ravn AP. A formal description of hybrid systems. In: Alur R, Henzinger TA, Sontag ED, eds. Proc. of the Hybrid Systems’95. LNCS 1066, Heidelberg: Springer-Verlag, 1995. 511-530. [doi: 10.1007/BFb0020972]
    [13] David R. Modeling of hybrid systems using continuous and hybrid Petri nets. In: Proc. of the 6th Int’l Workshop on Petri Nets and Performance Models (PNPM’97). Washington: IEEE Computer Society, 1997. [doi: 10.1109/PNPM.1997.595536]
    [14] Platzer A. Differential dynamic logic for hybrid systems. Journal of Automated Reasoning, 2008,41(2):143-189. [doi: 10.1007/ s10817-008-9103-8]
    [15] Henzinger TA, Ho PH, Wong-Toi H. Algorithmic analysis of nonlinear hybrid systems. IEEE Trans. on Automatic Control, 1998, 43(4):540-554. [doi: 10.1109/9.664156]
    [16] Alur R, Courcoubetis C, Halbwachs N, Henzinger TA, Ho PH, Nicollin X, Olivero A, Sifakis J, Yovine S. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 1995,138(1):3-34. [doi: 10.1016/0304-3975(94)00202-T]
    [17] Alur R, Dill DL. A theory of timed automata. Theoretical Computer Science, 1994,126(2):183-235. [doi: 10. 1016/0304-3975(94)9 0010-8]
    [18] Lamport L. Proving the correetness of multiprocess programs. IEEE Trans. on Software Engineering, 1977,SE-3(2):125-143. [doi: 10.1109/TSE.1977.229904]
    [19] Manna Z, Pnueli A. The Temporal Logic of Reactive and Concurrent Systems. New York: Springer-Verlag, 1992.
    [20] Asarin E, Dang T, Maler O. d/dt: A tool for reachability analysis of continuous and hybrid systems. In: Proc. of the Int’l Federation of Automatic Control (IFAC), Nonlinear Control Systems. Oxford: Pergamon, 2001. 20-31.
    [21] Asarin E, Dang T, Maler O, Bournez O. Approximate reachability analysis of piecewise-linear dynamical systems. In: Lynch N, ed. Proc. of the 3rd Int’l Workshop on Hybrid Systems: Computation and Control (HSCC 2000). London: Springer-Verlag, 2000. 20-31. [doi: 10.1007/3-540-46430-1_6]
    [22] Bemporad A, Morari M. Verification of hybrid systems via mathematical programming. In: Vaandrager FW, ed. Proc. of the 2nd Int’l Workshop on Hybrid Systems (HSCC’99). London: Springer-Verlag, 1999. 31-45. [doi: 10.1007/3-540-48983-5_7]
    [23] Bemporad A, Torrisi FD, Morari M. Optimization-Based verification and stability characterization of piecewise affine and hybrid systems. In: Lynch N, ed. Proc. of the 3rd Int’l Workshop on Hybrid Systems: Computation and Control (HSCC 2000). London: Springer-Verlag, 2000. 45-58. [doi: 10.1007/3-540-46430-1_8]
    [24] Botchkarev O, Tripakis S. Verification of hybrid systems with linear differential inclusions using ellipsoidal approximations. In: Lynch N, ed. Proc. of the 3rd Int’l Workshop on Hybrid Systems: Computation and Control (HSCC 2000). London: Springer- Verlag, 2000. 73-88.
    [25] Kurzhanski AB, Varaiya P. Ellipsoidal techniques for reachability analysis. In: Lynch N, ed. Proc. of the Hybrid Systems: Computation and Control (HSCC 2000). London: Springer-Verlag, 2000. 202-214. [doi: 10.1007/3-540-46430-1_19]
    [26] Kesten Y, Pnueli A, Sifakis J, Yovine S. Integration graphs: A class of decidable hybrid systems. In: Grossman RL, ed. Proc. of the Hybrid Systems. LNCS 736, Berlin, Heidelberg: Springer-Verlag, 1993. 179-208. [doi: 10.1007/3-540-57318-6_29]
    [27] Henzinger TA, Kopke PW, Puri A, Varaiya P. What’s decidable about hybrid automata? In: Leighton F, Borodin A, eds. Proc. of the 27th Annual ACM Symp. on Theory of Computing. New York: ACM, 1995. 373-382. [doi: 10.1145/225058.225162]
    [28] Silva BI, Stursberg O, Krogh BH, Engell S. An assessment of the current status of algorithmic approaches to the verification of hybrid systems. In: Proc. of the 40th Conf. on Decision and Control. Orlando: IEEE, 2001. 2867-2874. [doi: 10.1109/.2001.9807 11]
    [29] Henzinger TA, Ho PH, Wong-Toi H. HYTECH: A model checker for hybrid systems. In: Grumberg O, ed. Proc. of the 9th Int’l Conf. on Computer Aided Verification (CAV’97). London: Springer-Verlag, 1997. 460-463. [doi: 10.1007/3-540-63166-6_48]
    [30] Frehse G. PHAVer: Algorithmic verification of hybrid systems past HyTech. In: Morari M, ed. Proc. of the Int’l Conf. on Hybrid Systems: Computation and Control. Heidelberg: Springer-Verlag, 2005. 258-273. [doi: 10.1007/978-3-540-31954-2_17]
    [31] Silva B, Richeson K, Krogh B, Chutinan A. Modeling and verifying hybrid dynamic systems using checkmate. In: Proc. of the 4th Int’l Conf. on Automataion of Mixed Processes. Shaker Publisher, 2000. 323-328.
    [32] Chen X, Abraham E, Sankaranarayanan S. Flow*: An analyzer for non-linear hybrid systems. In: Sharygina N, Veith H, eds. Proc. of the Computer Aided Verification 2013. LNCS 8044, Beilin, Heidelberg: Springer-Verlag, 2013. 258-263. [doi: 10.1007/978-3- 642-39799-8_18]
    [33] Frehse G, Le Guernic C, Donzé A, Cotton S, Ray R, Lebeltel O, Ripado R, Girard A, Dang T, Maler O. SpaceEx: Scalable verification of hybrid systems. In: Gopalakrishnan G, Qadeer S, eds. Proc. of the Computer Aided Verification. LNCS 6806, Berlin, Heidelberg: Springer-Verlag, 2011. 379-395. [doi: 10.1007/978-3-642-22110-1_30]
    [34] Clarke E, Grumberg O, Jha S, Lu Y, Veith H. Counterexample-Guided abstraction refinement. In: Emerson EA, Sistla AP, eds. Proc. of the Computer aided verification. LNCS 1855, Berlin, Heidelberg: Springer-Verlag, 2000. 154-169. [doi: 10.1007/1072216 7_15]
    [35] Clarke E, Fehnker A, Han Z, Krogh B, Stursberg O, Theobald M. Verification of hybrid systems based on counterexample-guided abstraction refinement. In: Garavel H, Hatcliff J, eds. Proc. of the Tools and Algorithms for the Construction and Analysis of Systems. LNCS 2619, Berlin, Heidelberg: Springer-Verlag, 2003. 192-207. [doi: 10.1007/3-540-36577-X_14]
    [36] Alur R, Dang T, Ivančić F. Counterexample-Guided predicate abstraction of hybrid systems. Theoretical Computer Science, 2006, 354(2):250-271. [doi:10.1016/j.tcs.2005.11.026]
    [37] Jha S, Krogh BH, Weimer JE, Clarke EM. Reachability for linear hybrid automata using iterative relaxation abstraction. In: Bemporad A, Bicchi A, Buttazzo G, eds. Proc. of the Hybrid Systems: Computation and Control. Berlin, Heidelberg: Springer- Verlag, 2007. 287-300. [doi: 10.1007/978-3-540-71493-4_24]
    [38] Li XD, Jha SK, Bu L. Towards an efficient path-oriented tool for bounded reachability analysis of linear hybrid systems using linear programming. Electronic Notes on Theoretical Computer Science, 2007,174(3):57-70. [doi: 10.1016/j.entcs.2006.12.023]
    [39] Bryant RE. Graph-Based algorithms for boolean function manipulation. IEEE Trans. on Computers, 1986,C-35(8):677-691. [doi: 10.1109/TC.1986.1676819]
    [40] Biere A, Cimatti A, Clarke EM, Strichman O, Zhu Y. Bounded model checking. Advance in Computers, 2008,58:117-148.
    [41] Zhang L, Malik S. The quest for efficient boolean satifiability solvers. In: Brinksma E, Larsen K, eds. Proc. of the Computer Aided Verification. Heidelberg: Springer-Verlag, 2002. 17-36.
    [42] Audemard G, Bozzano M, Cimatti A, Sebastiani R. Verifying industrial hybrid systems with MathSAT. Electronic Notes on Theoretical Computer Science, 2005,119(2):17-32. [doi: 10.1016/j.entcs.2004.12.022]
    [43] Audemard G, Cimatti A, Kornilowicz A, Sebastiani R. Bounded model checking for timed systems. In: Peled DA, Vardi M, eds. Proc. of the FORTE 2002. LNCS 2529, Berlin, Heidelberg: Springer-Verlag, 2002. 243-259. [doi: 10.1007/3-540-36135-9_16]
    [44] Franzle M, Herde C. Efficient proof engines for bounded model checking of hybrid systems. Electronic Notes on Theoretical Computer Science, 2005,133:119-137. [doi: 10.1016/j.entcs.2004.08.061]
    [45] Bu L, Li Y, Wang LZ, Li XD. BACH: Bounded reachability checker for linear hybrid automata. In: Cimatti A, Jones RB, eds. Proc. of the 8th Int’l Conf. on Formal Methods in Computer Aided Design (FMCAD 2008). Portland: IEEE Computer Society Press, 2008. 1-4. [doi: 10.1109/FMCAD.2008.ECP.13]
    [46] Yang Y, Bu L, Li XD. Forward and backward: Bounded model checking of linear hybrid automata from two directions. In: Cabodi G, Singh S, eds. Proc. of the Formal Methods in Computer-Aided Design. Cambridge: IEEE Computer Society Press, 2012. 204-208.
    [47] Bu L, Yang Y, Li XD. IIS-Guided DFS for efficient bounded reachability analysis of linear hybrid automata. In: Eder K, Lourenço J, Shehory O, eds. Proc. of the Hardware and Software: Verification and Testing 2011. LNCS 7261, Berlin, Heidelberg: Springer- Verlag, 2012. 35-49. [doi: 10.1007/978-3-642-34188-5_7]
    [48] Bu L, Li XD. Path-Oriented bounded reachability analysis of composed linear hybrid systems. Int’l Journal on Software Tools for Technology Transfer, 2011,13(4):307-317. [doi: 10.1007/s10009-010-0163-9]
    [49] Bu L, Cimatti A, Li XD, Mover S, Tonetta S. Model checking of hybrid systems using shallow synchronization. In: Hatcliff J, Zucca E, eds. Proc. of the Formal Techniques for Distributed Systems. LNCS 6117, Berlin, Heidelberg: Springer-Verlag, 2010. 155-169. [doi: 10.1007/978-3-642-13464-7_13]
    [50] Moore RE, Bierbaum F. Methods and Applications of Interval Analysis. Philadelphia: Society of Industrial and Applied Mathematics, 1979.
    [51] Franzle M, Herde C, Teige T. Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. Journal on Satisfiability, Boolean Modeling and Computation, 2007,1:209-236.
    [52] Gao SC, Avigad J, Clarke EM. Delta-Complete decision procedures for satisfiability over the reals. In: Gramlich B, Miller D, Sattler U, eds. Proc. of the Int’l Joint Conf. on Automated Reasoning (IJCAR). Heidelberg: Springer-Verlag, 2012. 286-300.
    [53] Gao SC, Kong S, Clarke EM. dReal: An SMT solver for nonlinear theories of the reals. In: Bonacina MP, ed. Proc. of the Conf. on Automated Deduction 2013. LNAI 7898, Berlin, Heidelberg: Springer-Verlag, 2013. 208-214. [doi: 10.1007/978-3-642-38574-2_ 14]
    [54] Bu L, Zhao JH, Li XD. Path-Oriented reachability verification of a class of nonlinear hybrid automata using convex programming. In: Barthe G, Hermenegildo M, eds. Proc. of the Verification, Model Checking, and Abstract Interpretation 2010. LNCS 5944, Berlin, Heidelberg: Springer-Verlag, 2010. 79-94. [doi: 10.1007/978-3-642-11319-2_9]
    [55] Cimatti A, Mover S, Tonetta S. A quantifier-free SMT encoding of non-linear hybrid automata. In: Cabodi G, Singh S, eds. Proc. of the Formal Methods in Computer-Aided Design. Cambridge: IEEE, 2012. 187-195.
    [56] Hoare CAR. An axiomatic basis for computer programming. Communications of the ACM, 1969,12(10):576–585. [doi: 10.1145/36 3235.363259]
    [57] Milner R. A Calculus of Communicating Systems. Heidelberg: Springer-Verlag, 1980.
    [58] Paulson LC. Isabelle: A generic theorem prover. LNCS 828, Heidelberg: Springer-Verlag, 1994.
    [59] Owre S, Rushby M, Shankar N. PVS: A prototype verification system. In: Kapur D, ed. Proc. of the 11th CADE. LNCS 607, Heidelberg: Springer-Verlag, 1992. 748-752. [doi: 10.1007/3- 540-55602-8_217]
    [60] Gordon M. Introduction to the HOL system. In: Archer M, Joyce JJ, Levitt KN, Windley PJ, eds. Proc. of the Int’l Workshop on the HOL Theorem Proving System and Its Applications. Davis: IEEE Computer Society, 1991. 2-3.
    [61] Liu J, Zhan N, Zhao H. Computing semi-algebraic invariants for polynomial dynamical systems. In: Chakraborty S, Jerraya A, Baruah SK, Fischmeister S, eds. Proc. of the Embedded Software (EMSOFT 2011). New York: ACM Press, 2011. 97-106. [doi: 10. 1145/2038642.2038659]
    [62] Liu J, Lv J, Quan Z, Zhan N, Zhao H, Zhou C, Zou L. A calculus for hybrid CSP. In: Ueda K, ed. Proc. of the APLAS 2010. LNCS 6461, Heidelberg: Springer-Verlag, 2010. 1-15. [doi: 10.1007/978-3-642-17164-2_1]
    [63] Sankaranarayanan S, Sipma H, Manna Z. Constructing invariants for hybrid systems. In: Alur R, Pappas GJ, eds. Proc. of the Hybrid Systems: Computation and Control. Heidelberg: Springer-Verlag, 2004. 539-554. [doi: 10.1007/978-3-540-24743-2_36]
    [64] Sankaranarayanan S. Automatic invariant generation for hybrid systems using ideal fixed points. In: Johansson KH, Wang Y, eds. Proc. of the Hybrid Systems: Computation and Control. New York, ACM, 2010. 221-230. [doi: 10.1145/1755952.1755984]
    [65] Gulwani S, Tiwari A. Constraint-Based approach for analysis of hybrid systems. In: Proc. of the Computer Aided Verification. Heidelberg: Springer-Verlag, 2008. 190-203. [doi: 10.1007/978-3-540-70545-1_18]
    [66] Zhao H, Zhan N, Kapur D. Synthesizing switching controllers for hybrid systems by generating invariants. In: Liu Z, Woodcock J, Zhu H, eds. Proc. of the Theories of Programming and Formal Methods. Berlin, Heidelberg: Springer-Verlag, 2013. 354-373. [doi: 10.1007/978-3-642-39698-4_22]
    [67] Prajna S, Jadbabaie A. Safety verification of hybrid systems using barrier certificates. In: Alur R, Pappas GJ, eds. Proc. of the Hybrid Systems: Computation and Control. Heidelberg: Springer-Verlag, 2004. 477-492. [doi: 10.1007/978-3-540-24743-2_32]
    [68] Tiwari A. Approximate reachability for linear systems. In: Maler O, Pnueli A, eds. Proc. of the Hybrid Systems: Computation and Control 2003. LNCS 2623, Heidelberg: Springer-Verlag, 2003. 514-525. [doi: 10.1007/3-540-36580-X_37]
    [69] Carbonell E, Tiwari A. Generating polynomial invariants for hybrid systems. In: Morari M, Thiele L, eds. Proc. of the Hybrid Systems: Computation and Control 2005. LNCS 3414, Heidelberg: Springer-Verlag, 2005. 590-605. [doi: 10.1007/978-3-540-3195 4-2_38]
    [70] Harel D, Kozen D, Tiuryn J. Dynamic Logic. Cambridge: The MIT Press, 2000.
    [71] Harel D. First-Order Dynamic Logic. In: Hansen PB, Gries D, Moler C, eds. Lecture Notes in Computer Science, Vol.68. Berlin, Heidelberg, New York: Springer-Verlag, 1979.
    [72] Platzer A, Clarke E. Computing differential invariants of hybrid systems as fixedpoints. Formal Methods in Systems Design, 2009, 35(1):98-120. [doi: 10.1007/s10703-009-0079-8]
    [73] Platzer A, Quesel JD. KeYmaera: A hybrid theorem prover for hybrid systems. In: Armando A, Baumgartner P, Dowek G, eds. Proc. of the Int’l Joint Conf. on Automated Reasoning. LNCS 5195, Berlin, Heidelberg: Springer-Verlag, 2008. 171-178. [doi: 10. 1007/978-3-540-71070-7_15]
    [74] Bu L, Wang QX, Chen X, Wang LZ, Zhang T, Zhao JH, Li XD. Toward online hybrid systems model checking of cyber-physical systems time-bounded short-run behavior. ACM SIGBED Review, 2011,8(2):7-10. [doi: 10.1145/2000367.2000368]
    [75] Platzer A. Quantified differential invariants. In: Caccamo M, Frazzoli E, Grosu R, eds. Proc. of the 14th ACM Int’l Conf. on Hybrid Systems: Computation and Control 2011. New York: ACM Press, 2011. 63-72. [doi: 10.1145/1967701.1967713]
    [76] Kwiatkowska M, Norman G, Parker D. Advances and challenges of probabilistic model checking. In: Proc. of the 48th Annual Allerton Conf. on Communication, Control and Computing. Allerton: IEEE Press, 2010. 1691-1698. [doi: 10.1109/ALLERTON. 2010.5707120]
    [77] Younes HLS, Simmons RG. Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma E, Larsen KG, eds. Proc. of the Computer Aided Verification. LNCS 2404, Berlin, Heidelberg: Springer-Verlag, 2002. 223-235. [doi: 10. 1007/3-540-45657-0_ 17]
    [78] Zhang L, She Z, Ratschan S, Hermanns H, Hahn EM. Safety verification for probabilistic hybrid systems. In: Touili T, Cook B, Jackson P, eds. Proc. of the Computer Aided Verification. Berlin, Heidelberg: Springer-Verlag, 2010. 196-211. [doi: 10.1007/978- 3-642-14295-6_21]
    [79] Hu J, Lygeros J, Sastry S. Towards a theory of stochastic hybrid systems. In: Lynch N, Krogh B, eds. Proc. of the Hybrid Systems: Computation and Control. LNCS 1790, Berlin, Heidelberg: Springer-Verlag, 2000. 160-173. [doi: 10.1007/3-540-46430-1_16]
    [80] Fränzle M, Hahn E, Hermanns H, Wolovick N, Zhang L. Measurability and safety verification for stochastic hybrid systems. In: Caccamo M, Frazzoli E, Grosu R, eds. Proc. of the 14th Int’l Conf. on Hybrid Systems: Computation and Control. Chicago: ACM Press, 2011. 43-52. [doi: 10.1145/1967701.1967710]
    [81] Abate A, Katoen J, Lygeros J, Prandini M. Approximate model checking of stochastic hybrid systems. European Journal of Control, 2010,16(6):624-641. [doi: 10.3166/ejc.16.624-641]
    [82] Abate A, Prandini M, Lygeros J, Sastry S. Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica, 2008,44(11):2724-2734. [doi: 10.1016/j.automatica.2008.03.027]
    [83] Fränzle M, Hermanns H, Teige T. Stochastic satisfiability modulo theory: A novel technique for the analysis of probabilistic hybrid systems. In: Egerstedt M, Mishra B, eds. Proc. of the Hybrid Systems: Computation and Control. LNCS 4981, Berlin, Heidelberg: Springer-Verlag, 2008. 172-186. [doi: 10.1007/978-3-540-78929-1_13]
    [84] David A, Larsen KG, Legay A, Mikucionis M, Wang Z. Time for statistical model checking of real-time systems. In: Gopalakrishnan G, Qadeer S, eds. Proc. of the Computer Aided Verification. LNCS 6806, Berlin, Heidelberg: Springer-Verlag, 2011. 349-355. [doi: 10.1007/978-3-642-22110-1_27]
    [85] Asarin E, Bournez O, Dang T, Maler O, Pnueli A. Effective synthesis of switching controllers for linear systems. Proc. of the IEEE, 2000,88(7):1011-25. [doi: 10.1109/5.871306]
    [86] Lygeros J, Tomlin C, Sastry S. Controllers for reachability specifications for hybrid systems. Automatica, 1999,35(3):349-370.[doi: 10.1016/S0005-1098(98)00193-9]
    [87] Tomlin C, Lygeros L, Sastry S. A game-theoretic approach to controller design for hybrid systems. Proc. of the IEEE, 2000,88(7): 949-970. [doi: 10.1109/5.871303]
    [88] Taly A, Gulwani S, Tiwari A. Synthesizing switching logic using constraint solving. In: Proc. of the Verification, Model Checking, and Abstract Interpretation. LNCS 5403, Berlin, Heidelberg: Springer-Verlag, 2009. 305-319. [doi: 10.1007/978-3-540-93900-9_ 25]
    [89] Taly A, Tiwari A. Switching logic synthesis for reachability. In: Carloni LP, Tripakis S, eds. Proc. of the 10th ACM Int’l Conf. on Embedded Software. New York: ACM Press, 2010. 19-28. [doi: 10.1145/1879021.1879025]
    [90] Cassez F, Jessen JJ, Larsen KG, Raskin JF, Reynier PA. Automatic synthesis of robust and optimal controllers—An industrial case study. In: Majumdar R, Tabuada P, eds. Proc. of the Hybrid Systems: Computation and Control. LNCS 5469, Berlin, Heidelberg: Springer-Verlag, 2009. 90-104. [doi: 10.1007/978-3-642-00602-9_7]
    [91] Jha S, Seshia S, Tiwari A. Synthesis of optimal switching logic for hybrid systems. In: Chakraborty S, Jerraya A, Baruah SK, Fischmeister S, eds. Proc. of the Embedded Software (EMSOFT 2011). New York: ACM Press: IEEE, 2011. 107-116. [doi: 10. 1145/2038642.2038 660]
    [92] Zhao H, Zhan N, Kapur D, Larsen K. A “Hybrid” approach for synthesizing optimal controllers of hybrid systems: A case study of the oil pump industrial example. In: Giannakopoulou D, Méry D. eds. Proc. of the Formal Methods (FM 2012). LNCS 7436, Berlin, Heidelberg: Springer-Verlag, 2012. 471-485. [doi: 10.1007/978-3-642-32759-9_38]
    [93] Chaudhuri S, Solar-Lezama A. Smooth interpretation. ACM Sigplan Notices, 2010,45(6):279-291. [doi: 10.1145/1809028.18066 29]
    [94] Hedlund S, Rantzer A. Optimal control of hybrid systems. In: Proc. of the 38th IEEE Conf. on Decision and Control, Vol.4. Phoenix: IEEE, 1999. 3972-3977.
    [95] Xu J, Chen Q. Optimal control of switched hybrid systems. In: Proc. of the 2011 8th Asian Control Conf. (ASCC). Kaohsiung: IEEE, 2011. 1216-1220.
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

卜磊,解定宝.混成系统形式化验证.软件学报,2014,25(2):219-233

复制
分享
文章指标
  • 点击次数:5847
  • 下载次数: 9690
  • HTML阅读次数: 3143
  • 引用次数: 0
历史
  • 收稿日期:2013-05-07
  • 最后修改日期:2013-09-29
  • 在线发布日期: 2014-01-26
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第19727936位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号