Initiation à la preuve de programme avec Frama-C

Magazine
Marque
GNU/Linux Magazine
HS n°
Numéro
55
Mois de parution
juillet 2011
Domaines


Résumé
Avec Frama-c, vérifiez et validez vos programmes C de manière sûre par la preuve de programme.

1. Introduction

Afin de rendre les programmes plus sûrs, une approche mathématique de la programmation fut recherchée depuis les années 50. Celles-ci nous amènent à la preuve de programme, qui se caractérise comme étant la démonstration que les spécifications formelles d'un programme sont vraies. La spécification consiste à décrire très précisément ce que fait le programme. Si le programme est conforme à ses spécifications, le programme est considéré comme sûr [7][8].

À quel point un programme prouvé mathématiquement est sûr ? Et comment être sûr du vérificateur de preuve, sed quis custodiet ipsos custodes ? La sûreté du programme dépend des spécifications formulées. En effet, plusieurs classes de spécifications doivent être décrites afin d'obtenir une grande sûreté du programme. De plus, les vérificateurs de preuves font aujourd'hui encore l'objet de recherches poussées, un domaine en pleine ébullition, et de contrôles assidus (par exemple...

Cet article est réservé aux abonnés. Il vous reste 95% à découvrir.
à partir de 21,65€ HT/mois/lecteur pour un accès 5 lecteurs à toute la plateforme
J'en profite


Articles qui pourraient vous intéresser...

Analyse de code avec Cppcheck (et intégration sous Eclipse)

Magazine
Marque
GNU/Linux Magazine
HS n°
Numéro
112
Mois de parution
janvier 2021
Domaines
Résumé

Zut ! Encore un plantage !!! Combien de fois n’avez vous pas prononcé cette phrase, face au blocage d’une application de bureautique bien connue ou face à un crash système ? Sur un ordinateur de bureau, ce type de désagrément n’a d’autre effet que de faire monter votre niveau d’énervement, mais dans le cas d’un système embarqué, les effets sont bien plus graves. Heureusement, Cppcheck est là pour vous aider.

Réinvention de la roue... des temporisations

Magazine
Marque
GNU/Linux Magazine
HS n°
Numéro
112
Mois de parution
janvier 2021
Domaines
Résumé

Les temporisations sont essentielles au sein des systèmes d'exploitation et dans certaines applications, pour déclencher des actions à l'échéance d'un délai. Il existe différents algorithmes pour les gérer de manière efficace. Cet article présente la fusion de deux d'entre eux, pour en tirer le meilleur.

Mesure fine de déplacement par RADAR interférométrique à synthèse d’ouverture (InSAR) par radio logicielle

Magazine
Marque
GNU/Linux Magazine
Numéro
244
Mois de parution
janvier 2021
Domaines
Résumé

Nous avons démontré dans le premier article de la série la capacité à mesurer la distance à une cible (range compression), puis dans un deuxième temps à détecter l’angle d’arrivée du signal (azimuth compression). Fort de cette capacité de cartographier des cibles, nous allons conclure cette série sur la conception de RADAR à base de radio logicielle, et le traitement des signaux associé, par la mesure fine de déplacement des cibles par analyse de la phase (interférométrie) du signal, lors de la répétition des mesures.

Utilisation de l’IDE Visual Studio Code

Magazine
Marque
GNU/Linux Magazine
HS n°
Numéro
112
Mois de parution
janvier 2021
Domaines
Résumé

Visual Studio Code, un outil dont Microsoft est à l’origine, est Open Source et gratuit, multiplateforme et ouvert grâce à son architecture d’extensions. Mis à jour mensuellement, il est écrit par des développeurs pour des développeurs.

La surcharge ou overloading en Python

Magazine
Marque
GNU/Linux Magazine
HS n°
Numéro
112
Mois de parution
janvier 2021
Domaines
Résumé

On vous l’a dit et répété : Python est un langage à typage dynamique ! Ah... donc, on ne peut pas réaliser de surcharge de fonctions ou de méthodes ? Pour les débutants, on dira non, pour les autres, on peut toujours s’arranger avec Python...