A Model-Checking Approach for Fault Analysis Based on Configurable Model Extraction

被引：0

作者：

Ogawa, Hideto ^{[1
]}

Ichii, Makoto ^{[1
]}

Myojin, Tomoyuki ^{[1
]}

Chikahisa, Masaki ^{[1
]}

Nakagawa, Yuichiro ^{[1
]}

机构：

[1] Hitachi Ltd, Res & Dev Grp, Ctr Technol Innovat Syst Engn, Yokohama, Kanagawa 2440817, Japan

来源：

IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS | 2015年 / E98D卷 / 06期

关键词：

model checking; fault analysis; model transformation;

D O I：

10.1587/transinf.2014FOP0012

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

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.

引用

页码：1150 / 1160

页数：11

共 50 条

[1] ANTICHAINS FOR THE AUTOMATA-BASED APPROACH TO MODEL-CHECKING
Doyen, Laurent
Raskin, Jean-Francois
LOGICAL METHODS IN COMPUTER SCIENCE, 2009, 5 (01)
[2] Model-checking for validation of a Fault Protection system
Feather, MS
Fickas, S
Razermera-Mamy, NA
SIXTH IEEE INTERNATIONAL SYMPOSIUM ON HIGH ASSURANCE SYSTEMS ENGINEERING, 2001, : 32 - 41
[3] Combining real-time model-checking and fault tree analysis
Schäfer, A
FME 2003: FORMAL METHODS, PROCEEDINGS, 2003, 2805 : 522 - 541
[4] Improved algorithms for the automata-based approach to model-checking
Doyen, Laurent
Raskin, Jean-Francois
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2007, 4424 : 451 - +
[5] Model-checking based data retrieval
Dovier, A
Quintarelli, E
DATABASE PROGRAMMING LANGUAGES, 2002, 2397 : 62 - 77
[6] The model-checking kit
Schröter, C
Schwoon, S
Esparza, J
APPLICATIONS AND THEORY OF PETRI NETS 2003, PROCEEDINGS, 2003, 2679 : 463 - 472
[7] A Model-Checking Approach for Service Component Architectures
Abreu, Joao
Mazzanti, Franco
Fiadeiro, Jose Luiz
Gnesi, Stefania
FORMAL TECHNIQUES FOR DISTRIBUTED SYSTEMS, PROCEEDINGS, 2009, 5522 : 219 - +
[8] QLTL Model-Checking
Laroussinie, Francois
Leclercq, Loriane
Sangnier, Arnaud
32ND EACSL ANNUAL CONFERENCE ON COMPUTER SCIENCE LOGIC, CSL 2024, 2024, 288
[9] SAT-based model-checking for security protocols analysis
Alessandro Armando
Luca Compagna
International Journal of Information Security, 2008, 7 : 3 - 32
[10] A state/event-based model-checking approach for the analysis of abstract system properties
ter Beek, Maurice H.
Fantechi, Alessandro
Gnesi, Stefania
Mazzanti, Franco
SCIENCE OF COMPUTER PROGRAMMING, 2011, 76 (02) : 119 - 135

← 1 2 3 4 5 →