Spécification et Vérification des Systèmes basés sur les Données – SVeDaS

Au cours des dernières années, les systèmes dits data-aware (DaS) ont été proposés comme un cadre global pour modéliser processus métier complexes en considérant les données et les processus comme des composantes de la meme importance dans la description du système. Ce paradigme est particulièrement adapté à modéliser les enchères et les méchanismes basés sur les enchères dans le commerce électronique.

Le projet SVeDaS vise à faire progresser l'état-de-l'art dans la modélisation, l'analyse et le déploiement de systèmes data-aware en utilisant une approche nouvelle, compositionelle et basée sur des agents dans leur spécification et vérification.

Les objectifs principaux du projet Svedas peuvent être résumés comme suit:

1. introduire des modèles computationnels basés sur les agents pour les systèmes data-aware, qui soient capables d'exprimer des processus métier complexes, y compris les enchères dans les marchés électroniques;

2. explorer des langages formels pour la spécification des comportements stratégiques d'agents autonomes (y compris la robustesse contre les comportements malveillants, ainsi que la manipulabilité et la collusion dans les ventes aux enchères) qui concernent les processus métier ainsi que les agents qui y agissant;

3. analyser les propriétés formelles de ces modèles data-aware, en particulier les questions relatives à la vérification formelle dans des contextes d'information imparfaite;

4. répérer des classes de systèmes data-aware ainsi que des fragments logiques expressifs, qui aient un problème de model checking décidable, et qui prêtent également à des methodes de vérification efficace;

5. développer des outils et des techniques de model-checking pour la vérification et la validation des systèmes data-aware dans des scénarios multi-agents, en mettant l'accent sur les mécanismes aux enchères.

Nous prévoyons que les résultats du projet SVeDaS contribueront de manière significative à notre compréhension des systèmes data-aware, améliorant ainsi la conception et la gestion des processus métier par le biais de la vérification formelle par model checking.
À son tour, ces contributions contribueront à la construction de systèmes plus surs et fiables, ainsi qu'à la réduction des coûts des défauts dans les mécanismes basés sur enchères pour le commerce électronique et l'e-business.