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
A especificação formal baseada em refinamento é uma abordagem promissora para a crescente complexidade dos sistemas de software, conforme demonstrado no método formal Event-B. Ele permite modelagem e verificação passo a passo de sistemas complexos com múltiplas etapas em diferentes níveis de abstração. Porém, fazer alterações é mais difícil, pois é necessário cautela para não quebrar a consistência entre as etapas. Julgar se uma mudança é válida ou não não é uma tarefa trivial, pois as relações lógicas de dependência entre os elementos de modelagem (predicados) são implícitas e complexas. Neste artigo, propomos um método para analisar o impacto das mudanças do Evento-B. Ao anexar rótulos aos elementos de modelagem (predicados), o método ajuda os engenheiros a entender como um modelo está estruturado e o que precisa ser modificado para realizar uma mudança.
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.
Copiar
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
Copiar
@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},}
Copiar
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 -