Text size
  • Small
  • Medium
  • Large
Contrast
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

    On Formalizing UML2 Activities Using TPNets: Case Studies

    Fifth International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2011)

    Tunis, Tunisia, 15-16 September 2011

    AUTHORS

    Sabine Boufenara, Kamel Barkaoui, Faiza Belala and Hanifa Boucheneb

    ABSTRACT

    Transactional Petri Nets (TPNets) are a new class of high-level Zero-Safe Nets (ZSNs), defined as a more suitable semantic framework for UML2 activity diagrams. Indeed, they ensure reactivity and synchronization of concurrent flows triggering with their junction. Reactivity is guaranteed due to the real time massive cancellation semantics based on the definition of new dynamic enabling rules and the imposed priority among executions. Global synchronization in turn is assured thanks to non-locality principle, an outcome of exploiting atomic stable transactions. Rewriting logic is defined as the operational semantics framework of TPNets.

    PAPER FORMATS

    PDF filePDF Version of this Paper (291kb)