Quantitative architecture styles
Creators: name: Παραπονιάρη, Παυλίνα Μ.
Publisher: name: Aristotle University of Thessaloniki
Year: 2024
Subjects: Αρχιτεκτονικές λογισμικού
Ποσοτική προτασιακή λογική διαμόρφωσης
Αποφασισιμότητα της ισοδυναμίας
Ασαφής λογική
Software architectures
Weighted propositional configuration logic
Decidability of equivalence
Fuzzy logic

description: Οι αρχιτεκτονικές λογισμικού είναι σημαντικές για το σχεδιασμό και την ανάπτυξη πολύπλοκων συστημάτων λογισμικού. Οι αρχιτεκτονικές έχουν ποιοτικά και ποσοτικά χαρακτηριστικά. Τα ποιοτικά χαρακτηριστικά αφορούν κυρίως τον τρόπο αλληλεπίδρασης των συνιστωσών της αρχιτεκτονικής, ενώ τα ποσοτικά χαρακτηριστικά είναι για παράδειγμα το κόστος υλοποίησης ή ακόμα ο βαθμός αβεβαιότητας των αλληλεπιδράσεων. Ένα μεγάλο κομμάτι της βιβλιογραφίας ασχολείται κυρίως με την περιγραφή μόνο των ποιοτικών χαρακτηριστικών των αρχιτεκτονικών. Στην διατριβή αυτή μελετούμε λογικές με βάρη που είναι σε θέση να περιγράφουν αρχιτεκτονικές λογισμικού με ποσοτικά χαρακτηριστικά. Προτείνουμε τρεις ποσοτικές λογικές οι οποίες μπορούν να περιγράψουν μια σειρά από ποσοτικά χαρακτηριστικά αρχιτεκτονικών. Πρώτον, εισάγουμε και διερευνούμε τη ποσοτική προτασιακή λογική διαμόρφωσης με τιμές σε ένα αντιμεταθετικό ημιδακτύλιο. Η λογική αυτή μπορεί να περιγράψει αρχιτεκτονικές λογισμικού με ποσοτικά χαρακτηριστικά όπως το μέγιστο (ή το ελάχιστο) κόστος, την πιθανότητα ή τον χρόνο που απαιτούν οι αλληλεπιδράσεις της αρχιτεκτονικής. Ως πρώτο και κύριο αποτέλεσμα αυτής της λογικής, αποδεικνύουμε ότι για κάθε ποσοτικό τύπο μπορούμε να κατασκευάσουμε αποτελεσματικά, σε διπλά εκθετικό χρόνο, τον ισοδύναμό του τύπο σε πλήρη κανονική μορφή. Ως εκ τούτου, το δεύτερο κύριο αποτέλεσμα αυτής της λογικής είναι ότι η ισοδυναμία των ποσοτικών τύπων αυτής είναι αποφασίσιμη. Στη συνέχεια, χρησιμοποιώντας το σύστημα Maude μπορούμε να υπολογίσουμε την πλήρη κανονική μορφή για κάθε ποσοτικό τύπο της λογικής με αυτοματοποιημένο τρόπο. Παρουσιάζουμε στην συνέχεια τη δεύτερη ποσοτική λογική, η οποία είναι μια ποσοτική προτασιακή λογική διαμόρφωσης σε ένα product valuation monoid. Αυτή η λογική είναι ικανή να περιγράφει αρχιτεκτονικές λογισμικού με ποσοτικά χαρακτηριστικά όπως ο μέσος όρος του κόστους των αλληλεπιδράσεων της αρχιτεκτονικής. Επιπλέον, αποδεικνύουμε ότι μπορούμε να κατασκευάσουμε αποτελεσματικά την πλήρη κανονική μορφή των ποσοτικών τύπων. Με την βοήθεια αυτού του αποτελέσματος αποδεικνύουμε ότι το πρόβλημα της ισοδυναμίας των ποσοτικών τύπων της λογικής είναι αποφασίσιμο. Τέλος, παρουσιάζουμε και διερευνούμε την τρίτη ποσοτική λογική της διατριβής αυτής που είναι η λογική της ασαφούς προτασιακής διαμόρφωσης. Αυτή η λογική είναι σε θέση να χαρακτηρίσει ποσοτικά χαρακτηριστικά όπου οι άλλες ποσοτικές λογικές που παρουσιάσαμε δεν μπορούν. Αυτά τα χαρακτηριστικά είναι ο βαθμός της αβεβαιότητας και αξιοπιστίας των αλληλεπιδράσεων μιας αρχιτεκτονικής. Παρουσιάζουμε μια ποσοτική προτασιακή λογική διαμόρφωσης σε μια De Morgan άλγεβρα. Κατασκευάζουμε ποσοτικούς τύπους που χαρακτηρίζουν γνωστές αρχιτεκτονικές στις οποίες θεωρούμε ότι οι αλληλεπιδράσεις τους έχουν κάποιο βαθμό αβεβαιότητας. Στη συνέχεια, ασχολούμαστε με το πρόβλημα της ισοδυναμίας των τύπων της λογικής μας. Αρχικά, δείχνουμε ότι κάθε ποσοτικός τύπος μπορεί να γραφεί σε κανονική μορφή σε εκθετικό χρόνο. Στη συνέχεια, αποδεικνύουμε ότι το πρόβλημα της ισοδυναμίας των ποσοτικών τύπων σε μια τυχαία De Morgan άλγεβρα είναι αποφασίσιμο σε εκθετικό χρόνο. Τέλος, ασχολούμαστε με τύπους που δεν είναι ισοδύναμοι σε μια τυχαία De Morgan άλγεβρα αλλά μόνο σε συγκεκριμένες όπως η Kleene και η Boolean άλγεβρα. Τέλος, αποδεικνύουμε ότι για κάθε ποσοτικό τύπο σε μια Kleene άλγεβρα (αντίστοιχα σε μια άλγεβρα του Boole) μπορούμε να κατασκευάσουμε αποτελεσματικά τον ισοδύναμο ποσοτικό τύπο του σε κανονική μορφή. Ως εκ τούτου, το πρόβλημα ισοδυναμίας των ποσοτικών τύπων στις προαναφερθείσες De Morgan άλγεβρες είναι επίσης αποφασίσιμο.
description: Software architectures are crucial in design and development of complex software systems. 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 characterizes the qualitative features of software architectures. In this dissertation, we study weighted logics which are able to describe software architectures with quantitative features. We propose three weighted logics where they can describe a range of quantitative features of architectures. 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. 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. The second main result of this work states that the equivalence of two weighted formulas is decidable. Next, by using the Maude system we accomplish to compute the full normal form of every weighted formula in an automated way. In the sequel, 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. 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. 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.