Home // PATTERNS 2011, The Third International Conferences on Pervasive Patterns and Applications // View article

A Formalization of UML AD Refinement Patterns in Event B

Authors:
Ahlem Ben Younes
Leila Jemni Ben Ayed

Keywords: Progressive Development; Workflow Applications; Specification; Refinement UML AD; Patterns; Event-B; Formal Verification.

Abstract:
In this paper, we propose a specification and verification technique using the combination UML Activity Diagrams (AD) and Event B to both improve graphical representation of the workflow application structure and its functions. Its required properties are also verified. The workflow is initially expressed incrementally graphically with UML AD, then translated into Event B and verified using the B powerful support tools. The Event-B expression of the UML AD model allows us to give it a precise semantics. We propose a workflow applications constructive approach in witch Event B models are built incrementally from UML AD models, driven by UML AD refinement patterns. The use of the B formal method and its refinement mechanism allows the verification of the correction of the UML AD refinement patterns.

Pages: 116 to 121

Copyright: Copyright (c) IARIA, 2011

Publication date: September 25, 2011

Published in: conference

ISSN: 2308-3557

ISBN: 978-1-61208-158-8

Location: Rome, Italy

Dates: from September 25, 2011 to September 30, 2011