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 Jun 17
Event10th WSEAS International Conference on Software Engineering, Parallel and Distributed Systems, SEPADS'11 - Cambridge, United Kingdom
Duration: 2011 Feb 202011 Feb 22

Publication series

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

Conference

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

Keywords

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

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'A method for detecting unusual defects in enterprise system using model checking techniques'. Together they form a unique fingerprint.

Cite this