1. Home page
  2. Search

A Coq Framework for Verified Property-Based Testing

This item is provided by the institution :
National Technical University of Athens   

Repository :
Digital Library of National Technical University of Athens | Dspace@NTUA   

see the original item page
in the repository's web site and access all digital files if the item*



Ανάπτυξη Εργαλείου για την Επαλήθευση Δοκιμών Βασισμένων σε Προδιαγραφές (EL)
A Coq Framework for Verified Property-Based Testing (EN)
Παρασκευοπούλου, Ζωή Α. (EL)
Paraskevopoulou, Zoi A. (EN)
Σαγώνας, Κωστής (EL)
Σμαραγδάκης, Ιωάννης (EL)
Παπασπύρου, Νικόλαος (EL)
bachelorThesis
2014-12-11T10:49:52Z
2014-09-08
2014-12-11
Παρότι η τυχαία δοκιμή λογισμικού βασισμένη σε προδιαγραφές (random property-based testing) είναι μια αποτελεσματική μέθοδος εύρεσης σφαλμάτων και βελτίωσης της ποιότητας του λογισμικού, λάθη στην διαδικασία ελέγχου μπορεί να συγκαλύψουν σημαντικά σφάλματα στο λογισμικό και να μειώσουν την αποτελεσματικότητα της μεθόδου. Στη διπλωματική αυτή παρουσιάζουμε μια καινοτόμο μέθοδο που μας επιτρέπει να επαληθεύσουμε τυπικά τις τεχνικές δοκιμής λογισμικού, την οποία ενσωματώνουμε στο εργαλείο QuickChick, το οποίο παρέχει τη δυνατότητα αυτόματων δοκιμών βασισμένων σε προδιαγραφές για το εργαλείο διαδραστικών αποδείξεων Coq. Ο στόχος της επέκτασης του εργαλείου είναι η τυπική απόδειξη ορθότητας του εκτελέσιμου κώδικα που χρησιμοποιείται για τη δοκιμή λογισμικού αναφορικά με υψηλού επιπέδου προδιαγραφές, οι οποίες αποτυπώνουν πιο άμεσα την υπό δοκιμή υπόθεση. Προκειμένου να επιτευχθεί κάτι τέτοιο παρέχουμε τη δυνατότητα τυπικής απόδειξης ορθότητας για γεννήτορες τυχαίων δεδομένων αντιστοιχίζοντας τους στα σύνολα των τιμών που έχουν μη μηδενική πιθανότητα να παραχθούν. Χρησιμοποιώντας την μεθοδολογία μας αποδείξαμε την ορθότητα των περισσότερων συνδυαστών που παρέχονται από την διεπαφή του εργαλείου QuickChick, έχοντας ως αναφορά έναν μικρό αριθμό αυτών για τους οποίους ορίσαμε τη σημασιολογία τους αξιωματικά. Τέλος, αξιολογήσαμε την προτεινόμενη μεθοδολογία μέσα από έναν αριθμό μη τετριμμένων περιπτώσεων εφαρμογής της και δείξαμε ότι μπορεί να κλιμακωθεί σε δοκιμές σύνθετων συστημάτων χωρίς να απαιτούνται αλλαγές σε ήδη υπάρχοντα κώδικα. (EL)
Ζωή Παρασκευοπούλου (EL)
75 σ. (EL)
While random property-based testing is often an effective way for quickly finding bugs and increasing software quality, testing errors can conceal important bugs and thus reduce its benefits. In this thesis we introduce a novel methodology for formally verified property-based testing; this methodology is embodied by a framework built on top of the QuickChick testing plugin for Coq. Our verification framework is aimed at proving the correctness of executable testing code with respect to a high-level specification, which captures the conjecture under test in a more direct way. To this end, we provide a systematic way for reasoning about the set of values a random data generator can produce with non-zero probability. We have used our methodology to prove the correctness of most QuickChick combinators, with respect to the axiomatic semantics of a small number of primitive ones. We have evaluated our verification methodology on two sizable case studies showing that it is modular, scalable, and requires minimal changes to existing code. (EN)
Επαλήθευση (EL)
Παραγωγή δεδομένων δοκιμής (EL)
Δοκιμή λογισμικού (EL)
Δοκιμή βασισμένη σε προδιαγραφές (EL)
Εργαλείο διαδραστικών αποδείξεων (EL)
Software testing (EN)
Coq (EN)
Proof assistants (EN)
Property-based testing (EN)
Verification (EN)
Test data generation (EN)
Εθνικό Μετσόβιο Πολυτεχνείο. Σχολή Ηλεκτρολόγων Μηχανικών και Μηχανικών Υπολογιστών. Τομέας Τεχνολογίας Πληροφορικής και Υπολογιστών. Εργαστήριο Τεχνολογίας Λογισμικού. (EL)
ETDFree-policy.xml (EN)
National Technical University of Athens
Digital Library of National Technical University of Athens | Dspace@NTUA
Κεντρική Βιβλιοθήκη Ε.Μ.Π.
Ιδρυματικό Αποθετήριο
Διπλωματικές Εργασίες



*Institutions are responsible for keeping their URLs functional (digital file, item page in repository site)