Change impact analysis for refinement-based formal specification

Shinnosuke Saruwatari, Fuyuki Ishikawa, Tsutomu Kobayashi, Shinichi Honiden

Research output: Contribution to journalArticle

Abstract

Refinement-based formal specification is a promising approach to the increasing complexity of software systems, as demonstrated in the formal method Event-B. It allows stepwise modeling and verifying of complex systems with multiple steps at different abstraction levels. However, making changes is more difficult, as caution is necessary to avoid breaking the consistency between the steps. Judging whether a change is valid or not is a non-trivial task, as the logical dependency relationships between the modeling elements (predicates) are implicit and complex. In this paper, we propose a method for analyzing the impact of the changes of Event-B. By attaching labels to modeling elements (predicates), the method helps engineers understand how a model is structured and what needs to be modified to accomplish a change.

Original languageEnglish
Pages (from-to)1462-1477
Number of pages16
JournalIEICE Transactions on Information and Systems
VolumeE102D
Issue number8
DOIs
Publication statusPublished - 2019 Jan 1

Fingerprint

Formal methods
Large scale systems
Labels
Engineers
Formal specification

Keywords

  • Event-B
  • Formal method
  • Formal specification
  • Impact analysis
  • Modification support
  • Refinement

ASJC Scopus subject areas

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

Cite this

Change impact analysis for refinement-based formal specification. / Saruwatari, Shinnosuke; Ishikawa, Fuyuki; Kobayashi, Tsutomu; Honiden, Shinichi.

In: IEICE Transactions on Information and Systems, Vol. E102D, No. 8, 01.01.2019, p. 1462-1477.

Research output: Contribution to journalArticle

Saruwatari, Shinnosuke ; Ishikawa, Fuyuki ; Kobayashi, Tsutomu ; Honiden, Shinichi. / Change impact analysis for refinement-based formal specification. In: IEICE Transactions on Information and Systems. 2019 ; Vol. E102D, No. 8. pp. 1462-1477.
@article{a260bc060fdd4f9082e43a72cd1f838d,
title = "Change impact analysis for refinement-based formal specification",
abstract = "Refinement-based formal specification is a promising approach to the increasing complexity of software systems, as demonstrated in the formal method Event-B. It allows stepwise modeling and verifying of complex systems with multiple steps at different abstraction levels. However, making changes is more difficult, as caution is necessary to avoid breaking the consistency between the steps. Judging whether a change is valid or not is a non-trivial task, as the logical dependency relationships between the modeling elements (predicates) are implicit and complex. In this paper, we propose a method for analyzing the impact of the changes of Event-B. By attaching labels to modeling elements (predicates), the method helps engineers understand how a model is structured and what needs to be modified to accomplish a change.",
keywords = "Event-B, Formal method, Formal specification, Impact analysis, Modification support, Refinement",
author = "Shinnosuke Saruwatari and Fuyuki Ishikawa and Tsutomu Kobayashi and Shinichi Honiden",
year = "2019",
month = "1",
day = "1",
doi = "10.1587/transinf.2018FOP0006",
language = "English",
volume = "E102D",
pages = "1462--1477",
journal = "IEICE Transactions on Information and Systems",
issn = "0916-8532",
publisher = "Maruzen Co., Ltd/Maruzen Kabushikikaisha",
number = "8",

}

TY - JOUR

T1 - Change impact analysis for refinement-based formal specification

AU - Saruwatari, Shinnosuke

AU - Ishikawa, Fuyuki

AU - Kobayashi, Tsutomu

AU - Honiden, Shinichi

PY - 2019/1/1

Y1 - 2019/1/1

N2 - Refinement-based formal specification is a promising approach to the increasing complexity of software systems, as demonstrated in the formal method Event-B. It allows stepwise modeling and verifying of complex systems with multiple steps at different abstraction levels. However, making changes is more difficult, as caution is necessary to avoid breaking the consistency between the steps. Judging whether a change is valid or not is a non-trivial task, as the logical dependency relationships between the modeling elements (predicates) are implicit and complex. In this paper, we propose a method for analyzing the impact of the changes of Event-B. By attaching labels to modeling elements (predicates), the method helps engineers understand how a model is structured and what needs to be modified to accomplish a change.

AB - Refinement-based formal specification is a promising approach to the increasing complexity of software systems, as demonstrated in the formal method Event-B. It allows stepwise modeling and verifying of complex systems with multiple steps at different abstraction levels. However, making changes is more difficult, as caution is necessary to avoid breaking the consistency between the steps. Judging whether a change is valid or not is a non-trivial task, as the logical dependency relationships between the modeling elements (predicates) are implicit and complex. In this paper, we propose a method for analyzing the impact of the changes of Event-B. By attaching labels to modeling elements (predicates), the method helps engineers understand how a model is structured and what needs to be modified to accomplish a change.

KW - Event-B

KW - Formal method

KW - Formal specification

KW - Impact analysis

KW - Modification support

KW - Refinement

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

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

U2 - 10.1587/transinf.2018FOP0006

DO - 10.1587/transinf.2018FOP0006

M3 - Article

AN - SCOPUS:85071983395

VL - E102D

SP - 1462

EP - 1477

JO - IEICE Transactions on Information and Systems

JF - IEICE Transactions on Information and Systems

SN - 0916-8532

IS - 8

ER -