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

Yoshitaka Aoki, Saeko Matsuura

Research output: Contribution to journalArticle

  • 1 Citations

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.

LanguageEnglish
Pages1097-1108
Number of pages12
JournalIEICE Transactions on Information and Systems
VolumeE96-D
Issue number5
DOIs
StatePublished - 2014

Fingerprint

Model checking
Defects
Industry
Specifications
Finite automata
Software engineering
Testing

Keywords

  • Eclipse
  • Model checking
  • UPPAAL

ASJC Scopus subject areas

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

Cite this

Verifying business rules using model-checking techniques for non-specialist in model-checking. / Aoki, Yoshitaka; Matsuura, Saeko.

In: IEICE Transactions on Information and Systems, Vol. E96-D, No. 5, 2014, p. 1097-1108.

Research output: Contribution to journalArticle

@article{56563efc534c414f84e0af2f731f3723,
title = "Verifying business rules using model-checking techniques for non-specialist in model-checking",
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.",
keywords = "Eclipse, Model checking, UPPAAL",
author = "Yoshitaka Aoki and Saeko Matsuura",
year = "2014",
doi = "10.1587/transinf.E97.D.1097",
language = "English",
volume = "E96-D",
pages = "1097--1108",
journal = "IEICE Transactions on Information and Systems",
issn = "0916-8532",
publisher = "Maruzen Co., Ltd/Maruzen Kabushikikaisha",
number = "5",

}

TY - JOUR

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

AU - Aoki,Yoshitaka

AU - Matsuura,Saeko

PY - 2014

Y1 - 2014

N2 - 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.

AB - 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.

KW - Eclipse

KW - Model checking

KW - UPPAAL

UR - http://www.scopus.com/inward/record.url?scp=84900018871&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84900018871&partnerID=8YFLogxK

U2 - 10.1587/transinf.E97.D.1097

DO - 10.1587/transinf.E97.D.1097

M3 - Article

VL - E96-D

SP - 1097

EP - 1108

JO - IEICE Transactions on Information and Systems

T2 - IEICE Transactions on Information and Systems

JF - IEICE Transactions on Information and Systems

SN - 0916-8532

IS - 5

ER -