Page 179 - 《软件学报》2025年第8期

3602 软件学报 2025 年第 36 卷第 8 期

Formal Methods in System Design, 2009, 34(2): 157–182. [doi: 10.1007/s10703-008-0058-5]
[21] Dang T, Nahhal T. Coverage-guided test generation for continuous and hybrid systems. Formal Methods in System Design, 2009, 34(2):
183–213. [doi: 10.1007/s10703-009-0066-0]
[22] Dreossi T, Dang T, Donzé A, Kapinski J, Jin XQ, Deshmukh JV. Efficient guiding strategies for testing of temporal properties of hybrid
systems. In: Proc. of the 7th Int’l Symp. on NASA Formal Methods. Pasadena: Springer, 2015. 127–142. [doi: 10.1007/978-3-319-17524-
9_10]
[23] Zutshi A, Sankaranarayanan S, Deshmukh JV, Kapinski J. A trajectory splicing approach to concretizing counterexamples for hybrid
systems. In: Proc. of the 52nd IEEE Conf. on Decision and Control. Firenze: IEEE, 2013. 3918–3925. [doi: 10.1109/CDC.2013.6760488]
[24] Zutshi A, Deshmukh JV, Sankaranarayanan S, Kapinski J. Multiple shooting, CEGAR-based falsification for hybrid systems. In: Proc. of
the 14th Int’l Conf. on Embedded Software. New Delhi: ACM, 2014. 5. [doi: 10.1145/2656045.2656061]
[25] Bogomolov S, Frehse G, Gurung A, Li DX, Martius G, Ray R. Falsification of hybrid systems using symbolic reachability and trajectory
splicing. In: Proc. of the 22nd ACM Int’l Conf. on Hybrid Systems: Computation and Control. Montreal: ACM, 2019. 1–10. [doi: 10.
1145/3302504.3311813]
[26] Bardin S, Herrmann P. Pruning the search space in path-based test generation. In: Proc. of the 2009 Int’l Conf. on Software Testing
Verification and Validation. Denver: IEEE, 2009. 240–249. [doi: 10.1109/ICST.2009.15]
[27] Xie DB, Bu L, Zhao JH, Li XD. SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata. Formal
Methods in System Design, 2014, 45(1): 42–62. [doi: 10.1007/s10703-014-0210-3]
[28] Kuznetsov V, Kinder J, Bucur S, Candea G. Efficient state merging in symbolic execution. In: Proc. of the 33rd ACM SIGPLAN Conf.
on Programming Language Design and Implementation. Beijing: ACM, 2012. 193–204. [doi: 10.1145/2254064.2254088]
[29] Staats M, Pǎsǎreanu CS. Parallel symbolic execution for structural test generation. In: Proc. of the 19th Int’l Symp. on Software Testing
and Analysis. Trento: ACM, 2010. 183–194. [doi: 10.1145/1831708.1831732]
[30] Bu L, Zhao JH, Li XD. Path-oriented reachability verification of a class of nonlinear hybrid automata using convex programming. In:
Proc. of the 11th Int’l Conf. on Verification, Model Checking, and Abstract Interpretation. Madrid: Springer, 2010. 78–94. [doi: 10.1007/
978-3-642-11319-2_9]
[31] Bu L, Wang JW, Wu YM, Li XD. From bounded reachability analysis of linear hybrid automata to verification of industrial CPS and IoT.
In: Proc. of the 5th Int’l School on Engineering Trustworthy Software Systems. Chongqing: Springer, 2020. 10–43. [doi: 10.1007/978-3-
030-55089-9_2]
[32] Xing SP, Wang JW, Bu L, Chen X, Li XD. Approximate optimal hybrid control synthesis by classification-based derivative-free
optimization. In: Proc. of the 24th Int’l Conf. on Hybrid Systems: Computation and Control. Nashville: ACM, 2021. 7. [doi: 10.1145/
3447928.3456658]
[33] Maler O, Nickovic D. Monitoring temporal properties of continuous signals. In: Proc. of the 2004 Joint Int’l Conf. on Formal Modeling
and Analysis of Timed Systems, FORMATS 2004 and Formal Techniques in Real Time and Fault-tolerant Systems, FTRTFT 2004.
Grenoble: Springer, 2004. 152–166. [doi: 10.1007/978-3-540-30206-3_12]
[34] Berry DA, Fristedt B. Bandit Problems: Sequential Allocation of Experiments (Monographs on Statistics and Applied Probability).
Dordrecht: Springer, 1985. 1–274. [doi: 10.1007/978-94-015-3711-7]
[35] Auer P, Cesa-Bianchi N, Fischer P. Finite-time analysis of the multiarmed bandit problem. Machine Learning, 2002, 47(2): 235–256.
[doi: 10.1023/A:1013689704352]
[36] De Moura L, Bjørner N. Z3: An efficient SMT solver. In: Proc. of the 14th Int’l Conf. on Tools and Algorithms for the Construction and
Analysis of Systems. Budapest: Springer, 2008. 337–340. [doi: 10.1007/978-3-540-78800-3_24]
[37] Fisher ME. A semiclosed-loop algorithm for the control of blood glucose levels in diabetics. IEEE Trans. on Biomedical Engineering,
1991, 38(1): 57–61. [doi: 10.1109/10.68209]
[38] Fehnker A, Ivančić F. Benchmarks for hybrid systems verification. In: Proc. of the 7th Int’l Workshop on Hybrid Systems: Computation
and Control. Philadelphia: Springer, 2004. 326–341. [doi: 10.1007/978-3-540-24743-2_22]
[39] Minopoli S, Frehse G. SL2SX translator: From simulink to SpaceEx models. In: Proc. of the 19th Int’l Conf. on Hybrid Systems:
Computation and Control. Vienna: ACM, 2016. 93–98. [doi: 10.1145/2883817.2883826]
[40] García Soto M, Henzinger TA, Schilling C, Zeleznik L. Membership-based synthesis of linear hybrid automata. In: Proc. of the 31st Int’l
Conf. on Computer Aided Verification. New York: Springer, 2019. 297–314. [doi: 10.1007/978-3-030-25540-4_16]
[41] Jin XY, An J, Zhan BH, Zhan NJ, Zhang MM. Inferring switched nonlinear dynamical systems. Formal Aspects of Computing, 2021,
33(3): 385–406. [doi: 10.1007/s00165-021-00542-7]
[42] Yang X, Beg OA, Kenigsberg M, Johnson TT. A framework for identification and validation of affine hybrid automata from input-output