| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 719395 | IFAC Proceedings Volumes | 2009 | 6 Pages |
Abstract
This paper focuses mainly on the transformation of UML activity diagrams into Event B for the specification and the verification of parallel and distributed workflow applications. With this transformation, UML models could be verified by verifying derived event B models. The design is initially expressed graphically with UML and translated into Event B. The resulting model is then enriched with invariants describing dynamic properties such as deadlock freeness, livelock freeness and reachability. The approach uses activity diagrams meta-model.
Related Topics
Physical Sciences and Engineering
Engineering
Computational Mechanics
Authors
Leila Jemni Ben Ayed, Najet Hamdi,