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

王佳宛 等: 基于混成自动机路径过滤与动态选择的 CPS 系统反例生成 3601

借助这类研究方法来生成系统的混成自动机模型, 再应用本文的方法进行基于路径的系统反例生成. 我们未来的
工作也计划进一步探索如何结合深度学习等技术, 学习系统模型的关键结构信息以用于路径生成与过滤, 以应对
日益复杂的 CPS 系统在缺乏形式化模型信息时对反例生成带来的挑战.

References:
[1] Alur R. Principles of Cyber-physical Systems. London: The MIT Press, 2015.
[2] Lee EA, Seshia SA. Introduction to Embedded Systems: A Cyber-physical Systems Approach. 2nd ed., Cambridge: MIT Press, 2017.
[3] 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]
[4] Doyen L, Frehse G, Pappas GJ, Platzer A. Verification of hybrid systems. In: Clarke EM, Henzinger TA, Veith H, Bloem R, eds.
Handbook of Model Checking. Cham: Springer, 2018. 1047–1110. [doi: 10.1007/978-3-319-10575-8_30]
[5] Henzinger TA, Kopke PW, Puri A, Varaiya P. What’s decidable about hybrid automata? In: Proc. of the 27th Annual ACM Symp. on
Theory of Computing. Las Vegas: ACM, 1995. 373–382. [doi: 10.1145/225058.225162]
[6] Kapinski J, Deshmukh JV, Jin XQ, Ito H, Butts K. Simulation-based approaches for verification of embedded control systems: An
overview of traditional and advanced modeling, testing, and verification techniques. IEEE Control Systems Magazine, 2016, 36(6):
45–64. [doi: 10.1109/MCS.2016.2602089]
[7] Nghiem T, Sankaranarayanan S, Fainekos G, Ivancić F, Gupta A, Pappas GJ. Monte-Carlo techniques for falsification of temporal
properties of non-linear hybrid systems. In: Proc. of the 13th ACM Int’l Conf. on Hybrid Systems: Computation and Control. Stockholm:
ACM, 2010. 211–220. [doi: 10.1145/1755952.1755983]
[8] Annapureddy YSR, Fainekos GE. Ant colonies for temporal logic falsification of hybrid systems. In: Proc. of the 36th Annual Conf. on
IEEE Industrial Electronics Society. Glendale: IEEE, 2010. 91–96. [doi: 10.1109/IECON.2010.5675195]
[9] Sankaranarayanan S, Fainekos G. Falsification of temporal properties of hybrid systems using the cross-entropy method. In: Proc. of the
15th ACM Int’l Conf. on Hybrid Systems: Computation and Control. Beijing: ACM, 2012. 125–134. [doi: 10.1145/2185632.2185653]
[10] Annpureddy Y, Liu C, Fainekos G, Sankaranarayanan S. S-TALIRO: A tool for temporal logic falsification for hybrid systems. In: Proc.
of the 17th Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Saarbrücken: Springer, 2011. 254–257.
[doi: 10.1007/978-3-642-19835-9_21]
[11] Donzé A. Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Proc. of the 22nd Int’l Conf. on Computer
Aided Verification. Edinburgh: Springer, 2010. 167–170. [doi: 10.1007/978-3-642-14295-6_17]
[12] Akazaki T, Liu S, Yamagata Y, Duan YH, Hao JY. Falsification of cyber-physical systems using deep reinforcement learning. In: Proc. of
the 22nd Int’l Symp. on Formal Methods. Oxford: Springer, 2018. 456–465. [doi: 10.1007/978-3-319-95582-7_27]
[13] Wang JW, Bu L, Xing SP, Li XD. PDF: Path-oriented, derivative-free approach for safety falsification of nonlinear and nondeterministic
CPS. IEEE Trans. on Computer-aided Design of Integrated Circuits and Systems, 2022, 41(2): 238–251. [doi: 10.1109/TCAD.2021.
3056360]
[14] Wang JW, Liu WX, Zhang MM, Wei JQ, Shi YH, Bu L, Li XD. Scenario-based flexible modeling and scalable falsification for
reconfigurable CPSs. In: Proc. of the 36th Int’l Conf. on Computer Aided Verification. Montreal: Springer, 2024. 329–355. [doi: 10.1007/
978-3-031-65633-0_15]
[15] Fainekos GE, Pappas GJ. Robustness of temporal logic specifications for continuous-time signals. Theoretical Computer Science, 2009,
410(42): 4262–4291. [doi: 10.1016/j.tcs.2009.06.021]
[16] Donzé A, Maler O. Robust satisfaction of temporal logic over real-valued signals. In: Proc. of the 8th Int’l Conf. on Formal Modeling and
Analysis of Timed Systems. Klosterneuburg: Springer, 2010. 92–106. [doi: 10.1007/978-3-642-15297-9_9]
[17] Mathesen L, Yaghoubi S, Pedrielli G, Fainekos G. Falsification of cyber-physical systems with robustness uncertainty quantification
through stochastic optimization with adaptive restart. In: Proc. of the 15th IEEE Int’l Conf. on Automation Science and Engineering
(CASE). Vancouver: IEEE, 2019. 991–997. [doi: 10.1109/COASE.2019.8843005]
[18] Yaghoubi S, Fainekos G. Falsification of temporal logic requirements using gradient based local search in space and time. IFAC-
PapersOnLine, 2018, 51(16): 103–108. [doi: 10.1016/j.ifacol.2018.08.018]
[19] Zhang ZY, Ernst G, Sedwards S, Arcaini P, Hasuo I. Two-layered falsification of hybrid systems guided by Monte Carlo tree search.
IEEE Trans. on Computer-aided Design of Integrated Circuits and Systems, 2018, 37(11): 2894–2905. [doi: 10.1109/TCAD.2018.
2858463]
[20] Plaku E, Kavraki LE, Vardi MY. Hybrid systems: From verification to falsification by combining motion planning and discrete search.