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

Yoshitaka Aoki, Saeko Matsuura

Research output: Contribution to journalArticle

2 Citations (Scopus)

Abstract

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
VolumeE96-D
Issue number5
DOIs
Publication statusPublished - 2014 May

    Fingerprint

Keywords

  • Eclipse
  • Model checking
  • UPPAAL

ASJC Scopus subject areas

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

Cite this