Item request has been placed! ×
Item request cannot be made. ×
loading  Processing Request

A Direct Formal Semantics for BPMN Time-Related Constructs

Item request has been placed! ×
Item request cannot be made. ×
loading   Processing Request
  • معلومة اضافية
    • Contributors:
      Université Mohamed Khider de Biskra (BISKRA); Modélisation et Vérification (MoVe); LIP6; Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS); Models And Reuse Engineering, Languages (MAREL); Laboratoire d'Informatique de Robotique et de Microélectronique de Montpellier (LIRMM); Université de Montpellier (UM)-Centre National de la Recherche Scientifique (CNRS)-Université de Montpellier (UM)-Centre National de la Recherche Scientifique (CNRS); Université Paris Nanterre (UPN); Université Paris Lumières (UPL); Assistance à la Certification d’Applications DIstribuées et Embarquées (IRIT-ACADIE); Institut de recherche en informatique de Toulouse (IRIT); Université Toulouse Capitole (UT Capitole); Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse - Jean Jaurès (UT2J); Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3); Université de Toulouse (UT)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP); Université de Toulouse (UT)-Toulouse Mind & Brain Institut (TMBI); Université Toulouse - Jean Jaurès (UT2J); Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3); Université de Toulouse (UT)-Université Toulouse Capitole (UT Capitole); Université de Toulouse (UT); Institut National Polytechnique (Toulouse) (Toulouse INP); ANR-16-CE25-0006,PARDI,Vérification de systèmes distribués paramétrés(2016)
    • بيانات النشر:
      HAL CCSD
    • الموضوع:
      2021
    • Collection:
      Université Paris Lumières: HAL
    • الموضوع:
    • نبذة مختصرة :
      International audience ; BPMN supports the design of intra-organization workflows and inter-organization collaborations. This rich notation includes elements to deal with models where time is central. However, the expressiveness of the BPMN time-related constructs hampers the definition of a formal semantics including them, and the provision of formal analysis means for timed process models. We propose here a first-order logic semantics for a subset of BPMN that includes its time-related constructs. With reference to related work, we support the specification of datetimes, durations, and cycles, using ISO-8601 formats as specified in the standard. Our approach is tool-supported by a model transformation into the Alloy formal language and its bounded counter-example generator. Our tool and model database are open source and freely available.
    • Relation:
      hal-03170814; https://hal.science/hal-03170814; https://hal.science/hal-03170814/document; https://hal.science/hal-03170814/file/ENASE.pdf
    • الرقم المعرف:
      10.5220/0010462901380149
    • الدخول الالكتروني :
      https://hal.science/hal-03170814
      https://hal.science/hal-03170814/document
      https://hal.science/hal-03170814/file/ENASE.pdf
      https://doi.org/10.5220/0010462901380149
    • Rights:
      http://creativecommons.org/licenses/by-nc-nd/ ; info:eu-repo/semantics/OpenAccess
    • الرقم المعرف:
      edsbas.F87802FD