Αυτόματος Τυχαίος Έλεγχος Συστημάτων Με Εσωτερική Κατάσταση Βάσει Μοντέλου

Abstract

To PropEr είναι ένα εργαλείο ανοιχτού λογισμικού για τον αυτόματο τυχαίο έλεγχο ιδιοτήτων συναρτήσεων, γραμμένων στη γλώσσα Erlang, από τις προδιαγραφές τους. Αρχικά ήτανεπικεντρωμένο στον έλεγχο αγνών συναρτήσεων. Ωστόσο, οι εφαρμογές που υλοποιούνται σε Erlang συνήθως αποτελούνται από κώδικα με εσωτερική κατάσταση. Στην παρούσαδιπλωματική εργασία, έχουμε επεκτείνει το PropEr με δύο βιβλιοθήκες που υποστηρίζουν τον τυχαίο έλεγχο συστημάτων με εσωτερική κατάσταση βάσει μοντέλου. Ο χρήστης καλείται ναπροσδιορίσει ένα μοντέλο της συμπεριφοράς του συστήματος υπό έλεγχο. Δεδομένου αυτού του μοντέλου, ελέγχουμε ένα σύστημα παράγοντας και εκτελώντας ακολουθίες κλήσεων προς αυτό, ενώ καταγράφουμε τις αποκρίσεις του ώστε να επιβεβαιώσουμε ότι το σύστημα παρουσιάζει την αναμενόμενη συμπεριφορά.Η πρώτη βιβλιοθήκη, που ονομάζεται proper_statem, έχει σχεδιαστεί για τον έλεγχο γενικευμένων εξυπηρετητών και άλλων συστημάτων των οποίων η διεπαφή παρουσιάζει εσωτερικήκατάσταση. Οι παρενέργειες των συστημάτων προσδιορίζονται μέσω μίας αφηρημένης μηχανής κατάστασης. Η ίδια μηχανή κατάστασης μπορεί επίσης να χρησιμοποιηθεί για την παραγωγήακολουθιών κλήσεων, οι οποίες θα εκτελεστούν παράλληλα για τον εντοπισμό συνθηκών ανταγωνισμού. Η δεύτερη βιβλιοθήκη, που ονομάζεται proper_fsm, προσφέρεται για τον έλεγχο συστημάτων που παρουσιάζουν συμπεριφορά μηχανής πεπερασμένης κατάστασης, αφού είναι σχεδιασμένη ώστε να φέρνει την περιγραφή του μοντέλου του συστήματος πολύ κοντά σε ένα διάγραμμα κατάστασης. Ο προσδιορισμός ενός μοντέλου για το σύστημα υπό έλεγχο δεν είναι σε καμία περίπτωση τετριμμένη διαδικασία. Γι’αυτό το λόγο, παρουσιάζουμε λεπτομερή επεξηγηματικά παραδείγματα σχετικά με την αποτελεσματική χρήση των νέων βιβλιοθηκών για τον έλεγχο συστημάτων με εσωτερική κατάσταση.