Remerciez-le!

Remerciez @Admin pour avoir partagé cet document gratuitement, de la manière la plus simple, en partageant sur les réseaux sociaux.

Validation formelle des systèmes informatiques (VFSI) 2020/2021 Master 1 Génie

Validation formelle des systèmes informatiques (VFSI) 2020/2021 Master 1 Génie Logiciel 1 Introduction les systèmes informatiques contrôlent de plus en plus de tâches dans notre entourage, de l'instrument médical au système de contrôle du trafic aérien.  Il est évident que les systèmes, qui assurent ces tâches doivent être fiables et sûres. 2 Exemples de systèmes Transport: Systèmes de contrôle ferroviaire: Système de contrôle et de gestion des trains Système de contrôle d'une ligne de métro /Tramway 3 Exemples de systèmes Aviation: -Système de contrôle automatisé du trafic aérien -Système de pilotage automatique d’un avion Banque: -Distributeurs automatique de billets 4 Exemples de systèmes Automobiles: - Système ESP ( anti-dérapage), Calculateur, ... - Chaine de montage de véhicule. - Smart cars ( conduite, stationnement, freinage ,...). Maison: Domotique Smart Home ( systèmes de gestion d'énergie, du Confort, de sécurité...). 5 Systèmes complexe • Un système est dit complexe si le résultat final n'est pas prédictible directement en connaissant les règles qui disent comment le système change • S.O.S (System Of Systems): résulte du fonctionnement collaboratif de systèmes 6 SOS 7 SOS 8 Pourquoi la validation des systèmes informatiques? • Sécurité des personnes, • Retour des produits, • Relations contractuelles, Cout de bugs ( des milliards de dollars) 9 Bugs /couts • The Systems Sciences Institute at IBM has reported that “the cost to fix an error found after product release was four to five times as much as one uncovered during design, and up to 100 times more than one identified in the maintenance phase.” 10 Bugs /couts • "désastre LOUVOIS". " Cet acronyme désigne un logiciel, lancé en 2009, un projet majeur de modernisation du secteur public permettant la gestion de la paye des militaires", Quatre ans plus tard, on compte 100.000 dossiers litigieux, à cause de soldes non versées et de trop perçus. Et cela s’aggrave: 35 millions d’euros ont été versés en trop sur les soldes des militaires, rien qu’en janvier 2013, selon la Cour des Comptes. " Source: www.challenges.fr/economie 11 Bugs /couts • Toyota recall • Toyota a rappelé plus de 9 millions de voitures dans le monde entier en 2010, mais il n'a pas été à cause d'un problème mécanique. Les voitures avaient un bug logiciel qui a causé un retard dans le système anti-blocage de frein (ABS). 12 Validation vs Vérification • Validation : Développons-nous le bon produit ? • Vérification : Développons-nous correctement le produit ? • La vérification concerne la preuve de propriétés alors que la validation est un processus plus général qui va jusqu’à la satisfaction du client vis- à-vis du produit. 13 Validation et vérification : Définitions Vérification : La vérification est l’ensemble des actions d’inspection, test, preuve automatique, ou autres techniques appropriées permettant d’établir et de documenter la conformité des étapes de développement vis-à-vis de critères préétablis. 14 Validation et vérification : Définitions Validation: La validation consiste à évaluer l’adéquation du système développé vis à-vis des besoins exprimés par ses futurs utilisateurs. Disposer d’un modèle cohérent, et si possible complet, du système que l’on souhaite développer permet de raisonner sur ce système. 15 la validation des systèmes informatiques Est le processus d'assurance-qualité, garantissant qu'un système informatique répondra aux exigences requises, de manière cohérente, dans un environnement opérationnel donné. 16 La Validation peut être: informelle ou formelle informelle : Inspection de fautes dans les programmes. Est-ce que toutes les variables sont initialisées avant l’utilisation de leurs valeurs ? Est-ce que toutes les constantes ont été nommées ? Est-ce que les indices des tableaux sont corrects ? 17 • Est-ce la condition de chaque test est correcte ? • Est-ce que l’on est sûr que chaque boucle se termine ? • Est-ce que toutes les variables d’entrée sont valides ? • ... 18 Validation formelle Il s’agit de prouver formellement la correction d’une spécification ou d’un programme la vérification impose: Une description formelle du système, ainsi qu'une spécification formelle des propriétés. 19 Méthodes Formelles DÉFINITION: Le terme « méthodes formelles » se réfère à l'utilisation des techniques de la logique et des mathématiques discrètes dans la spécification, la conception et la construction de systèmes informatiques et de logiciels. Le mot «formelle» provient de la logique formelle. La logique formelle se réfère à des modes de raisonnement qui sont valides en vertu de leur forme, en indépendant de leur contenu. 20 Rôle et objectif Réduire la dépendance au jugement et à l'intuition humaine dans l'évaluation des arguments. 21 Validation formelle • Principe des méthodes formelles: – Utiliser les mathématiques pour concevoir et si possible réaliser des systèmes informatiques. 22 Validation formelle • Parmi les formalisme les plus utilisés, les réseaux de Petri occupent une place prépondérante et se trouvent être l'outil ayant été le plus largement étudié. 23 Validation formelle • Parmi les méthodes de validation formelle,deux approches sont essentiellement utilisées: • Les vérifications basées sur les preuves de théorèmes. • Les vérifications basées sur le model-checking. 24 Les vérifications basées sur les preuves de théorèmes. A pour principe de poser un ensemble d'axiomes, souvent donnés par le concepteur, puis à prouver un ensemble d'assertions déterminant ainsi la conformité du système. Cette preuve est faite plus ou moins manuellement. 25 Les vérifications basées sur les preuves de théorèmes. Par exemple: Une pré-condition qui assure une post-condition après l'exécution du programme. 26 Les vérifications basées sur le model-checking. Elle est basées sur les modèles, permet une vérification simple et efficace et elle est complètement automatisables. La vérification basée sur les modèles ou Model- checking est surtout applicable pour les systèmes ayant un espace d'états fini. 27 Les vérifications basées sur le model-checking. Les algorithmes de vérification dans cette méthode utilisent l'ensemble des états que le système peut atteindre pour prouver la satisfaction ou la non-satisfaction des propriétés. 28 Model checking • Principe: « étant donnés une formule F ‘’propriété à vérifier’’ (en logique LTL, CTL, etc) et un système de transitions S, est-ce que S satisfait F ?» (on dit aussi «est-ce que S est un modèle pour F » d’où le nom de model- checking). 29 Test de Logiciel Les tests déterminent la qualité du logiciel. Les tests unitaires sont orientés code. Les tests d’acceptation vérifient les attentes d’un produit logiciel. 30 Simulation Une des techniques les plus utilisées, pour valider un système est la simulation. Elle consiste à définir un modèle pour le système ou pour son environnement et à exécuter les programmes correspondants sur machine et analyser ensuite les résultats. 31 32 Les Réseaux de Petri (Rdp) 33 Les Réseaux de Petri (Rdp) • RDP : une approche orienté modèle • C’est à la fois un outil de modélisation et un outil d’analyse • Une notation mathématique et graphique 34 Les Réseaux de Petri (Rdp) Rdp Places /Transition 35 Concepts fondamentaux Ensemble de Places : P Ensemble de transitions : T Arcs entrant/sortant des transitions et des places Jetons (dans des places) Marquage (des places) : Mi Fonctionnement du réseau : franchissement des transitions et donc, changement de l’état global (marquage). 36 Une place est représentée par un cercle Une transition par un trait P T Un arc relie soit une place à une transition soit une transition à une place 37 Marquage: Chaque place contient un nombre entier positif ou nul de marques ou jetons. Le marquage M définit l'état du système décrit par le réseau à un instant donné. C'est un vecteur colonne. Le i éme élément du vecteur correspond au nombre de jetons contenus dans la place Pi 38 Marquage: Exemple 1 39 Marquage: Exemple 2 40 Marquage: Exemple 3 41 • Franchissement d'une transition Une transition est franchissable lorsque toutes les places qui lui sont en amont (ou toutes les places d'entrée de la transition) contiennent au moins un jeton. 42 Le franchissement consiste à retirer un jeton de chacune des places d'entrée et à rajouter un jeton à chacune des places de sortie de la même transition. Avant franchissement Après franchissement 43 En informatique: Il ne faut jamais raisonner avec l’exemple. 44 Il faut comprendre l’exemple pour l’exploiter Exemple1: Considérons un système connecté à une imprimante. Initialement ,elle est au repos . Quand elle reçoit une demande d'impression , elle passe dans l’état «réception des données»,puis ,quand elle a reçu les données , elle passe dans l'état «en impression», Et enfin, quand l'impression est terminée ,elle réinitialise ses paramètres et revient à l'état «au repos». Nous pouvons décrire l'état de l'imprimante à l'aide des 4 Prédicats suivants: p 1: L'imprimante est au repos p 2: L'imprimante reçoit les données p 3: L'imprimante est en cours d'impression p 4: L'impression est terminée Les quatre événements suivants permettent de décrire le fonctionnement de l'imprimante: e 1: Réception d'une demande d'impression e 2 :Début d'impression e 3 : Fin d'impression e 4 :Fin de réinitialisation Ces événements correspondent aux actions effectuées par l'imprimante, le déclenchement d'une action est conditionné par l'état de l'imprimante: l'action «Fin d'impression» ne peut se produire que si l'imprimante est en cours d'impression . Le déroulement d'une action peut modifier l'état de l’imprimante: après uploads/Management/ vfsi-cours.pdf