A methodology to support UML-B model development

UML-B is a graphical front-end for the formal method Event-B. UML-B models are translated to Event-B for verification purpose. Modelling and proving become difficult for complex models with many state variables and transitions. Reducing modelling and proving effort is potential for UML-B models....

Full description

Saved in:
Bibliographic Details
Main Author: Jasser, Muhammed Basheer
Format: Thesis
Language:English
Published: 2018
Subjects:
Online Access:http://psasir.upm.edu.my/id/eprint/68808/1/FSKTM%202018%2019%20IR.pdf
Tags: Add Tag
No Tags, Be the first to tag this record!
id my-upm-ir.68808
record_format uketd_dc
institution Universiti Putra Malaysia
collection PSAS Institutional Repository
language English
topic UML (Computer science)
Decomposition method

spellingShingle UML (Computer science)
Decomposition method

Jasser, Muhammed Basheer
A methodology to support UML-B model development
description UML-B is a graphical front-end for the formal method Event-B. UML-B models are translated to Event-B for verification purpose. Modelling and proving become difficult for complex models with many state variables and transitions. Reducing modelling and proving effort is potential for UML-B models. Decomposition, composition, model matching, and pattern reuse are attracting methods to support individual team modelling, comparing, integrating, and reusing models helping UML-B modellers and practitioners to avoid remodelling and reduce the proof effort required to verify the correctness of the models. Decomposition in Event-B divides a complex model into sub-parts reducing certainly its complexity and facilitating independent modelling for the sub-parts. Two decomposition styles exist for Event-B which are shared-event and sharedvariable. The shared-event style has been introduced in UML-B and it is considered suitable for synchronous message passing systems. However, the sharedvariable style is not supported before in UML-B. In this research, a correctby- construction method is introduced to support the shared-variable decomposition in UML-B that is considered suitable for asynchronous shared variable models. The proposed method is provided through three sequential phases which are refinement-preparation, actual-decomposition, and refinement-afterdecomposition. The provision of new notions, conditions, and rules is a significant step to maintain the graphical semantics of UML-B and the shared variable formalism of Event-B. We introduce refinement-preparation strategies and conditions, actual-decomposition rules, refinement-after-decomposition conditions, new UML-B notions, and a representation mechanism. The method is formalised and verified via a generic proof on a theoretical level to show how the generated semantic implicit invariants and the shared variable formalism are preserved, and to prove that any recomposed machine is indeed correct and a refinement of the original decomposable machine when the method phases conditions and rules are followed. The method is illustrated by a case study on the updating of master data, in which the notions, conditions, and rules are applied. Event-B composition is to reuse existing interacting models specifications to construct a larger one fulfilling the complete system behaviour. In this research, a correct-by-construction method is introduced to compose UML-B machines that interact via the shared-variable style. This saves the modelling and proving effort via the correct machines that are being composed. The method is provided through steps and rules, and its correctness is verified by proving that any composed machine is indeed correct when the method rules are followed. The method applicability is also illustrated by the case study on the updating of master data. Identifying similarities between models has several benefits such as model comparison, integration, and evolution. Several matching and comparison methods have been done in the context of model driven software engineering. However, matching models via a systematic method is not supported yet in UML-B. In this work, we propose a matching method for UML-B elements based on their semantics. This method includes variable-based, event-based, and state-machine matching. The variable-based matching provides rules for matching UML-B classes, attributes, states, and variables. The event-based matching provides rules and cases for matching UML-B transitions and class-events. The statemachine matching provides rules for matching UML-B state-machines based on the state and transition matching rules. The matching rules are formalized by means of the generated corresponding Event-B specifications. The correctness of the rules is justified via preserving the compatibility of the matched statevariables and corresponding modifying events including their matched guards and actions. These rules are illustrated via a communication-based case study to show their applicability. Pattern reuse allows reusing models in constructing new ones saving the modelling and proving effort. However, there is no systematic method in terms of pattern reuse in UML-B. In this research, a correct-by-construction method is introduced to support the reuse of UML-B models which is based on the Event-B pattern reuse. The method is provided through three sequential phases which are pattern matching, checking, and incorporation. The provision of new guidelines and rules is necessary to preserve both the UML-B graphical semantics and the method correctness. This is proven via a generic proof using the proofs from the pattern that is integrated with the problem model. The proposed method reduces certainly the modelling and proving effort by using existing models in constructing new ones, since it is always that the proof obligations from the pattern model do not need to be proven again during the integration between the pattern and problem models. The method applicability is illustrated by the communication-based case study introduced in the model matching.
format Thesis
qualification_level Doctorate
author Jasser, Muhammed Basheer
author_facet Jasser, Muhammed Basheer
author_sort Jasser, Muhammed Basheer
title A methodology to support UML-B model development
title_short A methodology to support UML-B model development
title_full A methodology to support UML-B model development
title_fullStr A methodology to support UML-B model development
title_full_unstemmed A methodology to support UML-B model development
title_sort methodology to support uml-b model development
granting_institution Universiti Putra Malaysia
publishDate 2018
url http://psasir.upm.edu.my/id/eprint/68808/1/FSKTM%202018%2019%20IR.pdf
_version_ 1747812636364374016
spelling my-upm-ir.688082019-06-18T03:03:56Z A methodology to support UML-B model development 2018-01 Jasser, Muhammed Basheer UML-B is a graphical front-end for the formal method Event-B. UML-B models are translated to Event-B for verification purpose. Modelling and proving become difficult for complex models with many state variables and transitions. Reducing modelling and proving effort is potential for UML-B models. Decomposition, composition, model matching, and pattern reuse are attracting methods to support individual team modelling, comparing, integrating, and reusing models helping UML-B modellers and practitioners to avoid remodelling and reduce the proof effort required to verify the correctness of the models. Decomposition in Event-B divides a complex model into sub-parts reducing certainly its complexity and facilitating independent modelling for the sub-parts. Two decomposition styles exist for Event-B which are shared-event and sharedvariable. The shared-event style has been introduced in UML-B and it is considered suitable for synchronous message passing systems. However, the sharedvariable style is not supported before in UML-B. In this research, a correctby- construction method is introduced to support the shared-variable decomposition in UML-B that is considered suitable for asynchronous shared variable models. The proposed method is provided through three sequential phases which are refinement-preparation, actual-decomposition, and refinement-afterdecomposition. The provision of new notions, conditions, and rules is a significant step to maintain the graphical semantics of UML-B and the shared variable formalism of Event-B. We introduce refinement-preparation strategies and conditions, actual-decomposition rules, refinement-after-decomposition conditions, new UML-B notions, and a representation mechanism. The method is formalised and verified via a generic proof on a theoretical level to show how the generated semantic implicit invariants and the shared variable formalism are preserved, and to prove that any recomposed machine is indeed correct and a refinement of the original decomposable machine when the method phases conditions and rules are followed. The method is illustrated by a case study on the updating of master data, in which the notions, conditions, and rules are applied. Event-B composition is to reuse existing interacting models specifications to construct a larger one fulfilling the complete system behaviour. In this research, a correct-by-construction method is introduced to compose UML-B machines that interact via the shared-variable style. This saves the modelling and proving effort via the correct machines that are being composed. The method is provided through steps and rules, and its correctness is verified by proving that any composed machine is indeed correct when the method rules are followed. The method applicability is also illustrated by the case study on the updating of master data. Identifying similarities between models has several benefits such as model comparison, integration, and evolution. Several matching and comparison methods have been done in the context of model driven software engineering. However, matching models via a systematic method is not supported yet in UML-B. In this work, we propose a matching method for UML-B elements based on their semantics. This method includes variable-based, event-based, and state-machine matching. The variable-based matching provides rules for matching UML-B classes, attributes, states, and variables. The event-based matching provides rules and cases for matching UML-B transitions and class-events. The statemachine matching provides rules for matching UML-B state-machines based on the state and transition matching rules. The matching rules are formalized by means of the generated corresponding Event-B specifications. The correctness of the rules is justified via preserving the compatibility of the matched statevariables and corresponding modifying events including their matched guards and actions. These rules are illustrated via a communication-based case study to show their applicability. Pattern reuse allows reusing models in constructing new ones saving the modelling and proving effort. However, there is no systematic method in terms of pattern reuse in UML-B. In this research, a correct-by-construction method is introduced to support the reuse of UML-B models which is based on the Event-B pattern reuse. The method is provided through three sequential phases which are pattern matching, checking, and incorporation. The provision of new guidelines and rules is necessary to preserve both the UML-B graphical semantics and the method correctness. This is proven via a generic proof using the proofs from the pattern that is integrated with the problem model. The proposed method reduces certainly the modelling and proving effort by using existing models in constructing new ones, since it is always that the proof obligations from the pattern model do not need to be proven again during the integration between the pattern and problem models. The method applicability is illustrated by the communication-based case study introduced in the model matching. UML (Computer science) Decomposition method 2018-01 Thesis http://psasir.upm.edu.my/id/eprint/68808/ http://psasir.upm.edu.my/id/eprint/68808/1/FSKTM%202018%2019%20IR.pdf text en public doctoral Universiti Putra Malaysia UML (Computer science) Decomposition method