Belluccini, Sara (2023) Exploiting Process Algebras and BPM Techniques for Guaranteeing Success of Distributed Activities. Advisor: De Nicola, Prof. Rocco. Coadvisor: Tiezzi, Prof. Francesco . pp. 159. [IMT PhD Thesis]
![[img]](http://e-theses.imtlucca.it/style/images/fileicons/text.png) |
Text (Doctoral thesis)
Belluccini_phdthesis.pdf - Published Version Available under License Creative Commons Attribution Non-commercial Share Alike. Download (1MB) |
Abstract
The communications and collaborations among activities, pro- cesses, or systems, in general, are the base of complex sys- tems defined as distributed systems. Given the increasing complexity of their structure, interactions, and functionali- ties, many research areas are interested in providing mod- elling techniques and verification capabilities to guarantee their correctness and satisfaction of properties. In particular, the formal methods community provides robust verification techniques to prove system properties. However, most ap- proaches rely on manually designed formal models, making the analysis process challenging because it requires an expert in the field. On the other hand, the BPM community pro- vides a widely used graphical notation (i.e., BPMN) to design internal behaviour and interactions of complex distributed systems that can be enhanced with additional features (e.g., privacy technologies). Furthermore, BPM uses process min- ing techniques to automatically discover these models from events observation. However, verifying properties and ex- pected behaviour, especially in collaborations, still needs a solid methodology. This thesis aims at exploiting the features of the formal meth- ods and BPM communities to provide approaches that en- able formal verification over distributed systems. In this con- text, we propose two approaches. The modelling-based ap- proach starts from BPMN models and produces process al- gebra specifications to enable formal verification of system properties, including privacy-related ones. The process mining- based approach starts from logs observations to automati- xv cally generate process algebra specifications to enable veri- fication capabilities.
| Item Type: | IMT PhD Thesis |
|---|---|
| Subjects: | Q Science > QA Mathematics > QA75 Electronic computers. Computer science |
| PhD Course: | Computer science and systems engineering |
| Identification Number: | https://doi.org/10.13118/imtlucca/e-theses/386 |
| NBN Number: | urn:nbn:it:imtlucca-29528 |
| Date Deposited: | 01 Aug 2023 07:28 |
| URI: | http://e-theses.imtlucca.it/id/eprint/386 |
Actions (login required, only for staff repository)
 |
View Item |
