Vérification statique étendue - Extended static checking
La vérification statique étendue ( ESC ) est un nom collectif en informatique pour une gamme de techniques permettant de vérifier statiquement l'exactitude de diverses contraintes de programme. ESC peut être considéré comme une forme étendue de vérification de type . Comme pour la vérification de type, ESC est exécuté automatiquement au moment de la compilation (c'est-à-dire sans intervention humaine). Cela le distingue des approches plus générales de la vérification formelle des logiciels, qui reposent généralement sur des preuves générées par l'homme. En outre, il favorise la praticité par rapport à la solidité, en ce sens qu'il vise à réduire considérablement le nombre de faux positifs (erreurs surestimées qui ne sont pas des erreurs réelles, c'est-à-dire ESC sur la rigueur) au prix de l'introduction de certains faux négatifs (erreur réelle de sous-estimation ESC, mais qui ne nécessitent pas l'attention du programmeur, ou ne sont pas ciblés par ESC). ESC peut identifier une gamme d'erreurs qui sont actuellement en dehors de la portée d'un vérificateur de type, y compris la division par zéro , le tableau hors limites , le débordement d'entier et les déréférencements nuls .
Les techniques utilisées dans la vérification statique étendue proviennent de divers domaines de l' informatique , y compris l'analyse de programme statique , la simulation symbolique , la vérification de modèle , l'interprétation abstraite , la résolution SAT et la démonstration automatisée de théorèmes et la vérification de type . La vérification statique étendue est généralement effectuée uniquement à un niveau intraprocédural (plutôt qu'interprocédural) afin de s'adapter à de grands programmes. De plus, la vérification statique étendue vise à signaler les erreurs en exploitant les spécifications fournies par l'utilisateur, sous la forme de pré- et post-conditions , d' invariants de boucle et d' invariants de classe .
Les vérificateurs statiques étendus fonctionnent généralement en propageant les postconditions les plus fortes (resp. les préconditions les plus faibles ) de manière intraprocédurale via une méthode commençant à partir de la précondition (resp. postcondition). À chaque point de ce processus, une condition intermédiaire est générée qui capture ce qui est connu à ce point du programme. Ceci est combiné avec les conditions nécessaires de l'instruction de programme à ce stade pour former une condition de vérification . Un exemple de ceci est une déclaration impliquant une division, dont la condition nécessaire est que le diviseur soit différent de zéro. La condition de vérification qui en découle énonce effectivement : étant donné la condition intermédiaire à ce stade, il doit s'ensuivre que le diviseur est non nul . Toutes les conditions de vérification doivent être fausses (donc correctes au moyen d'un tiers exclu ) pour qu'une méthode réussisse la vérification statique étendue (ou "incapable de trouver plus d'erreurs"). Typiquement, une certaine forme de prouveur de théorème automatisé est utilisée pour décharger les conditions de vérification.
La vérification statique étendue a été lancée dans ESC/Modula-3 et, plus tard, ESC/Java . Ses racines proviennent de techniques de vérification statique plus simplistes, telles que le débogage statique ou Lint (logiciel) et FindBugs . Un certain nombre d'autres langages ont adopté ESC, notamment Spec# et SPARKada et VHDL VSPEC. Cependant, il n'existe actuellement aucun langage de programmation logiciel largement utilisé qui offre une vérification statique étendue dans son environnement de développement de base.
Voir également
Les références
Lectures complémentaires
- Cormac Flanagan; K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, Raymie Stata (2002). Vérification statique étendue pour Java . Actes de la Conférence sur la conception et la mise en œuvre des langages de programmation (PLDI) . p. 234. doi : 10.1145/512529.512558 . ISBN 978-1581134636.CS1 maint : plusieurs noms : liste des auteurs ( lien )
- Babic, Domagoj; Hu, Alan J. (2008). Calysto : Vérification statique étendue évolutive et précise . Actes de la Conférence internationale sur le génie logiciel (ICSE) . p. 211. doi : 10.1145/1368088.1368118 . ISBN 9781605580791.
- Échecs, BV (2002). Amélioration de la sécurité informatique grâce à la vérification statique étendue . Actes du Symposium IEEE sur la sécurité et la confidentialité . 160-173. CiteSeerX 10.1.1.15.2090 . doi : 10.1109/SECPRI.2002.1004369 . ISBN 978-0-7695-1543-4.
- Rioux, Frédéric ; Chalin, Patrice (2006). "Améliorer la qualité des applications d'entreprise basées sur le Web avec la vérification statique étendue : une étude de cas" . Notes électroniques en informatique théorique . 157 (2) : 119-132. doi : 10.1016/j.entcs.2005.12.050 . ISSN 1571-0661 .
- James, Perry R.; Chalin, Patrice (2009). "Vérification statique étendue plus rapide et plus complète pour le langage de modélisation Java". Journal de raisonnement automatisé . 44 (1–2) : 145-174. CiteSeerX 10.1.1.165.7920 . doi : 10.1007/s10817-009-9134-9 . ISSN 0168-7433 .
- Xu, Dana N. (2006). Vérification statique étendue pour haskell . Actes de l'atelier ACM sur Haskell . p. 48. CiteSeerX 10.1.1.377.3777 . doi : 10.1145/1159842.1159849 . ISBN 978-1595934895.
- Leino, K. Rustan M. (2001). Vérification statique étendue : une perspective sur dix ans . Informatique . Notes de cours en informatique. 2000 . p. 157–175. doi : 10.1007/3-540-44577-3_11 . ISBN 978-3-540-41635-7.
- Detlefs, David L.; Leino, K. Rustan M.; Nelson, Greg ; Saxe, James B. (1998). "Vérification statique étendue". Rapport de recherche Compaq SRC (159).