Search

The crowd flows prediction plays an important role in urban planning management and urban public safety. Accuracy is a challenge for predicting the flow of crowds in a region. On the one hand, crowd flow is influenced by many factors such as holidays and weather. On the other hand, sample data about crowd flows are generally high-dimensional, which not only has a negative impact on the prediction accuracy but also increases computational complexity. In this paper, an efficiency-enhanced model is constructed for predicting citywide crowd flows based on multi-source data using deep learning techniques. Specifically, a data reconstruction mechanism is built with Bernoulli restricted Boltzmann machine (BRBM), for the purpose of reducing the dimension of sample data. A collaborative prediction mechanism is introduced to improve the prediction accuracy of crowd flows, in which a spatio-temporal data oriented prediction model is constructed based on bottleneck residual network that can reduce the effectively computational complexity of model training, and an auxiliary prediction to further optimize the prediction accuracy based on the fully-connected network. The proposed method is evaluated by using two open datasets. The experimental results show that our method can significantly improve the prediction accuracy and reduce the training time of the prediction model, compared with other methods.

As a complementary technology to Binary Decision Diagram-based (BDD-based) symbolic model checking, the verification techniques on Boolean satisfiability problem have gained an increasing wide of applications over the last few decades, which brings a dramatic improvement for automatic verification. In this paper, we firstly introduce the theory about the Boolean satisfiability verification, including the description on the problem of Boolean satisfiability verification, Davis-Putnam-Logemann-Loveland (DPLL) based complete verification algorithm, and all kinds of solvers generated and the logic languages used by those solvers. Moreover, we formulate a large number optimizations of technique revolutions based on Boolean SATisfiability (SAT) and Satisfiability Modulo Theories (SMT) solving in detail, including incomplete methods such as bounded model checking, and other methods for concurrent programs model checking. Finally, we point out the major challenge pervasively in industrial practice and prospect directions for future research in the field of formal verification.

Web-services are highly distributed programs, and concurrent software is notoriously error-prone. Model checking is a powerful technique to find bugs in concurrent systems. However, the existing model checkers have no enough ability to support for the programming languages and communication mechanisms used for Web services. We propose to use Kripke structures as means of modeling Web service. This paper presents an automated way to extract formal models from programs implementing Web services using predicate abstraction for abstract model checking. The abstract models are checked by means of a model checker that implements automatic abstraction refinement. These results enable the verification of the applications that implement Web services.

Category Partition Method (CPM) is a general approach to specification-based program testing, where test frame reduction and refinement are two important issues. Test frame reduction is necessary since too many test frames may be produced, and test frame refinement is important since during CPM testing new information about test frame generation may be achieved and considered incrementally. Besides the information provided by testers or users, implementation related knowledge offers alternative information for reducing and refining CPM test frames. This paper explores the idea by proposing a call patterns semantics based test frame updating method for Prolog programs, in which a call patterns analysis is used to collect information about the way in which procedures are used in a program. The updated test frames will be represented as constraints. The effect of our test frame updating is two-fold. On one hand, it removes "uncared" data from the original set of test frames; on the other hand, it refines the test frames to which we should pay more attention. The first effect makes the input domain on which a procedure must be tested a subset of the procedure's input domain, and the latter makes testers stand more chance to find out the faults that are more likely to show their presence in the use of the program under consideration. Our test frame updating method preserves the effectiveness of CPM testing with respect to the detection of faults we care. The test case generation from the updated set of test frames is also discussed. In order to show the applicability of our method an approximation call patterns semantics is proposed, and the test frame updating on the semantics is illustrated by an example.