ΠΥΞΙΔΑ Ιδρυματικό Αποθετήριο
και Ψηφιακή Βιβλιοθήκη
Συλλογές :

Τίτλος :Παραγωγή Δεδομένων Ελέγχου με Συμβολική - Concolic Εξέταση και Έλεγχο Μοντέλου
Δημιουργός :Καλλία, Μαρία
Συντελεστής :Μαλεύρης, Νικόλαος (Επιβλέπων καθηγητής)
Εκδότης :Οικονομικό Πανεπιστήμιο Αθηνών
Τύπος :Text
Φυσική περιγραφή :103σ.
Γλώσσα :el
Βιβλιογραφική Σημείωση :Βιβλιογραφία : σ. 101-103
Περίληψη :Ο έλεγχος του λογισμικού, είναι μία από τις κυρίες τεχνικές που συνεισφέρουν στηνυψηλή αξιοπιστία και ποιότητα του λογισμικού. Είναι η κύρια μέθοδος για την εμπέδωση τηςεμπιστοσύνης στο λογισμικό. Παρόλα αυτά, είναι μία δαπανηρή και χρονοβόρα διαδικασία,για αυτό και η αυτοματοποίηση των διαδικασιών του κρίνεται αναγκαία. Η αυτοματοποίησητου ελέγχου δεν θα μείωνε μόνο το κόστος της ανάπτυξης του λογισμικού αλλά θα αύξανετην αξιοπιστία των διαδικασιών του και θα βελτίωνε την ποιότητα του λογισμικού.Σε αυτή τη διπλωματική εργασία θα παρουσιαστεί το πρόβλημα της παραγωγήςδεδομένων ελέγχου για τα προγράμματα που περιλαμβάνουν απλές και πολύπλοκες δομέςδεδομένων και θα παρουσιαστεί ένα πλαίσιο για την αυτοματοποιημένη παραγωγήδεδομένων ελέγχου με την χρήση της συμβολικής εκτέλεσης και της concolic εκτέλεσης γιατην παραγωγή δεδομένων ελέγχου για τη μέθοδο των μεταλλάξεων και για την κάλυψη τουκριτηρίου των κλάδων(branch testing).Η κύρια πρόκληση στην περιοχή αυτή είναι το πώς θα γίνει αποτελεσματική παραγωγήδεδομένων ελέγχου που θα εξασφαλίσει υψηλό ποσοστό κάλυψης του κώδικα. Θαπαρουσιαστεί πως η συμβολική εκτέλεση, η concolic εκτέλεση και ο έλεγχος μοντέλουμπορούν να χρησιμοποιηθούν για την αυτοματοποιημένη παραγωγή δεδομένων ελέγχου γιατην κάλυψη του εκάστοτε κριτηρίου.Οι τεχνικές για την αυτοματοποιημένη παραγωγή δεδομένων ελέγχου για πολύπλοκεςδομές δεδομένων βασίζονται στον έλεγχο μοντέλου που χρησιμοποιεί αντιστοίχησηκαταστάσεων(state matching) για την αποφυγή της παραγωγής περιττών δεδομένων ελέγχου.Οι εξαντλητικές τεχνικές χρησιμοποιούν έλεγχο μοντέλων με λεπτομερή(explicit) ήσυμβολική εκτέλεση για την αναζήτηση όλων των πιθανών ακολουθιών ελέγχου μέχρι ένακαθορισμένο μέγεθος εισόδου. Οι lossy τεχνικές βασίζονται σε αντιστοιχήσεις καταστάσεωνμε χρήση αφαίρεσης(abstraction) για τον υπολογισμό και την αποθήκευση αφηρημένωνεκδόσεων των καταστάσεων. Αναζητάνε κάτω από προσεγγίσεις όλες τις πιθανές ακολουθίεςελέγχου.Επιπλέον, θα παρουσιαστεί το εργαλείο Java Pathfinder, ένας ελεγκτής μοντέλουκαταστάσεων για προγράμματα της γλώσσας java, το οποίο υλοποιεί τις τεχνικές πουαναφέρθηκαν και το οποίο επεκτείνετε και χρησιμοποιείται για την παραγωγή τωνπειραματικών αποτελεσμάτων που παρουσιάζονται στην ενότητα 8 της παρούσαςδιπλωματικής εργασίας. Επιπρόσθετα, θα παρουσιαστεί ο τρόπος με τον οποίοχρησιμοποιήθηκε η concolic εκτέλεση καθώς και συγκεκριμένες βελτιώσεις που έγιναν γιανα αυξηθεί η αποδοτικότητά της τεχνικής κυρίως σε ότι αφορά στην παραγωγή δεδομένωνελέγχου για τη μέθοδο των μεταλλάξεων.Τέλος, στην ενότητα 8 παρουσιάζονται τα πειράματα που διεξήχθησαν, τα οποίαδιακρίνονται (χωρισμένα) σε τρεις κατηγορίες. Η πρώτη κατηγορία πειραμάτων έχει σανσκοπό την ανεύρεση δεδομένων ελέγχου για branch testing, με χρήση της συμβολικής αλλάκαι της concolic εκτέλεσης. Η δεύτερη κατηγορία πειραμάτων αναφέρεται σε προγράμματαμε πολύπλοκες δομές δεδομένων όπου ο στόχος είναι η παραγωγή ακολουθιών ελέγχου είτεμε τη χρήση εξαντλητικών τεχνικών είτε με lossy. Τέλος, η τρίτη κατηγορία πειραμάτωναναφέρεται στην παραγωγή δεδομένων ελέγχου για τη μέθοδο των μεταλλάξεων, στην οποίαχρησιμοποιείται τόσο η συμβολική όσο και η concolic εκτέλεση μαζί με τις βελτιώσεις πουέχουν προταθεί.
Λέξη κλειδί :Λογισμικό
Σχεδίαση λογισμικού
Αυτοματοποίηση
Computer programs
Software engineering
Automation
Ημερομηνία έκδοσης :2010

Αρχείο: Kallia_2010.pdf

Τύπος: application/pdf