×

SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata. (English) Zbl 1317.68126

Summary: As discrete jumps and continuous flows tangle in the behavior of linear hybrid automata (LHA), the bounded model checking (BMC) for reachability of LHA is a challenging problem. Current works try to handle this problem by encoding all the discrete and continuous behaviors in the bound into a set of SMT formulas which can then be solved by SMT solvers. However, when the system size is large, the object SMT problem could be huge and difficult to solve. Instead of encoding everything into one constraint set, this paper proposes a SAT-LP-IIS joint-directed solution to conduct the BMC for reachability of LHA in a layered way. First, the bounded graph structure of LHA is encoded into a propositional formula set, and solved by SAT solvers to find potential paths which can reach the target location on the graph. Then, the feasibility of certain path is encoded into a set of linear constraints which can then be solved by linear programming (LP) efficiently. If the path is not feasible, irreducible infeasible set (IIS) technique is deployed to locate an infeasible path segment which will be fed to the SAT solver to accelerate the enumerating process. Experiments show that by this SAT-LP-IIS joint-directed solution, the memory usage of the BMC of LHA is well-controlled and the performance outperforms the state-of-the-art SMT-style competitors significantly.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q45 Formal languages and automata
90C05 Linear programming
Full Text: DOI

References:

[1] Henzinger TA (1996) The theory of hybrid automata. In: Proceedings of LICS 1996. IEEE Computer Society, pp 278-292 · Zbl 0959.68073
[2] Clarke E, Grumberg O, Peled D (1999) Model checking. MIT Press, Cambridge, MA · Zbl 0847.68063
[3] Henzinger TA, Kopke PW, Puri A, Varaiya P (1998) What’s decidable about hybrid automata? J Comput Syst Sci 94-124 · Zbl 0920.68091
[4] Henzinger TA, Ho P, Wong-Toi H (1998) Algorithmic analysis of nonlinear hybrid systems. In: IEEE transactions on automatic control, pp 540-554 · Zbl 0918.93019
[5] Alur R, Courcoubetis C, Halbwachs N et al. (1995) The algorithmic analysis of hybrid systems. Theor Comput Sci 138(1):3-34 · Zbl 0874.68206
[6] Frehse G (2005) PHAVer: algorithmic verification of hybrid systems past HyTech. In: Proceedings of HSCC’05, LNCS 2289, pp 258-273 · Zbl 1078.93533
[7] Frehse G, Guernic CL, Donzé A et al. (2011) SpaceEx: scalable verification of hybrid systems. In: CAV, pp 379-395
[8] Biere A, Cimatti A, Clarke E, Strichman O, Zhu Y (2003) Bounded model checking. In: Advance in computers, vol 58, Academic Press, London, pp 118-149
[9] Barrett CW, Sebastiani R, Seshia SA, Tinelli C (2009) Satisifiability modulo theories. In: Handbook of satisfiability, pp 825-885
[10] Audemard G, Bozzano M, Cimatti A et al. (2005) Verifying industrial hybrid systems with MathSAT. In: Proceedings of BMC2004, ENTCS, vol 119, Issue 2, Elsevier Science, pp 17-32 · Zbl 1272.68220
[11] de Moura L, Bjørner N (2008) Z3: an efficient SMT solver. In: Tools and algorithms for the construction and analysis of systems (TACAS), LNCS, vol 4963, pp 337-340
[12] Li X, Jha S, Bu L (2007) Towards an efficient path-oriented tool for bounded reachability analysis of linear hybrid systems using linear programming. In: Proceedings of BMC06, ENTCS, vol 174, Issue 3, Elsevier Science, pp 57-70 · Zbl 1277.68139
[13] Bu L, Li X (2011) Path-oriented bounded reachability analysis of composed linear hybrid systems. Softw Tools Technol Transf, 13(4):307-317
[14] Bu L, Li Y, Wang L, Li X (2008) BACH: bounded reachability checker for linear hybrid automata. In: FMCAD’08. IEEE Computer Society, pp 65-68
[15] Biere A, Clarke E, Zhu Y (1999) Symbolic model checking without BDDs. In: TACAS’99, LNCS 1579. Springer, Berlin · Zbl 1046.68578
[16] Chinneck J, Dravnieks E (1991) Locating minimal infeasible constraint sets in linear programs. ORSA J Comput 3:157-168 · Zbl 0755.90055 · doi:10.1287/ijoc.3.2.157
[17] Eé n N, Sörensson N (2004) An extensible SAT-solver. In: Theory and applications of satisfiability testing, vol 2919, pp 502-518 · Zbl 1204.68191
[18] CPLEX. http://www-01.ibm.com/software/integration/optimization/cplex-optimizer/ · Zbl 0755.90055
[19] SAT4J. http://www.sat4j.org/
[20] Jha S, Krogh BH, Weimer JE, Clarke EM (2007) Reachability for linear hybrid automata using iterative relaxation abstraction. In: Proceedings of HSCC’07, pp 287-300 · Zbl 1221.93115
[21] runlim. http://fmv.jku.at/runlim/
[22] Cimatti A, Mover S, Tonetta S (2012) SMT-based verification of hybrid systems. In: AAAI · Zbl 1284.03216
[23] Cimatti A, Mover S, Tonetta S, (2013) SMT-based scenario verification for hybrid systems. Formal Methods Syst Des 42:46-66 · Zbl 1284.03216
[24] Bruttomesso R et al. (2008) The MathSAT 4 SMT Solver. In: CAV, pp 299-303
[25] Audemard G et al. (2002) Bounded model checking for timed systems. In: Proceedings of conference on formal techniques for networked and distributed systems. In: LNCS 2529, pp 243-259 · Zbl 1037.68549
[26] Franzle M, Herde C (2007) HySAT: an efficient proof engine for bounded model checking of hybrid systems. Form Methods Syst Des 30(3):179-198 · Zbl 1116.68048
[27] Ábrahám E, Becker B, Klaedtke F, Steffen M (2005) Optimizing bounded model checking for linear hybrid systems. In: Proceedings of VMCAI 2005, LNCS, vol 3385, pp 396-412 · Zbl 1111.68493
[28] Sheeran M, Singh S, Stalmarck G (2000) Checking safety properties using induction and a SAT solver. In: FMCAD, pp 108-125
[29] Jha S, Brady BA, Seshia SA (2007) Seshia symbolic reachability analysis of lazy linear hybrid automata. In: Formal modeling and analysis of timed systems, vol 4763. Springer, Berlin, pp 241-256 · Zbl 1141.93352
[30] Clarke E et al (2000) Counterexample-guided abstraction refinement. In: CAV 2000, LNCS 1855. Springer, Heidelberg, pp 154-169 · Zbl 0974.68517
[31] Fehnker A, Clarke E, Kumar Jha S, Krogh B (2005) Refining abstractions of hybrid systems using counterexample fragments. In: Proceedings of HSCC’05, pp 242-257 · Zbl 1078.93041
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.