Mechanized support for the formal specification, verification and deployment of component-based applications

Nuno Gaspar 1
1 SCALE - Safe Composition of Autonomous applications with Large-SCALE Execution environment
CRISAM - Inria Sophia Antipolis - Méditerranée , COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Résumé : Cette thèse appartient au domaine des méthodes formelles. Nous nous concentrons sur leur application à une méthodologie spécifique pour le développement de logiciels: l'ingénierie à base de composants. Le Grid Component Model (GCM) suit cette méthodologie en fournissant tous les moyens pour définir, composer, et dynamiquement reconfigurer les applications distribuées à base de composants. Dans cette thèse, nous abordons la spécification formelle, la vérification et le déploiement d'applications GCM reconfigurables et distribuées. Notre première contribution est un cas d'étude industriel sur la spécification comportementale et la vérification d'une application distribuée et reconfigurable: L'HyperManager. Notre deuxième contribution est une plate-forme, élaborée avec l'assistant de preuve Coq, pour le raisonnement sur les architectures logicielles: Mefresa. Cela comprend la mécanisation de la spécification du GCM, et les moyens pour raisonner sur les architectures reconfigurables GCM. En outre, nous adressons les aspects comportementaux en formalisant une sémantique basée sur les traces d'exécution de systèmes de transitions synchronisées. Enfin, notre troisième contribution est un nouveau langage de description d'architecture (ADL): Painless. En outre, nous discutons son intégration avec ProActive, un intergiciel Java pour la programmation concurrente et distribuée, et l'implantation de référence du GCM.
Type de document :
Thèse
Other [cs.OH]. Université Nice Sophia Antipolis, 2014. English. < NNT : 2014NICE4127 >
Liste complète des métadonnées


https://hal.inria.fr/tel-01114217
Contributeur : Abes Star <>
Soumis le : vendredi 10 avril 2015 - 12:21:06
Dernière modification le : mercredi 5 juillet 2017 - 01:17:02
Document(s) archivé(s) le : lundi 14 septembre 2015 - 06:51:06

Fichier

2014NICE4127.pdf
Version validée par le jury (STAR)

Identifiants

  • HAL Id : tel-01114217, version 2

Collections

Citation

Nuno Gaspar. Mechanized support for the formal specification, verification and deployment of component-based applications. Other [cs.OH]. Université Nice Sophia Antipolis, 2014. English. < NNT : 2014NICE4127 >. <tel-01114217v2>

Partager

Métriques

Consultations de
la notice

427

Téléchargements du document

141