Skip to Main content Skip to Navigation
Theses

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
Laboratoire I3S - 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.
Document type :
Theses
Complete list of metadatas

Cited literature [58 references]  Display  Hide  Download

https://hal.inria.fr/tel-01114217
Contributor : Abes Star :  Contact
Submitted on : Friday, April 10, 2015 - 12:21:06 PM
Last modification on : Tuesday, May 26, 2020 - 6:50:55 PM
Document(s) archivé(s) le : Monday, September 14, 2015 - 6:51:06 AM

File

2014NICE4127.pdf
Version validated by the jury (STAR)

Identifiers

  • 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⟩

Share

Metrics

Record views

667

Files downloads

376