Raționament continuu
Raționamentul continuu (sau raționamentul continuu , CR) este o metodologie de raționament automat care exploatează compoziționalitatea pentru a analiza sistemele la scară largă într-un mod diferențial. Raționamentul continuu se concentrează pe analiza ultimelor modificări introduse în sistem și reutilizarea rezultatelor analizei anterioare cât mai mult posibil. Scopul raționamentului continuu este de a conține complexitatea de calcul ridicată a problemelor pe sisteme la scară largă prin rezolvarea unor instanțe mai mici ale problemelor care trebuie rezolvate, adică prin rezolvarea unor instanțe care iau în considerare în principal ceea ce s-a schimbat în sistem de la ultima analiză efectuată.
Raționamentul continuu a fost propus pentru prima dată de O'Hearn [1] în 2018 și a avut un succes deosebit în susținerea dezvoltării software iterative în companiile IT mari, cu ajutorul instrumentelor de raționament automatizate, cum ar fi Infer [2] [3] și Amazon s2n de Facebook [4] ] . Aceste instrumente efectuează analize statice incrementale [5] pe baze de coduri mari, concentrându-se doar pe diferențele dintre modificări, pentru a identifica posibile erori sau probleme de securitate înainte de introducerea codului în producție. Recent, s-a propus utilizarea raționamentului continuu și pentru gestionarea aplicațiilor pe infrastructurile de calcul Fog [6] .
Notă
- ^ (EN) Peter W. O'Hearn, Raționament continuu: Scalarea impactului metodelor formale , în Proceedings of the 33rd Annual ACM / IEEE Symposium on Logic in Computer Science, ACM, 9 iulie 2018, pp. 13-25, DOI : 10.1145 / 3209108.3209109 . Adus la 30 septembrie 2020 .
- ^ (EN) Dino Distefano, Manuel Fähndrich și Francesco Logozzo, Scaling static analysis at Facebook , în Communications of the ACM, vol. 62, nr. 8, 24 iulie 2019, pp. 62-70, DOI : 10.1145 / 3338112 . Adus la 30 septembrie 2020 .
- ^ (EN) Cristiano Calcagno, Dino Distefano și Jeremy Dubreil, Moving Fast Software Verification with NASA Formal Methods, Springer International Publishing, 2015, pp. 3-11, DOI : 10.1007 / 978-3-319-17524-9_1 . Adus la 30 septembrie 2020 .
- ^ Andrey Chudnov, Nathan Collins și Byron Cook, Computer Aided Verification , vol. 10982, Editura Springer International, 2018, pp. 430–446, DOI : 10.1007 / 978-3-319-96142-2_26 , ISBN 978-3-319-96141-5 . Adus la 30 septembrie 2020 .
- ^ (EN) Helmut Seidl, Julian Erhard și Ralf Vogler,De la calculul Lambda la securitatea cibernetică prin analiza programului , vol. 12065, Editura Springer International, 2020, pp. 132–148, DOI : 10.1007 / 978-3-030-41103-9_5 , ISBN 978-3-030-41102-2 . Adus la 30 septembrie 2020 .
- ^ (EN) Strong, Stephen și Brogi, Antonio, Raționament continuu pentru gestionarea aplicațiilor distribuite de generația următoare , în Proceedings of the 36th Conference International on Logic Programming (ICLP) Technical Communications, EPTCS, vol. 325, 164–177, DOI : 10.4204 / EPTCS.325.22 .
