When the nodes in the network are deployed in the target area with an appropriate density, the effective aggregation and transmission of the data gathered in the monitoring area remain to be solved. The existing Compressed Sensing (CS) based on data aggregation schemes are accomplished in a centralized manner and the Sink node achieves the task of data aggregation. However, these existing schemes may suffer from load imbalance and coverage void issues. In order to address these problems, we propose a Compressed Sensing based on Fault-tolerant Correcting Data Aggregation (CS-FCDA) scheme to accurately reconstruct the compressed data. Therefore, the network communication overhead can be greatly reduced while maintaining the quality of the reconstructed data. Meanwhile, we adopt the node clustering mechanism to optimize and balance the network load. It is shown via simulation results, compared with other data aggregation schemes, that the proposed scheme shows obvious improvement in terms of the Fault-tolerant correcting capability and the network energy efficiency of the data reconstruction.

The core of the abstraction-refinement verification is the analysis of the counterexample and refinement of the abstract model, which are the most expensive parts of the verification procedure. In this paper, we present a method that aims at reducing the complexity as much as possible. Our method combines the qualitative analysis with the reachability analysis. Qualitative analysis checks the feasibility of pair-wise transitions without the explicit numerical reachability computation. While reachability analysis employs bidirectional analysis strategy to minimize the region to be refined. Experiment shows that the integration of these strategies and techniques make the verification more efficient.

This paper demonstrate a novel methodology for safety verification of hybrid systems. The methodology uses functions of state termed barrier certificates that guarantee the safety requirement of hybrid systems, instead of computing reachable sets. The barrier certificates can be computed using the sum of squares decomposition and semidefinite programming. The unmanned aerial vehicles which used to perform a given mission and execute the flight plan are modeled by hybrid automata. Barrier certificates are constructed using the software SOSTOOLS for safety verification of flight plans of unmanned aircraft.