A Method for Detecting Unusual Defects in Enterprise System Using Model Checking Techniques

摘要

This paper proposes a method based on model checking for detecting hard-to-discover defects in enterprise systems. Source codes are transformed into an appropriate phased abstract model so that we can observe the phenomena. UPPAAL, which is a typical model checking tool, makes an exhaustive checking of the model and provides a result whether the model can reach the specified state or not. We have developed a supporting tool to narrow the range of model checking and to generate UPPAAL model automatically. We discuss our method in detail on the basis of the results of a case study.