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. 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.

Preview Text FSKTM 2018 19 IR.pdf Download (1MB) | Preview

Actions (login required)

View Item