Home > Table of Contents


Proceedings of 2009 International Symposium on Computer Science and Computational Technology (ISCSCT 2009)

Huangshan, China, December 26-28, 2009

Editors: Fei Yu, Guangxue Yue, Jian Shu, Yun Liu

AP Catalog Number: AP-PROC-CS-09CN005

ISBN: 978-952-5726-07-7 (Print), 978-952-5726-08-4 (CD-ROM)

Page(s): 496-499

From Graphical Model in UML Activity Diagrams to Formal Specification in Event B for Workflow Applications Modeling

Ahlem Ben Younes and Leila Jemni Ben Ayed

Full text: PDF


The lack of a precise semantics for UML AD makes the reasoning on models constructed using such diagrams infeasible. However, such diagrams are widely used in domains that require a certain degree of confidence. Due to economical interests, the business domain is one of these. To enhance confidence level of UML AD, this paper provides a formal definition of their syntax and semantics. The main interest of our approach is that we chose UML AD, which are recognized to be more tractable by engineers. We outline the translation of UML AD into Event B in order to verify functional properties of workflow models (such as deadlock-inexistence, liveness, fairness) automatically, using the B powerful support tools like B4free. We propose a solution to specify time in Event B, and by an example of workflow application, we illustrate the proposed technique.

Index Terms

Specification, Formal verification, Validation, UML, Event B, workflow application

Copyright @ 2009 ACADEMY PUBLISHER All rights reserved