In automotive control systems, the potential risks of software defects have been increasing due to growing software complexity driven by advances in electric-electronic control. Some kind of defects such as race conditions can rarely be detected by testing or simulations because these defects manifest themselves only in some rare executions. Model checking, which employs an exhaustive state-space exploration, is effective for detecting such defects. This paper reports our approach to applying model checking techniques to real-world automotive control programs. It is impossible to directly model check such programs because of their large size and high complexity; thus, it is necessary to derive, from the program under verification, a model that is amenable to model checking. Our approach uses the SPIN model checker as well as in-house tools that facilitate this process. One of the key features implemented in these tools is boundary-adjustable program slicing, which allows the user to specify and extract part of the source code that is relevant to the verification problem of interest. The conversion from extracted code into Promela, SPIN's input language, is performed using one of the tools in a semi-automatic manner. This approach has been used for several years in practice and found to be useful even when the code size of the software exceeds 400 KLOC.

Change-aware development environments can automatically record fine-grained code changes on a program and allow programmers to replay the recorded changes in chronological order. However, since they do not always need to replay all the code changes to investigate how a particular entity of the program has been changed, they often eliminate several code changes of no interest by manually skipping them in replaying. This skipping action is an obstacle that makes many programmers hesitate when they use existing replaying tools. This paper proposes a slicing mechanism that automatically removes manually skipped code changes from the whole history of past code changes and extracts only those necessary to build a particular class member of a Java program. In this mechanism, fine-grained code changes are represented by edit operations recorded on the source code of a program and dependencies among edit operations are formalized. The paper also presents a running tool that slices the operation history and replays its resulting slices. With this tool, programmers can avoid replaying nonessential edit operations for the construction of class members that they want to understand. Experimental results show that the tool offered improvements over conventional replaying tools with respect to the reduction of the number of edit operations needed to be examined and over history filtering tools with respect to the accuracy of edit operations to be replayed.

To understand the behavior of a program, developers often need to read source code fragments in various modules. System-dependence-graph-based (SDG) program slicing is a good candidate for supporting the investigation of data-flow paths among modules, as SDG is capable of showing the data-dependence of focused program elements. However, this technique has two problems. First, constructing SDG requires heavyweight analysis, so SDG is not suitable for daily uses. Second, the results of SDG-based program slicing are difficult to visualize, as they contain many vertices. In this research, we proposed variable data-flow graphs (VDFG) for use in program slicing techniques. In contrast to SDG, VDFG is created by lightweight analysis because several approximations are used. Furthermore, we propose using the fractal value to visualize VDFG-based program slice in order to reduce the graph complexity for visualization purposes. We performed three experiments that demonstrate the accuracy of VDFG program slicing with fractal value, the size of a visualized program slice, and effectiveness of our tool for source code reading.

Fault localization is essential for conducting effective program repair. However, preliminary studies have shown that existing fault localization approaches do not take the requirements of automatic repair into account, and therefore restrict the repair performance. To address this issue, this paper presents the first study on designing fault localization approaches for automatic program repair, that is, we propose a fault localization approach using failure-related contexts in order to improve automatic program repair. The proposed approach first utilizes program slicing technique to construct a failure-related context, then evaluates the suspiciousness of each element in this context, and finally transfers the result of evaluation to automatic program repair techniques for performing repair on faulty programs. The experimental results demonstrate that the proposed approach is effective to improve automatic repair performance.

Program slicing is an important approach for debugging, program comprehension, impact analysis, etc. There are various program slicing techniques ranging from the lightweight to the more accurate but heavyweight. Comparative analyses are important for selecting the most appropriate technique. This paper presents a comparative study of four backward program slicing techniques for Java. The results show the scalability and precision of these techniques. We develop guidelines that indicate which slicing techniques are appropriate for different situations, based on the results.

Program comprehension using dynamic information is one of key tasks of software maintenance. Software visualization with sequence diagrams is a promising technique to help developer comprehend the behavior of object-oriented systems effectively. There are many tools that can support automatic generation of a sequence diagram from execution traces. However it is still difficult to understand the behavior because the size of automatically generated sequence diagrams from the massive amounts of execution traces tends to be beyond developer's capacity. In this paper, we propose an execution trace slicing and visualization method. Our proposed method is capable of slice calculation based on a behavior model which can treat dependencies based on static and dynamic analysis and supports for various programs including exceptions and multi-threading. We also introduce our tool that perform our proposed slice calculation on the Eclipse platform. We show the applicability of our proposed method by applying the tool to two Java programs as case studies. As a result, we confirm effectiveness of our proposed method for understanding the behavior of object-oriented systems.

In this paper, an efficient equivalence checking method for two C descriptions is described. The equivalence of two C descriptions is proved by symbolic simulation. Symbolic simulation used in this paper can prove the equivalence of all of the variables in the descriptions. However, it takes long time to verify the equivalence of all of the variables if large descriptions are given. Therefore, in order to improve the verification, our method identifies textual differences between descriptions. The identified textual differences are used to reduce the number of equivalence checkings among variables. The proposed method has been implemented in C language and evaluated with several C descriptions.

We propose a new inferring programmers' intention system COSMO based on a classification of assignment statements. COSMO is a subsystem of our intelligent programming environment for programming education. The programming environment consists of a program understanding system designed for novice programmers and a novice program evaluation support system designed for teachers, both of which use the technique of the program slicing. Usually, the method of program slicing requires selection of slicing criteria. However, automatic selection of effective slicing criteria is difficult. Here we propose a new inferring programmers' intention system COSMO with automatic selection of effective slicing criteria. In our system, the slicing criteria are inferred using the context structure model of programs. Programs are regarded as natural language texts in the model and analyzed using a similar thinking in context structure analyses of natural language texts. The model is based on a classification of assignment statements using dependence analysis of programs. Furthermore, COSMO obtains networks with information on top-down decomposition of problems as a result of inferring programmers' intention. Therefore, COSMO is useful for understanding programs without presupposed knowledge.

Providing various assistances for design modifications on HDL source codes is important for design reuse and quick design cycle in VLSI CAD. Program slicing is a software-engineering technique for analyzing, abstracting, and transforming programs. We show algorithms for extracting/removing behaviors of specified signals in VHDL descriptions. We also describe a VHDL slicing system and show experimental results of efficiently extracting components from VHDL descriptions.

A program slice is a set of program statements that directly or indirectly contribute to the values assumed by a set of variables at some program execution point. A few slicing algorithms have proposed to far but none of them are considered from the viewpoint of program modification. In this paper, we define a variable dependence graph (VDG) and show a new slicing algorithm on VDG. We also compare the time complexity of the algorithm with that of other existing algorithms and discuss the suitableness of our algorithm for program modification. As the result of this, we argue our algorithm is suitable for embedding debugging systems.