logo

SCIENTIA SINICA Informationis, Volume 47, Issue 3: 288-309(2017) https://doi.org/10.1360/N112016-00042

Composed IIS path locating based optimization for bounded \\reachability analysis of compositional linear hybrid systems}{Composed IIS path locating based optimization for bounded reachability analysis of compositional linear hybrid systems

More info
  • ReceivedMar 2, 2016
  • AcceptedMay 31, 2016
  • PublishedSep 14, 2016

Abstract

Hybrid systems include both discrete and continuous behavior and are widely used to model control systems. The reachability analysis of its unsafe state is an important method for guaranteeing the safety of a system. However, the current techniques do not scale well to the problems of practical interest. Due to the synchronization of components and the combinatorial explosion of state space, the reachability analysis of compositional linear hybrid system is extremely complex. In order to reduce the complexity, a path-oriented approach was proposed in a previous work, which conducted bounded reachability analysis of a compositional linear hybrid system. By enumerating and verifying each potential path one by one, the size of the problem that can be solved will be increased substantially. This path-oriented approach will become quite inefficient due to a sharp increase in the number of candidate paths when analyzing complex systems. The path explosion problem in model checking is also famous. To solve this problem, we propose a state-space reduction technique, which accelerates the verification process. We propose a method to locate the cause of infeasibility, when a composed infeasible path segment after a path set is proved to be infeasible. As we can simply falsify a path set that contains a composed infeasible path segment, the number of candidate paths can be reduced significantly. Furthermore, to avoid such composed path segments efficiently, we propose an approach based on satisfiability modulo theories (SMT), to traverse the bounded graph structure of the composed linear hybrid system. The results of the experiment show that the performance of the path-oriented bounded reachability analysis can be optimized significantly and that the overall performance of the proposed approach is better than that of the state-of-the-art competitor.


Funded by

国家重点基础研究发展计划(973)

(2014CB340703)

国家自然科学基金(61561146394)

国家自然科学基金(61572249)

国家自然科学基金(61321491)


References

[1] Clarke E, Grumberg O, Peled D. Model Checking. Cambridge: MIT Press, 1999. Google Scholar

[2] Henzinger T A. The theory of hybrid automata. In: Proceedings of the 11st Annual IEEE Symposium on Logic in Computer Science, New Brunswick, 1996. 278-292. Google Scholar

[3] Henzinger T A, Kopke P W, Puri A, et al. What's decidable about hybrid automata? J Comput Syst Sci, 1998, 57: 94-124. Google Scholar

[4] Henzinger T A, Ho P H, Wong-Toi H. HYTECH: a model checker for hybrid systems. Softw Tools Techn Transfer, 1997, 1: 110-122. Google Scholar

[5] Frehse G. PHAVer: algorithmic verification of hybrid systems past HyTech. In: Hybrid Systems: Computation and Control. Berlin: Springer, 2005. 258-273. Google Scholar

[6] Frehse G, Guernic C L, Donzé A, et al. SpaceEx: scalable verification of hybrid systems. In: Computer Aided Verification. Berlin: Springer, 2011. 379-395. Google Scholar

[7] Biere A, Cimatti A, Clarke E, et al. Bounded model checking. Advance Comput, 2003, 58: 118-149. Google Scholar

[8] Barrett C W, Sebastiani R, Seshia S, et al. Satisifiability modulo theories. Handbook of Satisfiability, 2009, 185: 825-885. Google Scholar

[9] Audemard G, Bozzano M, Cimatti A, et al. Verifying industrial hybrid systems with MathSAT. Electron Notes Theor Comput Sci, 2005, 119: 17-32 CrossRef Google Scholar

[10] de Moura L, Bj{\o}rner N. Z3: an efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer, 2008. 337-340. Google Scholar

[11] Li X D, Jha S K, Bu L. Towards an efficient path-oriented tool for bounded reachability analysis of linear hybrid systems using linear programming. Electron Notes Theor Comput Sci, 2007, 174: 57-70. Google Scholar

[12] Bu L, Li Y, Wang L Z, et al. BACH 2: bounded reach ability checker for compositional linear hybrid systems. In: Proceedings of the 13th Design Automation & Test in Europe Conference, Leuven, 2010. 1512-1517. Google Scholar

[13] Xie D B, Bu L, Zhao J H, et al. SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata. Formal Methods Syst Design, 2014, 45: 42-62 CrossRef Google Scholar

[14] Bu L, Yang Y, Li X D. IIS-guided DFS for efficient bounded reachability analysis of linear hybrid automata. In: Proceedings of the 7th International Haifa Verification Conference, Haifa, 2011. 35-49. Google Scholar

[15] Mark L, Ammar M. Enumerating infeasibility: finding multiple MUSes quickly. In: Proceedings of the 10th International Conference on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming, Yorktown Heights, 2013. 160-175. Google Scholar

[16] Bu L, Li Y, Wang L Z, et al. BACH: bounded reachability checker for linear hybrid automata. In: Proceedings of the 8th International Conference on Formal Methods in Computer Aided Design, Portland, 2008. 65-68. Google Scholar

[17] Cimatti A, Griggio A, Mover S, et al. HyComp: an SMT-based model checker for hybrid systems. In: Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer, 2015. 52-67. Google Scholar

[18] Bu L, Li X D. Path-oriented bounded reachability analysis of composed linear hybrid systems. Int J Softw Tools Tech Transfer, 2011, 13: 307-317 CrossRef Google Scholar

[19] Chinneck J, Dravnieks E. Locating minimal infeasible constraint sets in linear programs. ORSA J Comput, 1991, 3: 157-168 CrossRef Google Scholar

[20] Biere A, Clarke E, Zhu Y S. Symbolic model checking without BDDs. In: Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer, 1999. 193-207. Google Scholar

[21] Xie D B, Bu L, Li X D. Deriving unbounded proof of linear hybrid automata from bounded verification. In: Proceedings of Real-Time Systems Symposium (RTSS), Rome, 2014. 128-137. Google Scholar

[22] Zhao J H, Li X D, Zheng T, et al. Removing irrelevant atomic formulas for checking timed automata efficiently.\linebreak In: Formal Modeling and Analysis of Timed Systems. Berlin: Springer, 2004. 34-45. Google Scholar

[23] Jha S, Krogh B H, Weimer J E, et al. Reachability for linear hybrid automata using iterative relaxation abstraction. In: Hybrid Systems: Computation and Control. Berlin: Springer, 2007. 287-300. Google Scholar

[24] Wang F. Symbolic parametric safety analysis of linear hybrid systems with BDD-like data structures. IEEE Trans Softw Eng, 2005, 31: 38-51 CrossRef Google Scholar

[25] Bu L, Cimatti A, Li X D, et al. Model checking of hybrid systems using shallow synchronzation. In: Formal Techniques for Distributed Systems. Berlin: Springer, 2010. 155-169. Google Scholar

[26] Heljabko K, Niemala I. Bounded LTL model checking with stable models. In: Theory and Practice of Logic Programming. Cambridge: Cambridge University Press, 2003. 519-550. Google Scholar

Copyright 2020 Science China Press Co., Ltd. 《中国科学》杂志社有限责任公司 版权所有

京ICP备18024590号-1