Model based system assessment: formalisation et évaluation de systèmes autonomes en Event-B

Cet article vise à décrire une architecture de sécurité de systèmes autonomes à l’aide de la méthode formelle Event-B. Le formalisme Event-B supporte une conception rigoureuse de ces systèmes. La technique de raffinement permet une modélisation progressive en vérifiant la correction et la pertinence des modèles par décharge de preuves. L’application de la méthode Event-B présente un intérêt dans la formalisation des relations entre couches qui assurent la cohérence d’un fonctionnement sûr ainsi que le respect des exigences de sécurité concernées par notre analyse. Par conséquent, la modélisation autour de ces relations fait apparaître en permanence un comportement nominal associé à des comportements en présence de fautes sous l’hypothèse d’une architecture intégrant des mécanismes de tolérance aux fautes