Please use this identifier to cite or link to this item: http://artemis.cslab.ece.ntua.gr:8080/jspui/handle/123456789/17000
Full metadata record
DC FieldValueLanguage
dc.contributor.authorΖωή Παρασκευοπούλου
dc.date.accessioned2018-07-23T19:42:10Z-
dc.date.available2018-07-23T19:42:10Z-
dc.date.issued2014-9-9
dc.date.submitted2014-9-8
dc.identifier.urihttp://artemis-new.cslab.ece.ntua.gr:8080/jspui/handle/123456789/17000-
dc.description.abstractΠαρότι η τυχαία δοκιμή λογισμικού βασισμένη σε προδιαγραφές (randomproperty-based testing) είναι μια αποτελεσματική μέθοδος εύρεσηςσφαλμάτων και βελτίωσης της ποιότητας του λογισμικού, λάθη στηνδιαδικασία ελέγχου μπορεί να συγκαλύψουν σημαντικά σφάλματα στολογισμικό και να μειώσουν την αποτελεσματικότητα της μεθόδου. Στηδιπλωματική αυτή παρουσιάζουμε μια καινοτόμο μέθοδο που μας επιτρέπεινα επαληθεύσουμε τυπικά τις τεχνικές δοκιμής λογισμικού, την οποίαενσωματώνουμε στο εργαλείο QuickChick, το οποίο παρέχει τη δυνατότητααυτόματων δοκιμών βασισμένων σε προδιαγραφές για το εργαλείοδιαδραστικών αποδείξεων Coq. Ο στόχος της επέκτασης του εργαλείουείναι η τυπική απόδειξη ορθότητας του εκτελέσιμου κώδικα πουχρησιμοποιείται για τη δοκιμή λογισμικού αναφορικά με υψηλού επιπέδουπροδιαγραφές, οι οποίες αποτυπώνουν πιο άμεσα την υπό δοκιμήυπόθεση. Προκειμένου να επιτευχθεί κάτι τέτοιο παρέχουμε τη δυνατότητατυπικής απόδειξης ορθότητας για γεννήτορες τυχαίων δεδομένωναντιστοιχίζοντας τους στα σύνολα των τιμών που έχουν μη μηδενικήπιθανότητα να παραχθούν. Χρησιμοποιώντας την μεθοδολογία μαςαποδείξαμε την ορθότητα των περισσότερων συνδυαστών που παρέχονται απότην διεπαφή του εργαλείου QuickChick, έχοντας ως αναφορά έναν μικρόαριθμό αυτών για τους οποίους ορίσαμε τη σημασιολογία τουςαξιωματικά. Τέλος, αξιολογήσαμε την προτεινόμενη μεθοδολογία μέσα απόέναν αριθμό μη τετριμμένων περιπτώσεων εφαρμογής της και δείξαμε ότιμπορεί να κλιμακωθεί σε δοκιμές σύνθετων συστημάτων χωρίς νααπαιτούνται αλλαγές σε ήδη υπάρχοντα κώδικα.
dc.languageEnglish
dc.subjectsoftware testing
dc.subjectproperty-based testing
dc.subjectverification
dc.subjecttest data generation
dc.subjectproof assistants
dc.subjectcoq
dc.titleΑνάπτυξη Εργαλείου Για Την Επαλήθευση Δοκιμών Βασισμένων Σε Προδιαγραφές
dc.typeDiploma Thesis
dc.description.pages75
dc.contributor.supervisorΠαπασπύρου Νικόλαος
dc.departmentΤομέας Τεχνολογίας Πληροφορικής & Υπολογιστών
dc.organizationΕΜΠ, Τμήμα Ηλεκτρολόγων Μηχανικών & Μηχανικών Υπολογιστών
Appears in Collections:Διπλωματικές Εργασίες - Theses

Files in This Item:
File SizeFormat 
DT2014-0240.pdf357.56 kBAdobe PDFView/Open


Items in Artemis are protected by copyright, with all rights reserved, unless otherwise indicated.