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

Yoshitaka Aoki, Saeko Matsuura

Research output: Contribution to journalArticlepeer-review

2 Citations (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.

Original languageEnglish
Pages (from-to)1097-1108
Number of pages12
JournalIEICE Transactions on Information and Systems
Issue number5
Publication statusPublished - 2014 May


  • Eclipse
  • Model checking

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture
  • Computer Vision and Pattern Recognition
  • Electrical and Electronic Engineering
  • Artificial Intelligence


Dive into the research topics of 'Verifying business rules using model-checking techniques for non-specialist in model-checking'. Together they form a unique fingerprint.

Cite this