From Sequence Diagrams to Event B: A Specification and Verification Approach of Flexible Workflow Applications of Cloud Services Based on Meta-model Transformation

This paper presents a meta-model transformation based approach to reasoning about sequence diagrams using B event. We present an approach for the specification and the verification of flexible Workflow applications of cloud services. Our approach is based on the semiformal notation of UML sequence d...

Full description

Saved in:
Bibliographic Details
Main Authors: Hlaoui, Yousra Bendaly, Younes, Ahlem Ben, Ben Ayed, Leila Jemni, Fathalli, Manel
Format: Conference Proceeding
Language:English
Subjects:
Cloud computing
Cognition
Elasticity
Event B
KerMeta
Mapping
Meta-model Transformation
Servers
Specification
UML Sequence Diagrams
Unified modeling language
Verification
Workflows
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This paper presents a meta-model transformation based approach to reasoning about sequence diagrams using B event. We present an approach for the specification and the verification of flexible Workflow applications of cloud services. Our approach is based on the semiformal notation of UML sequence diagrams, and the formal method B event. We have developed a tool called SD2EventB supporting the proposed approach. This tool allows the specification of flexible Cloud service Workflow application models using predefined flexibility patterns generated automatically by this tool. Once the model is specified, it is transformed to an event B model to be verified. In order to ensure this verification, we have used the platform Rodin supporting the event B method. This platform has been integrated into our tool. The transformation, as well, has been developed as a function of our tool using the meta-model transformation environment KerMeta.
ISSN:0730-3157
DOI:10.1109/COMPSAC.2017.135