Formalisation and Analysis of Time and Timed BPEL Processes by means of Time Models

Different standards and languages have been proposed in the literature for modeling the composition of Web services. Unfortunately, these languages are essentially syntactic and, thus, contain much ambiguity and inconsistency. In addition, the formal verification of these languages is impossible. In this thesis, we propose transformation approaches to high and low level real-time formal models in order to allow the formal representation, analysis, verification and refinement of BPEL Web services compositions. Both, timed constraints and the durations of interactions between these services are taken into account. We present a formal environment, named FMEBP, for modeling business processes. This environment is based on a transformation approach that translates Web services, described in BPEL language, to abstract specifications, written in a high-level real-time language, called D-LOTOS.Différents standards et langages ont été proposés dans la littérature pour modéliser la composition de services Web. Malheureusement, ces langages sont essentiellement syntaxiques et contiennent ainsi beaucoup d’ambiguïté et d’incohérence. En outre, la vérification formelle des langages proposés est impossible. Dans cette thèse, nous proposons des approches de transformation vers des modèles formels temps-réel de haut et de bas niveau permettant la représentation formelle, l’analyse, la vérification et le raffinement de compositions de services Web BPEL. Par ailleurs, les contraintes temporelles et les durées des interactions entre ces services sont prises en compte. Nous présentons un environnement formel, nommé FMEBP, pour la modélisation des processus métiers. Cet environnement est basé sur une approche de transformation qui traduit des services Web, décrits dans le langage BPEL, en des spécifications abstraites, écrites dans un langage temps-réel de haut-niveau, appelé D-LOTOS