The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. ex. Some numerals are expressed as "XNUMX".
Copyrights notice
The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. Copyrights notice
Spesifikasi formal berasaskan penghalusan ialah pendekatan yang menjanjikan kepada peningkatan kerumitan sistem perisian, seperti yang ditunjukkan dalam kaedah formal Event-B. Ia membenarkan pemodelan langkah demi langkah dan pengesahan sistem kompleks dengan pelbagai langkah pada tahap abstraksi yang berbeza. Walau bagaimanapun, membuat perubahan adalah lebih sukar, kerana berhati-hati adalah perlu untuk mengelakkan melanggar konsistensi antara langkah. Menilai sama ada perubahan itu sah atau tidak adalah tugas yang tidak remeh, kerana hubungan pergantungan logik antara elemen pemodelan (predikat) adalah tersirat dan kompleks. Dalam makalah ini, kami mencadangkan kaedah untuk menganalisis kesan perubahan Peristiwa-B. Dengan melampirkan label pada elemen pemodelan (predikat), kaedah ini membantu jurutera memahami cara model distrukturkan dan perkara yang perlu diubah suai untuk mencapai perubahan.
Shinnosuke SARUWATARI
University of Tokyo
Fuyuki ISHIKAWA
National Institute of Informatics
Tsutomu KOBAYASHI
National Institute of Informatics
Shinichi HONIDEN
Waseda University
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.
Salinan
Shinnosuke SARUWATARI, Fuyuki ISHIKAWA, Tsutomu KOBAYASHI, Shinichi HONIDEN, "Change Impact Analysis for Refinement-Based Formal Specification" in IEICE TRANSACTIONS on Information,
vol. E102-D, no. 8, pp. 1462-1477, August 2019, doi: 10.1587/transinf.2018FOP0006.
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.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.2018FOP0006/_p
Salinan
@ARTICLE{e102-d_8_1462,
author={Shinnosuke SARUWATARI, Fuyuki ISHIKAWA, Tsutomu KOBAYASHI, Shinichi HONIDEN, },
journal={IEICE TRANSACTIONS on Information},
title={Change Impact Analysis for Refinement-Based Formal Specification},
year={2019},
volume={E102-D},
number={8},
pages={1462-1477},
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={},
doi={10.1587/transinf.2018FOP0006},
ISSN={1745-1361},
month={August},}
Salinan
TY - JOUR
TI - Change Impact Analysis for Refinement-Based Formal Specification
T2 - IEICE TRANSACTIONS on Information
SP - 1462
EP - 1477
AU - Shinnosuke SARUWATARI
AU - Fuyuki ISHIKAWA
AU - Tsutomu KOBAYASHI
AU - Shinichi HONIDEN
PY - 2019
DO - 10.1587/transinf.2018FOP0006
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E102-D
IS - 8
JA - IEICE TRANSACTIONS on Information
Y1 - August 2019
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.
ER -