Safety critical systems are often modeled using Time Petri Nets (TPN) for analyzing their reliability with formal verification methods. This paper proposed an efficient verification method for TPN introducing bounded model checking based on satisfiability solving. The proposed method expresses time constraints of TPN by Difference Logic (DL) and uses SMT solvers for verification. Its effectiveness was also demonstrated with an experiment.

This paper focuses on the “data collection period” for training a better Just-In-Time (JIT) defect prediction model — the early commit data vs. the recent one —, and conducts a large-scale comparative study to explore an appropriate data collection period. Since there are many possible machine learning algorithms for training defect prediction models, the selection of machine learning algorithms can become a threat to validity. Hence, this study adopts the automatic machine learning method to mitigate the selection bias in the comparative study. The empirical results using 122 open-source software projects prove the trend that the dataset composed of the recent commits would become a better training set for JIT defect prediction models.

Recently, software development projects have been required to produce highly reliable systems within a short period and with low cost. In such situation, software quality prediction helps to confirm that the software product satisfies required quality expectations. In this paper, by using a Bayesian Belief Network (BBN), we try to construct a prediction model based on relationships elicited from the embedded software development process. On the one hand, according to a characteristic of embedded software development, we especially propose to classify test and debug activities into two distinct activities on software and hardware. Then we call the proposed model "the BBN for an embedded software development process". On the other hand, we define "the BBN for a general software development process" to be a model which does not consider this classification of activity, but rather, merges them into a single activity. Finally, we conducted experimental evaluations by applying these two BBNs to actual project data. As the results of our experiments show, the BBN for the embedded software development process is superior to the BBN for the general development process and is applicable effectively for effective practical use.

This paper focuses on the power of comments to predict fault-prone programs. In general, comments along with executable statements enhance the understandability of programs. However, comments may also be used to mask the lack of readability in the program, therefore well-written comments are referred to as “deodorant to mask code smells” in the field of code refactoring. This paper conducts an empirical analysis to examine whether Lines of Comments (LCM) written inside a method's body is a noteworthy metric for analyzing fault-proneness in Java methods. The empirical results show the following two findings: (1) more-commented methods (the methods having more comments than the amount estimated by size and complexity of the methods) are about 1.6 - 2.8 times more likely to be faulty than the others, and (2) LCM can be a useful factor in fault-prone method prediction models along with the method size and the method complexity.

During a software development phase where a product is progressively elaborated, it is difficult to guarantee that the refined product retains its original behaviors. In this paper, we propose a method to detect refinement errors in UML sequence diagrams using LTSA (Labeled Transition System Analyzer). The method integrates multiple sequence diagrams using hMSC (high-level Message Sequence Charts) into a sequence diagram. Then, the method translates the diagram into FSP representation, which is the input language of LTSA. The method also supports some combined fragment operators in the UML 2.0 specification. We applied the method to some examples of refined sequence diagrams and checked the correctness of refinement. As a result, we confirmed the method can detect refinement errors in practical time.