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

A compositional method for the synthesis of asynchronous communication mechanisms

Item request has been placed! ×
Item request cannot be made. ×
loading   Processing Request
  • معلومة اضافية
    • Contributors:
      Universitat Politècnica de Catalunya. Departament de Ciències de la Computació; Universitat Politècnica de Catalunya. ALBCOM - Algorismia, Bioinformàtica, Complexitat i Mètodes Formals
    • بيانات النشر:
      Springer
    • الموضوع:
      2007
    • Collection:
      Universitat Politècnica de Catalunya, BarcelonaTech: UPCommons - Global access to UPC knowledge
    • نبذة مختصرة :
      Asynchronous data communication mechanisms (ACMs) have been extensively studied as data connectors between independently timed concurrent processes. In previous work, an automatic ACM synthesis method based on the generation of the reachability graph and the theory of regions was proposed. In this paper, we propose a new synthesis method based on the composition of Petri net modules, avoiding the exploration of the reachability graph. The behavior of ACMs is formally defined and correctness properties are specified in CTL. Model checking is used to verify the correctness of the Petri net models. The algorithms to generate the Petri net models are presented. Finally, a method to automatically generate C++ source code from the Petri net model is described. ; Peer Reviewed ; Postprint (author's final draft)
    • File Description:
      20 p.; application/pdf
    • ISBN:
      978-3-540-73093-4
      3-540-73093-1
    • Relation:
      https://link.springer.com/book/10.1007/978-3-540-73094-1; Gorgônio, K.; Cortadella, J.; Xia, F. A compositional method for the synthesis of asynchronous communication mechanisms. A: "Petri Nets and Other Models of Concurrency, ICATPN 2007, 28th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency: Siedlce, Poland, June 25-29, 2007: proceedings". Springer, 2007, p. 144-163.; http://hdl.handle.net/2117/133432
    • الرقم المعرف:
      10.1007/978-3-540-73094-1
    • الدخول الالكتروني :
      http://hdl.handle.net/2117/133432
      https://doi.org/10.1007/978-3-540-73094-1
    • Rights:
      Open Access
    • الرقم المعرف:
      edsbas.E211F48