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

Abstract

Un développement plus récent des méthodes de vérification de modèle conventionnelles est connu sous le nom de vérification de modèle probabiliste, qui permet l'étude intégrée des aspects qualitatifs et quantitatifs des systèmes stochastiques. Dans cette lettre, nous définissons d'abord un système embarqué, puis discutons de ses nombreux types, de ses utilisations potentielles, de sa convivialité et de ses services. Ensuite, après avoir appris le langage de l'outil PRISM et comment l'utiliser, nous avons discuté de plusieurs modèles de probabilités aléatoires que nous pourrions utiliser pour simuler le comportement de ce système. Ensuite, pour examiner le système de prévision des accidents, nous avons effectué une vérification de modèle probabiliste (APS). en utilisant un modèle de Markov caché généré par PRISM A more recent development of conventional model-checking methods is known as probabilistic model checking, which allows for the integrated investigation of both qualitative and quantitative aspects of stochastic systems. In this letter, we first define an embedded system and then discuss its many types, potential uses, usability, and services. Then, after learning the PRISM tool's language and how to use it, we discussed several random probability models that we might use to simulate the behavior of this system. Next, to examine the Accident Prediction System, we performed probabilistic model verification (APS). utilizing a PRISM-generated hidden Markov model. تطور أحدث لطرق التحقق من النموذج التقليدية يُعرف باسم التحقق من النموذج الاحتمالي، والذي يسمح بالتحقيق المتكامل للجوانب النوعية والكمية للأنظمة العشوائية. في هذه الرسالة، نقوم أولاً بتعريف النظام المدمج ثم نناقش أنواعه العديدة، واستخداماته المحتملة، وقابليته للاستخدام، والخدمات التي يقدمها. بعد ذلك، وبعد تعلم لغة أداة PRISM وكيفية استخدامها، ناقشنا عدة نماذج احتمالية عشوائية يمكننا استخدامها لمحاكاة سلوك هذا النظام. بعد ذلك، لدراسة نظام التنبؤ بالحوادث، قمنا بإجراء تحقق احتمالي من النموذج (APS) باستخدام نموذج ماركوف المخفي الذي تم إنشاؤه بواسطة PRISM.