Bounded Verification of Software Models: Challenges and Opportunities

Resum

Assegurar l’absència d’errades en un sistema software és un problema important però també un repte. La detecció ràpida d’errors dins el procés de desenvolupament de software redueix els costos de detectar i corregir els defectes. Així doncs, l’anàlisi de models pot incrementar la qualitat final del software i reduir els costos de desenvolupament.

Una línia de recerca prometedora en aquest camp és l’us de solvers de satisfactibilitat booleana (SAT) o programació amb restriccions (CP) per realitzar verificació afitada. La verificació afitada consisteix en comprovar formalment l’absència d’errades dins d’un espai finit definit com a paràmetre de l’anàlisi. Aquest tipus d’anàlisi és usualment ràpid a la pràctica i proporciona un feedback valuós. En qualsevol cas, la seva complexitat computacional és elevada en general i no ofereix resultats concloents fora del rang de verificació definit com a paràmetre.

En aquest article, discutim tendències recents i resultats en l’aplicació de verificació afitada a un camp específic dins de l’enginyeria del software : l’anàlisi de models d’un sistema software. A més, discutim contribucions prometedores que poden ampliar el treball previ per millorar la seva aplicabilitat pràctica dins la indústria del software.