Quantitative architecture styles
Authors: Παραπονιάρη Παυλίνα 
Published: July 2024

Οι αρχιτεκτονικές λογισμικού είναι σημαντικές για το σχεδιασμό και την ανάπτυξη πολύπλοκων συστημάτων λογισμικού. Για να μπορούν τα συστήματα να λειτουργούν ικανοποιώντας τις ιδιότητές τους θα πρέπει να βασίζονται σε μια σωστή αρχιτεκτονική λογισμικού. Οι αρχιτεκτονικές έχουν ποιοτικά και ποσοτικά χαρακτηριστικά. Τα ποιοτικά χαρακτηριστικά αφορούν κυρίως τον τρόπο αλληλεπίδρασης των συνιστωσών της αρχιτεκτονικής, ενώ τα ποσοτικά χαρακτηριστικά είναι για παράδειγμα το κόστος υλοποίησης ή ακόμα ο βαθμός αβεβαιότητας των αλληλεπιδράσεων. Ένα μεγάλο κομμάτι της βιβλιογραφίας ασχολείται κυρίως με την περιγραφή μόνο των ποιοτικών χαρακτηριστικών των αρχιτεκτονικών. Ωστόσο, μια αρχιτεκτονική είναι αντιπροσωπευτική ενός συστήματος όταν περιγράφει τόσο τα ποιοτικά όσα και τα ποσοτικά χαρακτηριστικά του. Επιπλέον κάποιες βασικές προϋποθέσεις ώστε οι αρχιτεκτονικές λογισμικού να μπορούν να περιγράφουν αποτελεσματικά τα συστήματα με τα χαρακτηριστικά τους, αποτελούν οι ακόλουθες. Αρχικά, να είναι σωστές από κατασκευής (correctness-by-construction) και επίσης φιλικές ως προς τους ενδιαφερόμενους ώστε να μπορούν να κατανοούν και να αναλύουν τον τρόπο αλληλεπίδρασης των συνιστωσών του συστήματος. Στην διατριβή αυτή, ασχολούμαστε με τα ζητήματα που αναφέραμε, και άλλα, μελετώντας λογικές με βάρη που είναι σε θέση να περιγράφουν αρχιτεκτονικές λογισμικού με ποιοτικά και ποσοτικά χαρακτηριστικά. Οι λογικές είναι ένα πολύ χρήσιμο εργαλείο για την τυπική περιγραφή των αρχιτεκτονικών λογισμικού διασφαλίζοντας την ορθότητα από κατασκευής της αρχιτεκτονικής. Προτείνουμε τρεις ποσοτικές λογικές οι οποίες μπορούν να περιγράψουν μια σειρά από ποσοτικά χαρακτηριστικά αρχιτεκτονικών. Για τις λογικές μας, θεωρούμε ότι κάθε αλληλεπίδραση σε μια αρχιτεκτονική έχει βάρος. Αυτό το βάρος μπορεί να αντιπροσωπεύει το κόστος, την πιθανότητα, την αβεβαιότητα ή ακόμα και τον χρόνο που απαιτείται για την υλοποίηση της αλληλεπίδρασης. Πρώτον, εισάγουμε και διερευνούμε τη ποσοτική προτασιακή λογική διαμόρφωσης με τιμές σε ένα αντιμεταθετικό ημιδακτύλιο. Η λογική αυτή μπορεί να περιγράψει αρχιτεκτονικές λογισμικού με ποσοτικά χαρακτηριστικά όπως το μέγιστο (ή το ελάχιστο) κόστος, την πιθανότητα ή τον χρόνο που απαιτούν οι αλληλεπιδράσεις της αρχιτεκτονικής. Δεδομένης μιας αρχιτεκτονικής όπου οι αλληλεπιδράσεις της είναι με βάρη, μπορούμε να κατασκευάσουμε έναν ποσοτικό τύπο της λογικής αυτής, ο οποίος περιγράφει τον τρόπο αλληλεπίδρασης των συνιστωσών με τα αντίστοιχα βάρη τους. Επιπλέον, δείχνουμε ότι μπορούμε να υπολογίσουμε όλες τις πιθανές αλληλεπιδράσεις της αρχιτεκτονικής. Με άλλα λόγια, μπορούμε να υπολογίσουμε όλους τους πιθανούς τρόπους με τους οποίους οι συνιστώσες της αρχιτεκτονικής μπορούν να αλληλεπιδράσουν ώστε να ικανοποιούν τις ποιοτικές και ποσοτικές ιδιότητές της. Ως πρώτο και κύριο αποτέλεσμα αυτής της λογικής, αποδεικνύουμε ότι για κάθε ποσοτικό τύπο μπορούμε να κατασκευάσουμε αποτελεσματικά, σε διπλά εκθετικό χρόνο, τον ισοδύναμό του τύπο σε πλήρη κανονική μορφή. Λόγω αυτού του αποτελέσματος, δύο ποσοτικοί τύποι είναι ισοδύναμοι αν και μόνο αν έχουν την ίδια πλήρη κανονική μορφή. Συνεπώς, δεν χρειάζεται να ελέγξουμε την ισότητα για όλα τα πιθανά σχήματα αλληλεπιδράσεων, παρά μόνο την κανονική τους μορφή. Ως εκ τούτου, το δεύτερο κύριο αποτέλεσμα αυτής της λογικής είναι ότι η ισοδυναμία των ποσοτικών τύπων αυτής είναι αποφασίσιμη. Επιπλέον, εισάγουμε την έννοια της ορθότητας (soundness) και ως τρίτο κύριο αποτέλεσμα δείχνουμε ότι η προαναφερθείσα λογική είναι ορθή (sound). Στη συνέχεια, χρησιμοποιώντας το σύστημα Maude, το οποίο είναι ένα σύστημα επανεγγραφής κανόνων λογικής, μπορούμε να υπολογίσουμε την πλήρη κανονική μορφή για κάθε ποσοτικό τύπο της λογικής με αυτοματοποιημένο τρόπο. Παρουσιάζουμε τον κώδικα με τους κανόνες επανεγγραφής της λογικής μας και τη απόδοση του κώδικα όταν εξετάζουμε ποσοτικούς τύπους που περιγράφουν γνωστές αρχιτεκτονικές. Όπως αναφέραμε, η λογική της ποσοτικής προτασιακής διαμόρφωσης σε ένα αντιμεταθετικό ημιδακτύλιο είναι σε θέση να χαρακτηρίσει τις αρχιτεκτονικές που έχουν συγκεκριμένα ποσοτικά χαρακτηριστικά. Ωστόσο, χαρακτηριστικά όπως το μέσο κόστος μιας αρχιτεκτονικής δεν μπορούν να χαρακτηριστούν με την προαναφερθείσα λογική. Αυτό οφείλεται στο γεγονός ότι η πράξη του μέσου όρου δεν μπορεί να εκφραστεί από την αλγεβρική δομή των αντιμεταθετικών ημιδακτυλίων. Μια δομή που μπορεί να εκφράσει αυτή τη πράξη είναι αυτή των product valuation monoids. Συνεπώς, παρουσιάζουμε στην συνέχεια τη δεύτερη ποσοτική λογική, η οποία είναι μια ποσοτική προτασιακή λογική διαμόρφωσης σε ένα product valuation monoid. Αυτή η λογική είναι ικανή να περιγράφει αρχιτεκτονικές λογισμικού με ποσοτικά χαρακτηριστικά όπως ο μέσος όρος του κόστους των αλληλεπιδράσεων της αρχιτεκτονικής και το μέγιστο κόστος μεταξύ όλων των δαπανών που εμφανίζονται συχνότερα σε έναν συγκεκριμένο αριθμό συνιστωσών της αρχιτεκτονικής. Παρουσιάζουμε ποσοτικούς τύπους της λογικής αυτής που περιγράφουν γνωστές αρχιτεκτονικές εξοπλισμένες με ποσοτικά χαρακτηριστικά. Επιπλέον, αποδεικνύουμε ότι μπορούμε να κατασκευάσουμε αποτελεσματικά την πλήρη κανονική μορφή των ποσοτικών τύπων. Με την βοήθεια αυτού του αποτελέσματος αποδεικνύουμε ότι το πρόβλημα της ισοδυναμίας των ποσοτικών τύπων της λογικής είναι αποφασίσιμο. Τέλος, παρουσιάζουμε και διερευνούμε την τρίτη ποσοτική λογική της διατριβής αυτής που είναι η λογική της ασαφούς προτασιακής διαμόρφωσης. Αυτή η λογική είναι σε θέση να χαρακτηρίσει ποσοτικά χαρακτηριστικά όπου οι άλλες ποσοτικές λογικές που παρουσιάσαμε δεν μπορούν. Αυτά τα χαρακτηριστικά είναι ο βαθμός της αβεβαιότητας και αξιοπιστίας των αλληλεπιδράσεων μιας αρχιτεκτονικής. Για αυτά τα χαρακτηριστικά θεωρούμε ότι οι ασαφείς λογικές (fuzzy logic) αποτελούν κατάλληλο εργαλείο για να μπορέσουμε να εκφράσουμε την αβεβαιότητα στις αρχιτεκτονικές. Τα αποτελέσματα της λογικής αυτής είναι τα ακόλουθα. Παρουσιάζουμε τη σύνταξη και σημασιολογία αυτής της ποσοτικής λογικής, η οποία είναι μια ποσοτική προτασιακή λογική διαμόρφωσης σε μια De Morgan άλγεβρα. Κατασκευάζουμε ποσοτικούς τύπους που χαρακτηρίζουν γνωστές αρχιτεκτονικές στις οποίες θεωρούμε ότι οι αλληλεπιδράσεις τους έχουν κάποιο βαθμό αβεβαιότητας. Στη συνέχεια, ασχολούμαστε με το πρόβλημα της ισοδυναμίας των τύπων της λογικής μας. Αρχικά, δείχνουμε ότι κάθε ποσοτικός τύπος μπορεί να γραφεί σε κανονική μορφή σε εκθετικό χρόνο. Στη συνέχεια, αποδεικνύουμε ότι το πρόβλημα της ισοδυναμίας των ποσοτικών τύπων σε μια τυχαία De Morgan άλγεβρα είναι αποφασίσιμο σε εκθετικό χρόνο. Τέλος, ασχολούμαστε με τύπους που δεν είναι ισοδύναμοι σε μια τυχαία De Morgan άλγεβρα αλλά μόνο σε συγκεκριμένες όπως η Kleene και η Boolean άλγεβρα. Τέλος, αποδεικνύουμε ότι για κάθε ποσοτικό τύπο σε μια Kleene άλγεβρα (αντίστοιχα σε μια άλγεβρα του Boole) μπορούμε να κατασκευάσουμε αποτελεσματικά τον ισοδύναμο ποσοτικό τύπο του σε κανονική μορφή. Ως εκ τούτου, το πρόβλημα ισοδυναμίας των ποσοτικών τύπων στις προαναφερθείσες De Morgan άλγεβρες είναι επίσης αποφασίσιμο.