Lazy Linear Hybrid Automata (FORMATS 07) Lazy linear hybrid automata (LLHA) model the discrete time behavior of control systems containing finite-precision sensors and actuators interacting with their environment under bounded inertial delays. In this paper, we present a symbolic technique for reachability analysis of lazy linear hybrid automata. The model permits only linear flow constraints but the invariants and guards can be any computable function. We present an abstraction hierarchy for LLHA. Our verification technique is based on bounded model  checking and k-induction for reachability analysis at different levels of the abstraction hierarchy within an abstraction-refinement framework. The counterexamples obtained during BMC are used to construct refinements in each iteration. Our technique is practical and compares favorably with state- of-the-art tools, as demonstrated on examples that include the Air Traffic Alert and Collision Avoidance System (TCAS). Click here for the paper Experimental Results for LLHA

BACK

	Our experimental results on two case studies - Automated Highway System and Traffic Collision Avoidance System are detailed below. The UCLID, Phaver and HSolver models are also available for download at links given below. Feedbacks and suggestions would be welcome !

	1. Automated Highway System (AHS)

We used BMC+Induction on a 0-abstraction of the AHS model. The 0-abstraction is same as the model of Agrawal-Thiagarajan HSSC’05 work. No abstraction refinement was required for this example. This case study was used to show the scalability of our symbolic model checking approach for lazy linear hybrid automata. As presented in results below, we were able to compute reachability for AHS with 120 cars in less than 2 minutes. The Phaver tool took more than 10 hours to handle AHS examples with more than 15 cars.

	Click here for Models and Results.

There are 4 cars moving at some speed between $a$ and $f$. Whenever the distance between them decreases below $\alpha$, controller recognizes that there is a possibility of collision and moves to recovery mode (for 1,2 or 2,3 or 3,4) depending on which cars are involved. The cars involved are asked to change their speed : the ahead one is asked to increase to range of $d$ to $e$ and the behind one is required to change its speed to $b$ to $c$; the other cars ahead of these two are required to change speed to $ru$ and those behind to $rl$. If the distance between cars goes below $\alpha'$, it is inferred that the cars have collided

Runtime For AHS model using Phaver

Runtime For AHS Analysis using our technique

Our technique took less than 2 seconds for analysis using UCLID decision procedure.  Including the time to generate the model, it took less than 2 minutes. Phaver took more than 10 hours for models of size greater than 15. For 14 cars, Phaver took more than 1 hour while our technique took less than 1 second for SAT solving and 16.71 seconds including the model generation time. Runtime for larger models 2. Traffic Collision Avoidance System (TCAS). TCAS example has being a difficult example in literature. Due to non-linear invariants, Phaver could not be used over this example. HSolver was used to model TCAS with same parameters as UCLID for a turn angle of 30 degree. The reachability computation of HSolver did not terminate in 3 hours. As presented in result below, our technique took less than 15 minutes for any instance of the example. The abstraction technique was tested using this example. Clearly, the reachability query could be answered for a 16-abstraction in less than 20 seconds for this example. All levels of abstraction from 0 to 16 in this example showed that the error state was not reachable. This shows that instead of considering the concrete model, crude over-approximations constructed using our hierarchical abstraction can be used to decrease the run-time of answering reachability queries significantly. Thus, the abstraction-refinement technique makes our symbolic analysis method more scalable. Click here for Models The runtime for our technique with different levels of abstraction are presented below, with varying deviation angles. BACK TO TOP

BACK to HomePage