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....
Saved in:
| Main Author: | |
|---|---|
| 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!
|
| Summary: | 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. |
|---|