A Model-Checking Approach for Fault Analysis Based on Configurable Model Extraction
Summary :
A practical model-checking (MC) approach for fault analysis, that is one of the most cost-effective tasks in software development, is proposed. The proposed approach is based on a technique, named “Program-oriented Modeling” (POM) for extracting a model from source code. The framework of model extraction by POM provides configurable abstraction based on user-defined transformation rules, and it supports trial-and-error model extraction. An environment for MC called POM/MC was also built. POM/MC analyzes C source code to extract Promela models used for the SPIN model checker. It was applied to an industrial software system to evaluate the efficiency of the configurable model extraction by POM for fault analysis. Moreover, it was shown that the proposed MC approach can reduce the effort involved in analyzing software faults by MC.
- Publication
- IEICE TRANSACTIONS on Information Vol.E98-D No.6 pp.1150-1160
- Publication Date
- 2015/06/01
- Publicized
- 2015/02/17
- Online ISSN
- 1745-1361
- DOI
- 10.1587/transinf.2014FOP0012
- Type of Manuscript
- Special Section PAPER (Special Section on Formal Approach)
- Category
- Model Checking
Authors
Hideto OGAWA
Hitachi, Ltd.
Makoto ICHII
Hitachi, Ltd.
Tomoyuki MYOJIN
Hitachi, Ltd.
Masaki CHIKAHISA
Hitachi, Ltd.
Yuichiro NAKAGAWA
Hitachi, Ltd.
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Hideto OGAWA, Makoto ICHII, Tomoyuki MYOJIN, Masaki CHIKAHISA, Yuichiro NAKAGAWA, "A Model-Checking Approach for Fault Analysis Based on Configurable Model Extraction" in IEICE TRANSACTIONS on Information,
vol. E98-D, no. 6, pp. 1150-1160, June 2015, doi: 10.1587/transinf.2014FOP0012.
Abstract: A practical model-checking (MC) approach for fault analysis, that is one of the most cost-effective tasks in software development, is proposed. The proposed approach is based on a technique, named “Program-oriented Modeling” (POM) for extracting a model from source code. The framework of model extraction by POM provides configurable abstraction based on user-defined transformation rules, and it supports trial-and-error model extraction. An environment for MC called POM/MC was also built. POM/MC analyzes C source code to extract Promela models used for the SPIN model checker. It was applied to an industrial software system to evaluate the efficiency of the configurable model extraction by POM for fault analysis. Moreover, it was shown that the proposed MC approach can reduce the effort involved in analyzing software faults by MC.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.2014FOP0012/_p
Copy
@ARTICLE{e98-d_6_1150,
author={Hideto OGAWA, Makoto ICHII, Tomoyuki MYOJIN, Masaki CHIKAHISA, Yuichiro NAKAGAWA, },
journal={IEICE TRANSACTIONS on Information},
title={A Model-Checking Approach for Fault Analysis Based on Configurable Model Extraction},
year={2015},
volume={E98-D},
number={6},
pages={1150-1160},
abstract={A practical model-checking (MC) approach for fault analysis, that is one of the most cost-effective tasks in software development, is proposed. The proposed approach is based on a technique, named “Program-oriented Modeling” (POM) for extracting a model from source code. The framework of model extraction by POM provides configurable abstraction based on user-defined transformation rules, and it supports trial-and-error model extraction. An environment for MC called POM/MC was also built. POM/MC analyzes C source code to extract Promela models used for the SPIN model checker. It was applied to an industrial software system to evaluate the efficiency of the configurable model extraction by POM for fault analysis. Moreover, it was shown that the proposed MC approach can reduce the effort involved in analyzing software faults by MC.},
keywords={},
doi={10.1587/transinf.2014FOP0012},
ISSN={1745-1361},
month={June},}
Copy
TY - JOUR
TI - A Model-Checking Approach for Fault Analysis Based on Configurable Model Extraction
T2 - IEICE TRANSACTIONS on Information
SP - 1150
EP - 1160
AU - Hideto OGAWA
AU - Makoto ICHII
AU - Tomoyuki MYOJIN
AU - Masaki CHIKAHISA
AU - Yuichiro NAKAGAWA
PY - 2015
DO - 10.1587/transinf.2014FOP0012
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E98-D
IS - 6
JA - IEICE TRANSACTIONS on Information
Y1 - June 2015
AB - A practical model-checking (MC) approach for fault analysis, that is one of the most cost-effective tasks in software development, is proposed. The proposed approach is based on a technique, named “Program-oriented Modeling” (POM) for extracting a model from source code. The framework of model extraction by POM provides configurable abstraction based on user-defined transformation rules, and it supports trial-and-error model extraction. An environment for MC called POM/MC was also built. POM/MC analyzes C source code to extract Promela models used for the SPIN model checker. It was applied to an industrial software system to evaluate the efficiency of the configurable model extraction by POM for fault analysis. Moreover, it was shown that the proposed MC approach can reduce the effort involved in analyzing software faults by MC.
ER -
English
