Verifying business rules using model-checking techniques for non-specialist in model-checking

Yoshitaka Aoki, Saeko Matsuura

研究成果: Article査読

2 被引用数 (Scopus)


Software programs often include many defects that are not easy to detect because of the developers' mistakes, misunderstandings caused by the inadequate definition of requirements, and the complexity of the implementation. Due to the different skill levels of the testers, the significant increase in testing person-hours interferes with the progress of development projects. Therefore, it is desireable for any inexperienced developer to identify the cause of the defects. Model checking has been favored as a technique to improve the reliability earlier in the software development process. In this paper, we propose a verification method in which a Java source code control sequence is converted into finite automata in order to detect the cause of defects by using the model-checking tool UPPAAL, which has an exhaustive checking mechanism. We also propose a tool implemented by an Eclipse plug-in to assist general developers who have little knowledge of the model-checking tool. Because source code is generally complicated and large, the tool provides a step-wise verification mechanism based on the functional structure of the code and makes it easy to verify the business rules in the specification documents by adding a user-defined specification-based model to the source code model.

ジャーナルIEICE Transactions on Information and Systems
出版ステータスPublished - 2014 5月

ASJC Scopus subject areas

  • ソフトウェア
  • ハードウェアとアーキテクチャ
  • コンピュータ ビジョンおよびパターン認識
  • 電子工学および電気工学
  • 人工知能


「Verifying business rules using model-checking techniques for non-specialist in model-checking」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。