Cette thèse propose un cadre afin de modéliser, vérifier et générer des allocations de fonctions d'un système embarqué sur des ressources avioniques. Ce cadre est fondé sur l'utilisation du langage Altarica pour décrire formellement la propagation des défaillances au sein d'un système embarqué, sur l'utilisation de techniques de vérification tel que le "model-checking" et la génération d'arbre de défaillances et sur les techniques de résolution de contraintes. Les travaux sont illustrés par deux études de cas: l'allocation de ressources de calcul et de communication à une fonction de "suivi de terrain" d'un avion de chasse, le placement des équipements d'un système hydraulique au sein d'un avion en tenant compte de risques tels que l'éclatement d'un pneu ou d'un réacteur.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00906924 |
| Date | 04 December 2008 |
| Creators | Sagaspe, Laurent |
| Publisher | Université Sciences et Technologies - Bordeaux I |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0015 seconds