PRISM : un outil de vérification probabiliste des systèmes embarqués- Etude de cas-

Abstract

Dans ce mémoire, nous avons défini un système embarqué, ses types, domaines d'utilisation, facilité et services qu'il fournit dans la vie quotidienne, puis nous avons expliqué un ensemble de types de modèles de probabilités aléatoires à travers lesquels nous pouvons modéliser le comportement de ce système, puis nous avons appris à connaître l'outil PRISM avec son langage et son mode d'utilisation, ce qui nous permet de vérifier, et en analysant, simulant le comportement de ces différents modèles, nous avons donc abordé l'étude du système embarqué, qui est le télescope Hubble, en utilisant l'un des modèles aléatoires de probabilité, le modèle de Markov caché à l'aide de l'outil PRISM. In this memory, we have defined an embedded system, its types, areas of use, ease and services that it provides in daily life, then we have explained a set of types of random probability models through which we can model the behavior of this system, then we got to know the PRISM tool with its language and its mode of use, which allows us to verify, and by analyzing, simulating the behavior of these different models, we therefore approached the study of the on-board system, which is the Hubble Telescope, using one of the random probability models, the Markov model hidden using the PRISM tool. في هذا البحث، قمنا بتعريف النظام المضمن، وأنواعه، ومجالات استخدامه، وسهولته والخدمات التي يقدمها في الحياة اليومية، ثم قمنا بشرح مجموعة من أنواع نماذج الاحتمالات العشوائية التي من خلالها يمكننا نمذجة سلوك هذا النظام، ثم تعرفنا على أداة PRISM ولغتها وطريقة استخدامها، والتي تتيح لنا التحقق وتحليل ومحاكاة سلوك هذه النماذج المختلفة، وبالتالي اقتربنا من دراسة النظام المدمج، وهو تلسكوب هابل، باستخدام أحد نماذج الاحتمالات العشوائية، وهو نموذج ماركوف المخفي باستخدام أداة PRISM.