Abstract We consider the problem of statically detecting data races in periodic real-time programs that use locks, and run on a single processor platform. We propose a technique based on a small set of rules that exploits the priority, periodicity, locking, and timing information of tasks in the program. One of the key requirements is a response time analysis for such programs, and we propose an algorithm to compute this for the case of non-nested locks. We have implemented our analysis for real-time programs written in C in a tool called PePRacer and evaluated its performance on a small set of benchmarks from the literature.

Symbolic execution is an important program analysistechnique that has found a number of applications in the last fifteen years or so.Popular symbolic execution approaches use backtracking when faced with infeasibility along a path being explored.A simple backtracking strategy (i.e.backtracking by a single decision node) may suffice when the goal is to cover the entire control flow graph (CFG).However, if the goal is to cover specific parts of the CFG through a single path, simple backtracking may lead to non-optimality or even non-termination.In this paper, we present weighted backtracking strategy (WBS) that exploits previous knowledge about the program behaviour to compute 'good' candidates as destinations of backtracking.We have integrated our heuristic to SymTest, a symbolic testing framework for embedded systems.Experiments with casestudies have demonstrated that WBS improves SymTest's performance both in its ability to achieve termination as well as in computing shorter test sequences compared to the original approach.SymTest with WBS generates shorter test sequences compared to several other existing test generation approaches based on symbolic execution.

Automated testing tools for programs written in IEC 61131-3 standard of programming languages supporting the development of PLC control software is less available. Symbolic execution is a program analysis technique that determines what inputs cause each part of a program to execute. Here, a symbolic execution framework is utilized to achieve test target coverage for control system software. The framework does not ensure optimal feasible paths after backtracking. In this paper an approach using weight calculation is utilized to overcome the drawback. The calculated weight values helps to backtrack to a node, on flipping will result in an optimal feasible path.