Raisonnement continu

Le raisonnement continu (ou continuous reasoning, CR) est une méthodologie de raisonnement automatisé qui exploite la compositionnalité pour analyser les systèmes à grande échelle de manière différentielle. Le raisonnement continu se concentre sur l'analyse des derniers changements introduits dans le système et sur la réutilisation des résultats d'analyse précédents autant que possible. Le but du raisonnement continu est de contenir la complexité de calcul élevée des problèmes à grande échelle en résolvant des instances plus petites des problèmes à résoudre, c'est-à-dire en résolvant des instances qui considèrent principalement ce qui a changé dans le système depuis le dernier analyse effectuée.

Le raisonnement continu a été proposé pour la première fois par O'Hearn [1] en 2018 et a particulièrement réussi à soutenir le développement itératif de logiciels dans les grandes entreprises informatiques grâce à l'utilisation d'outils de raisonnement automatisé tels que Facebook's Infer [2],[3] et Amazon s2n [4] . Ces outils effectuent une analyse statique incrémentale [5] sur des bases de code volumineuses, en se concentrant uniquement sur les différences entre une modification et une autre, pour identifier les erreurs éventuelles ou les problèmes de sécurité avant la mise en production du code. Récemment, l'utilisation du raisonnement continu a également été proposée pour la gestion d'applications sur des infrastructures de Fog computing [6] .

Références

  1. (en) Peter W. O'Hearn, « Continuous Reasoning: Scaling the impact of formal methods », Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, ACM, , p. 13–25 (DOI 10.1145/3209108.3209109, lire en ligne, consulté le )
  2. (en) Dino Distefano, Manuel Fähndrich et Francesco Logozzo, « Scaling static analyses at Facebook », Communications of the ACM, vol. 62, no 8, , p. 62–70 (DOI 10.1145/3338112, lire en ligne, consulté le )
  3. (en) Cristiano Calcagno, Dino Distefano et Jeremy Dubreil, « Moving Fast with Software Verification », NASA Formal Methods, Springer International Publishing, , p. 3–11 (DOI 10.1007/978-3-319-17524-9_1, lire en ligne, consulté le )
  4. Andrey Chudnov, Nathan Collins et Byron Cook, Computer Aided Verification, vol. 10982, Springer International Publishing, , 430–446 p. (ISBN 978-3-319-96141-5, DOI 10.1007/978-3-319-96142-2_26, lire en ligne)
  5. (en) Helmut Seidl, Julian Erhard et Ralf Vogler, From Lambda Calculus to Cybersecurity Through Program Analysis, vol. 12065, Springer International Publishing, , 132–148 p. (ISBN 978-3-030-41102-2, DOI 10.1007/978-3-030-41103-9_5, lire en ligne)
  6. Forti, Stefano et Brogi, Antonio, « Continuous Reasoning for Managing Next-Gen Distributed Applications », Proceedings of the 36th International Conference on Logic Programming (ICLP) Technical Communications, EPTCS, vol. 325, , p. 164–177 (lire en ligne)
  • Portail de l’informatique
Cet article est issu de Wikipedia. Le texte est sous licence Creative Commons - Attribution - Partage dans les Mêmes. Des conditions supplémentaires peuvent s'appliquer aux fichiers multimédias.