Node.js has become one of the most popular development platforms due to its superior concurrency support. However, races induced by the nondeterministic execution order of event handlers may occur in Node.js applications, causing serious runtime failures. The state-of-the-art Node.js race detector NRace builds a happens-before (HB) graph before detection with a set of HB relation rules. In detection, NRace utilizes a heavy-weight BFS-based algorithm to query the reachability between resource operations, which introduces substantial overhead in practice, causing NRace inapplicable to real-world Node.js application test processes. This paper proposes a more practical Node.js dynamic race detection approach called NodeRT (Node.js Race Tracker). To reduce unnecessary overhead, NodeRT simplifies the HB relation rules, and divides the detection into three stages: trace collection stage, race candidate detection stage, and false positive removal stage. In the trace collection stage, NodeRT constructs a partial HB graph called asynchronous call tree (ACTree), enabling efficient reachability queries between event handlers. In the race candidate detection stage, NodeRT performs detection on the ACTree, which effectively eliminates most non-racing event handlers and outputs race candidates. In the false positive removal stage, NodeRT utilizes matching rules derived from HB relation rules and features of resources to reduce false positives in the race candidates. In experiments, NodeRT detects all known races and 9 unknown harmful races in real-world applications, whereas NRace only detects 3 of the unknown harmful races, with 64× more time consumption on average. Compared with NRace, NodeRT significantly reduces the overhead, making it practical to be integrated into real-world test processes.

It is an important problem to generate test data from EFSM model in model-based testing, but it is time-wasting to generate test data for the infeasible paths, so determining the feasibility of the paths before generating test data for them is necessary. The feasibility of EFSM transition paths is analyzed by combing slicing with theorem proving. It is divided into two phases. In the first phase, the transitions related to the predicate on each transition in the path are got by backward slicing. And in the second phase, the feasibility of the path is determined by theorem proving to prove whether the post-condition of the transitions related to the predicate implying the predicate or not. Experimental result shows that the feasibility of the paths can be decided effectively and the number of theorem proving is reduced greatly, the infeasibility of the path also can be checked quicker by the proposed method.