A method for detecting unusual defects in enterprise system using model checking techniques

Yoshitaka Aoki, Saeko Matsuura

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationRecent Researches in Software Engineering, Parallel and Distributed Systems - 10th WSEAS International Conference on Software Engineering, Parallel and Distributed Systems, SEPADS'11
Pages165-171
Number of pages7
Publication statusPublished - 2011
Event10th WSEAS International Conference on Software Engineering, Parallel and Distributed Systems, SEPADS'11 - Cambridge
Duration: 2011 Feb 202011 Feb 22

Other

Other10th WSEAS International Conference on Software Engineering, Parallel and Distributed Systems, SEPADS'11
CityCambridge
Period11/2/2011/2/22

Fingerprint

Model checking
Defects
Industry

Keywords

  • Abstraction
  • Bugs
  • Enterprise system
  • Infinity loop
  • Model checking
  • UPPAAL

ASJC Scopus subject areas

  • Software

Cite this

Aoki, Y., & Matsuura, S. (2011). A method for detecting unusual defects in enterprise system using model checking techniques. In Recent Researches in Software Engineering, Parallel and Distributed Systems - 10th WSEAS International Conference on Software Engineering, Parallel and Distributed Systems, SEPADS'11 (pp. 165-171)

A method for detecting unusual defects in enterprise system using model checking techniques. / Aoki, Yoshitaka; Matsuura, Saeko.

Recent Researches in Software Engineering, Parallel and Distributed Systems - 10th WSEAS International Conference on Software Engineering, Parallel and Distributed Systems, SEPADS'11. 2011. p. 165-171.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Aoki, Y & Matsuura, S 2011, A method for detecting unusual defects in enterprise system using model checking techniques. in Recent Researches in Software Engineering, Parallel and Distributed Systems - 10th WSEAS International Conference on Software Engineering, Parallel and Distributed Systems, SEPADS'11. pp. 165-171, 10th WSEAS International Conference on Software Engineering, Parallel and Distributed Systems, SEPADS'11, Cambridge, 11/2/20.
Aoki Y, Matsuura S. A method for detecting unusual defects in enterprise system using model checking techniques. In Recent Researches in Software Engineering, Parallel and Distributed Systems - 10th WSEAS International Conference on Software Engineering, Parallel and Distributed Systems, SEPADS'11. 2011. p. 165-171
Aoki, Yoshitaka ; Matsuura, Saeko. / A method for detecting unusual defects in enterprise system using model checking techniques. Recent Researches in Software Engineering, Parallel and Distributed Systems - 10th WSEAS International Conference on Software Engineering, Parallel and Distributed Systems, SEPADS'11. 2011. pp. 165-171
@inproceedings{3ec6ee93b96d4e61850f99d04dd57fc8,
title = "A method for detecting unusual defects in enterprise system using model checking techniques",
abstract = "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.",
keywords = "Abstraction, Bugs, Enterprise system, Infinity loop, Model checking, UPPAAL",
author = "Yoshitaka Aoki and Saeko Matsuura",
year = "2011",
language = "English",
isbn = "9789604742776",
pages = "165--171",
booktitle = "Recent Researches in Software Engineering, Parallel and Distributed Systems - 10th WSEAS International Conference on Software Engineering, Parallel and Distributed Systems, SEPADS'11",

}

TY - GEN

T1 - A method for detecting unusual defects in enterprise system using model checking techniques

AU - Aoki, Yoshitaka

AU - Matsuura, Saeko

PY - 2011

Y1 - 2011

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

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

KW - Abstraction

KW - Bugs

KW - Enterprise system

KW - Infinity loop

KW - Model checking

KW - UPPAAL

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

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

M3 - Conference contribution

AN - SCOPUS:79958727577

SN - 9789604742776

SP - 165

EP - 171

BT - Recent Researches in Software Engineering, Parallel and Distributed Systems - 10th WSEAS International Conference on Software Engineering, Parallel and Distributed Systems, SEPADS'11

ER -