Search

The introduction of embedded electronic in car industry induced a technological revolutionthat will last for years. Embedded electronic systems are more and more complex and theirfeatures involve the adaptation and structuring of the whole design activities. Verification,validation, design, and of course safety analysis should be integrated in a same process. First,we identify a class of formalism able to represent the functional and behavioral aspects of thesystem, and suited for hybrid and real time features. This model is the support of themethodology. Then, we propose an exploitation of formal methods, such as model-checking,to validate and check properties of the model and complement usual methods like tests andsimulations. Finally, we particularly emphasize the dependability aspects. A method, based onthe construction of an aggregated Markov graph, is developed. The advantage of thisapproach is to be able to model and assess the reliability of a dynamic hybrid system. Themain steps consist in spliting up the dynamic of the system and the dynamic of the failureprocess by the mean of the singular perturbation method. Then, we identify and we evaluatevariables of the system which interact with the failure dynamic. Simulation is used to estimatethese variables, because of its ability to handle complex systems. The variables are thenintegrated in the aggregated Markov graph.; La révolution technologique que connaît le secteur automobile avec la multiplication dessystèmes électroniques et informatiques embarqués n'est pas près de s'essouffler. Il estmanifeste que la complexité croissante et la spécificité des systèmes embarqués justifieront deplus en plus le besoin de structurer l'ensemble des activités de développement. Vérification,validation, conception et bien entendu sûreté de fonctionnement font partie intégrante d'unmême processus. Nous cherchons tout d'abord à définir un formalisme de modélisationfonctionnelle et comportementale, support de la méthodologie, et en cohérence avec lesspécificités des systèmes mécatroniques. En particulier, les aspects hybrides et temps réeldoivent pouvoir être représentés. Ensuite, sur le plan de la vérification et de la validation,nous proposons d'exploiter les méthodes formelles, telles que le model-checking, encomplément des tests et des simulations habituellement utilisées dans l'industrie. Enfin nousattachons une importance centrale à la sûreté de fonctionnement. Afin de pallier auxinsuffisances et aux limites des méthodes habituellement utilisées, nous proposons uneapproche basée sur la construction d'un graphe de Markov agrégé. L'originalité tient dans sacapacité de répondre à un problème de représentation et d'évaluation de la fiabilité dessystèmes dynamiques hybrides. Les principales étapes consistent à découpler la dynamique dusystème et la dynamique du processus de défaillance grâce à la théorie des perturbationssingulières, puis d'identifier et estimer les grandeurs du système influençant la dynamique desdéfaillances. Ces grandeurs sont évaluées par de simples simulations dans le but de pouvoirtraiter des systèmes complexes. Ceux-ci sont alors intégrés dans le graphe agrégé.

The introduction of embedded electronic in car industry induced a technological revolutionthat will last for years. Embedded electronic systems are more and more complex and theirfeatures involve the adaptation and structuring of the whole design activities. Verification,validation, design, and of course safety analysis should be integrated in a same process. First,we identify a class of formalism able to represent the functional and behavioral aspects of thesystem, and suited for hybrid and real time features. This model is the support of themethodology. Then, we propose an exploitation of formal methods, such as model-checking,to validate and check properties of the model and complement usual methods like tests andsimulations. Finally, we particularly emphasize the dependability aspects. A method, based onthe construction of an aggregated Markov graph, is developed. The advantage of thisapproach is to be able to model and assess the reliability of a dynamic hybrid system. Themain steps consist in spliting up the dynamic of the system and the dynamic of the failureprocess by the mean of the singular perturbation method. Then, we identify and we evaluatevariables of the system which interact with the failure dynamic. Simulation is used to estimatethese variables, because of its ability to handle complex systems. The variables are thenintegrated in the aggregated Markov graph., La révolution technologique que connaît le secteur automobile avec la multiplication dessystèmes électroniques et informatiques embarqués n'est pas près de s'essouffler. Il estmanifeste que la complexité croissante et la spécificité des systèmes embarqués justifieront deplus en plus le besoin de structurer l'ensemble des activités de développement. Vérification,validation, conception et bien entendu sûreté de fonctionnement font partie intégrante d'unmême processus. Nous cherchons tout d'abord à définir un formalisme de modélisationfonctionnelle et comportementale, support de la méthodologie, et en cohérence avec lesspécificités des systèmes mécatroniques. En particulier, les aspects hybrides et temps réeldoivent pouvoir être représentés. Ensuite, sur le plan de la vérification et de la validation,nous proposons d'exploiter les méthodes formelles, telles que le model-checking, encomplément des tests et des simulations habituellement utilisées dans l'industrie. Enfin nousattachons une importance centrale à la sûreté de fonctionnement. Afin de pallier auxinsuffisances et aux limites des méthodes habituellement utilisées, nous proposons uneapproche basée sur la construction d'un graphe de Markov agrégé. L'originalité tient dans sacapacité de répondre à un problème de représentation et d'évaluation de la fiabilité dessystèmes dynamiques hybrides. Les principales étapes consistent à découpler la dynamique dusystème et la dynamique du processus de défaillance grâce à la théorie des perturbationssingulières, puis d'identifier et estimer les grandeurs du système influençant la dynamique desdéfaillances. Ces grandeurs sont évaluées par de simples simulations dans le but de pouvoirtraiter des systèmes complexes. Ceux-ci sont alors intégrés dans le graphe agrégé.