基本説明
Ce manuel contient une introduction didactique des principes fondamentaux de la technique de vérification. Il traite de manière très pédagogique des éléments de stratégie pour vérifier et pour concevoir des logiciels.
Dans le monde de l'industrie et des services, la validation et la vérification des logiciels sont aujourd'hui des enjeux sécuritaires et économiques majeurs. La sécurité des passagers des véhicules de transport dépend par exemple de la sûreté des logiciels qui en contrôlent les fonctions motrices, tout comme la survie économique des fabricants de produits diffusés à des centaines de milliers d'exemplaires serait remise en cause si le logiciel embarqué se révélait erroné et devait être remplacé.
L'utilisation d'environnements de développement de logiciels intégrant des outils d'aide à la vérification et à la validation (JAVA/JML, C#/SPEC#, C/ACSL, Atelier B, Scade, Esterel, etc.) va se généraliser et, dans cette perspective, les futurs utilisateurs devront maîtriser ces outils autant que les techniques sous-jacentes.
À la base des techniques de vérification, la logique de Hoare est au cœur de cet ouvrage.
On trouvera ici comment utiliser cette méthode pour vérifier et concevoir des logiciels sûrs.
L'auteur montre également comment modéliser des systèmes informatiques dans le paradigme logico-ensembliste, puis comment les vérifier et les tester en recourant aux outils de la méthode B.
Divisé en deux parties, ce manuel contient une introduction didactique des principes fondamentaux de la technique de vérification par application des règles de la logique de Hoare.
