Quantitative architecture styles

Abstract

Software architectures are crucial in design and development of complex software systems. In order for the systems to work satisfying their properties they must be based on a proper software architecture. Software architectures have both qualitative and quantitative features. Qualitative features mainly concern the way the components in the architecture interact, whereas the quantitative features are for instance the implementation cost or also the degree of uncertainty of the interactions. Most work has been based on characterizing only the qualitative features of software architectures. However, a software architecture is considered to be more representative of a system, if it is able to characterize both qualitative and quantitative features. Yet another basic requirements for software architectures to describe efficiently software systems are to be correct-by-construction and helpful to stakeholders in understanding and analyzing the way the components interact. In this dissertation, we address these issues and more by studying weighted logics which are able to describe software architectures with quantitative features. Mathematical logics are a very useful tool for formally describing software architectures by ensuring correctness-by-construction. We propose three weighted logics where they can describe a range of quantitative features of architectures. For our logics, we consider that every interaction in an architecture has a weight. This weight can either represent the cost, the probability, the uncertainty, or the time needed of the implementation of the interaction. Firstly, we introduce and investigate a weighted propositional configuration logic over a commutative semiring. This logic is able to describe software architectures with quantitative features such as the maximum (or minimum) cost, the probability or time needed of the interactions in the architecture. Given an architecture with weighted interactions we are able to construct a weighted formula which is able to characterize the way the components interact among with their respectively weights. Moreover, we show that given this formula we can compute all possible interactions in the architecture. In other words, we can compute all possible architecture schemes. Our first main result of this logic is that we prove that for every weighted formula we can effectively construct, in doubly exponential time, its equivalent one in full normal form which is unique up to the equivalence relation. So we get that two weighted formulas being equivalent iff they have the same full normal form. Hence, we do not need to check equality for all possible models of the architectures. The second main result of this work states that the equivalence of two weighted formulas is decidable. Moreover, we introduce a notion of soundness, and as a third main result we show that the aforementioned logic is sound. Next, by using the Maude system, which is an implementation of rewriting logic, we accomplish to compute the full normal form of every weighted formula in an automated way. We present the code with rewriting rules of our logic and the time performance of the code when we consider weighted formulas formalizing well known architectures. As we mentioned, the weighted propositional configuration logic over commutative semirings is able to characterize architectures with specific quantitative features. However, features such as the average cost of an architecture cannot be characterized with the aforementioned logic. This is due to the fact that the average operation cannot be expressed by the algebraic structure of commutative semirings. A structure that is able to express this operation is the one of product valuation monoids. For this, we introduce our second weighted logic which is a weighted propositional configuration logic over product valuation monoids. This logic is intended to serve as a specification language for software architectures with quantitative features such as the average of all interactions' costs of the architecture and the maximum cost among all costs occurring most frequently within a specific number of components in an architecture. We provide weighted formulas of our logic which describe well-known architectures equipped with quantitative characteristics. Moreover, we prove an efficient construction of a full normal form which leads to decidability of equivalence of formulas in this logic. Lastly, we introduce and investigate our third weighted logic which is the fuzzy propositional configuration logic. This logic is able to characterize quantitative features where the other weighted logics we introduced cannot. Those features are the uncertainty and the reliability of the interactions in an architecture. For this, we consider that fuzzy logics constitute a suitable tool in order to deal with uncertainty. The contributions of this logic are the following. We introduce the syntax and semantics of this logic which is a weighted propositional configuration logic over De Morgan algebras. We construct weighted formulas characterizing known architectures employed with uncertainty in their interactions. Then, we deal with the decidability of equivalence of formulas in our logic. Firstly, we show that every formula can be written in normal form in exponential time. Then, we prove that the equivalence problem of weighted formulas over an arbitrary De Morgan algebra is decidable in exponential time. Lastly, we deal with formulas which are not equivalent over an arbitrary De Morgan algebra but only over specific ones such as the Kleene and the Boolean algebra. For this, we prove that for every weighted formula over a Kleene algebra (resp. a Boolean algebra) we can effectively construct its equivalent weighted formula in normal form. Hence, the equivalence problem of weighted formulas over the aforementioned De Morgan algebras is decidable.

Οι αρχιτεκτονικές λογισμικού είναι σημαντικές για το σχεδιασμό και την ανάπτυξη πολύπλοκων συστημάτων λογισμικού. Για να μπορούν τα συστήματα να λειτουργούν ικανοποιώντας τις ιδιότητές τους θα πρέπει να βασίζονται σε μια σωστή αρχιτεκτονική λογισμικού. Οι αρχιτεκτονικές έχουν ποιοτικά και ποσοτικά χαρακτηριστικά. Τα ποιοτικά χαρακτηριστικά αφορούν κυρίως τον τρόπο αλληλεπίδρασης των συνιστωσών της αρχιτεκτονικής, ενώ τα ποσοτικά χαρακτηριστικά είναι για παράδειγμα το κόστος υλοποίησης ή ακόμα ο βαθμός αβεβαιότητας των αλληλεπιδράσεων. Ένα μεγάλο κομμάτι της βιβλιογραφίας ασχολείται κυρίως με την περιγραφή μόνο των ποιοτικών χαρακτηριστικών των αρχιτεκτονικών. Ωστόσο, μια αρχιτεκτονική είναι αντιπροσωπευτική ενός συστήματος όταν περιγράφει τόσο τα ποιοτικά όσα και τα ποσοτικά χαρακτηριστικά του. Επιπλέον κάποιες βασικές προϋποθέσεις ώστε οι αρχιτεκτονικές λογισμικού να μπορούν να περιγράφουν αποτελεσματικά τα συστήματα με τα χαρακτηριστικά τους, αποτελούν οι ακόλουθες. Αρχικά, να είναι σωστές από κατασκευής (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 άλγεβρες είναι επίσης αποφασίσιμο.