Résumé:
Aujourd’hui, les systèmes sont construits à partir d’un ensemble de composants interconnectes pour produire un comportement incluant une ou plusieurs taches. Les contraintes imposées ´ a ces systèmes en termes de fonctionnalité, de fiabilité, de coût et de délais de mise sur le marché sont très stricts. Malheureusement, ` leurs développement devient un processus difficile, parce que les applications embarquées a temps réel sont de plus en plus complexes et la demande pour des ´ systèmes de haute qualité est en train de devenir un grand défi. Récemment, la ´ validation formelle a pu répondre aux contraintes des développeurs afin de prédire ´ le comportement du système et garantir son exactitude avant sa mise en œuvre. ` L’objectif de cette thèse est de fournir un framework formel qui permet l’évaluation ´ probabiliste et la vérification des exigences fonctionnelles sur un système modélisé par SysML internal blocks diagrams. Notre principale contribution est de fournir une nouvelle approche pour vérifier automatiquement le comportement des systèmes ` probabilistes sous contraintes temporelles en fonction de leurs exigences fonctionnelles. La vérification de la conception est basée sur les techniques de vérification des modèles probabilistes dont les propriétés sont exprimées en logique temporelle. Aussi, notre approche permet l’exploration automatique de l’espace de déploiement ´ qui maximise la durée de vie du système on considérant les caractéristiques de la plate-forme matérielle. Pour démontrer l’efficacité de notre approche, nous appliquons cette méthode sur un exemple académique et aussi sur les systèmes automobiles.
