Nos tutelles

CNRS

Nos partenaires


Accueil > Publications > Thèses > Archives Thèses > Thèses 2014 - 2015

LI Haizhou


Modélisation et vérification des processus métier orientés données probabilistes

Jeudi 26 mars 2015 - 14 h 30 - Salle A215 - Bâtiment ISIMA

There is a wide range of new applications that stress the need for business process models that are able to handle imprecise data. This thesis studies the underlying modelling and analysis issues. It uses as formal model to describe process behaviors a labelled transitions system in which transitions are guarded by conditions defined over a probabilistic database. To facilitate verification problems, we decompose this model to a set of traditional automata associated with probabilities named as world-partition automata. Next, this thesis presents an approach for testing probabilistic simulation preorder in this context. A complexity analysis reveals that the problem is in 2-exptime, and is EXPTIME-hard, w.r.t. expression complexity while it matches probabilistic query evaluation w.r.t. data-complexity. Then P-LTL and P-CTL model
checking methods are studied to verify this model. In this context, the complexity of P-LTL and P-CTL model checking is in EXPTIME. Finally a prototype called "PRODUS" which is a modeling and verification tool is introduced and we model a realistic scenario in the domain of GIS (graphical information system) by using our approach).

Jury :
- Farouk Toumani, Université Blaise Pascal
- François Pinet, IRSTEA
- Salima Benbernou, LIPADE, Université Paris Descartes
- Karine Zeitouni, PRISM, Université de Versailles-St-Quentin
- Vasile Marian Scuturici, INSA de Lyon
- Sandro Bimonté, IRSTEA.