Quantitative modelling of parametric component-based systems

Abstract

The design of complex systems is usually addressed by component-based methods that lie in constructing and coordinating multiple components of the same or different type. Moreover, many of these systems are parametric, i.e., aim to operate independently of the number of their components. Parametric systems form a wide class of component-based systems and consist of a finite number of component types each with an unknown number of component instances. The modelling process of such systems involves defining the communication patterns among the components. Coordination principles can be specified by means of architectures that characterize the topology and the permissible interactions among the components of a system. Efficient description of architectures is important in order for the systems to meet most of their requirements by construction. To achieve well-founded design there is need to address both the qualitative and quantitative aspects of architectures. On the other hand, the characterization of architectures takes place at the early stages of the modelling process, and hence a key issue is expressing the uncertainty resulting from ambiguity or missing information in the connections of the components. In this dissertation, we address these issues and for this we study the modelling problem of parametric component-based systems. We propose a logic-based modelling method for architectures applied to parametric component-based systems, in the qualitative, quantitative and fuzzy setting, in order to describe respectively, the interactions of the components, their weights and their uncertainty. In each of the three settings, we model a system as a pair of a set of components and an architecture. The qualitative and fuzzy framework belong to the most general quantitative framework. Firstly, we introduce an extended propositional interaction logic in order to formalize architectures and in turn investigate a first-order extended interaction logic which serves as a formal language for parametric architectures. These logics achieve to encode the order of the interactions and their recursive appearance, as it is imposed by each architecture. We model components with labelled transition systems, and in turn we define a component-based system as a pair of a finite set of components and an architecture, while a parametric component-based system is defined as a pair of a set of parametric components and a parametric architecture. Moreover, we show that the extended propositional interaction logic and its first-order level can sufficiently describe several well-known architectures applied in component-based systems and parametric component-based systems, respectively. In turn, for the sentences of first-order extended interaction logic we prove the decidability of the equivalence and validity problem in doubly exponential time as well as the decidability of the satisfiability problem in exponential time. We show the robustness of the presented framework by effectively extending our results in the quantitative setup. In particular, we introduce a weighted extended propositional interaction logic and a weighted first-order extended interaction logic over commutative semirings for describing the non-functional aspects of architectures and parametric architectures, respectively. Then we describe a weighted component by a pair of a component and a weighted mapping. In turn, we define a weighted component-based system as a pair of a finite set of weighted components and a weighted architecture, and a parametric weighted component-based system as a pair of a set of parametric weighted components and a parametric weighted architecture. The two weighted logics serve for modelling several architectures and parametric architectures, respectively, in the weighted setup, by respecting the order and recursion in their interactions. Also, we prove that the equivalence problem for the sentences of weighted first-order extended interaction logic is decidable in doubly exponential time over a large class of semirings, namely the class (of subsemirings) of skew fields. In turn, we introduce a fuzzy extended propositional interaction logic and a fuzzy first-order extended interaction logic over De Morgan algebras in order to model uncertainty in architectures and parametric architectures, respectively. Then we define a fuzzy component-based system as a pair of a finite set of components and a fuzzy architecture, and a parametric fuzzy component-based system as a pair of a set of parametric components and a parametric fuzzy architecture. Moreover, we apply fuzzy extended propositional interaction logic and fuzzy first-order extended interaction logic for modelling uncertainty in several architectures and parametric architectures, respectively, by respecting the order restrictions and the recursive appearance of their fuzzy interactions. Finally, we prove that the equivalence problem for a large class of sentences of fuzzy first-order extended interaction logic is decidable in doubly exponential time. For any such sentence over a totally ordered De Morgan algebra, we further prove that we can compute in exponential time the set of sequences of parametric fuzzy interactions which ensure the trustworthiness of the sentence according to a particular threshold.

Η μοντελοποίηση πολύπλοκων συστημάτων συνήθως επιτυγχάνεται με μεθόδους βασισμένες σε συνιστώσες στις οποίες η κατασκευή ενός συστήματος προκύπτει από τον σχεδιασμό και την σύνθεση πολλαπλών συνιστωσών του ίδιου ή διαφορετικού τύπου, οι οποίες αλληλεπιδρούν μεταξύ τους. Ωστόσο, πολλά από αυτά τα συστήματα είναι παραμετρικά δηλαδή λειτουργούν ανεξάρτητα από το πλήθος των αντιγράφων των συνιστωσών κάθε τύπου που τα απαρτίζουν. Τα παραμετρικά συστήματα αποτελούν μια ευρεία κατηγορία συστημάτων βασισμένα σε συνιστώσες και προκύπτουν από ένα πεπερασμένο αριθμό τύπων συνιστωσών όπου κάθε τύπος συνιστώσας έχει άγνωστο πλήθος αντιγράφων. Η μοντελοποίηση τέτοιων συστημάτων απαιτεί τη φορμαλιστική περιγραφή των κανόνων που αφορούν τις συνδέσεις μεταξύ των συνιστωσών τους. Τέτοιοι κανόνες επικοινωνίας μπορούν να περιγραφούν μέσω της έννοιας της αρχιτεκτονικής η οποία χαρακτηρίζει τη τοπολογία και τις επιτρεπτές αλληλεπιδράσεις μεταξύ των συνιστωσών ενός συστήματος. Ο ορθός χαρακτηρισμός των αρχιτεκτονικών εξασφαλίζει ότι το σύστημα ικανοποιεί τις περισσότερες προδιαγραφές λειτουργίας του, από κατασκευή. Για να επιτευχθεί μια καλά θεμελιωμένη μοντελοποίηση των αρχιτεκτονικών θα πρέπει να περιγραφούν τα ποιοτικά χαρακτηριστικά τους, αλλά και τα ποσοτικά τους χαρακτηριστικά όταν απαιτούνται. Από την άλλη, ο χαρακτηρισμός των αρχιτεκτονικών γίνεται στα αρχικά στάδια της κατασκευής των συστημάτων και ως εκ τούτου είναι σημαντική η περιγραφή της αβεβαιότητας και της έλλειψης πληροφοριών που οφείλονται στις αλληλεπιδράσεις των συνιστωσών. Στη παρούσα διδακτορική διατριβή, μελετάμε το πρόβλημα της μοντελοποίησης για παραμετρικά συστήματα βασισμένα σε συνιστώσες. Για αυτό, μοντελοποιούμε τις αρχιτεκτονικές τέτοιων συστημάτων στο ποιοτικό, το ποσοτικό και το ασαφές πλαίσιο, με τη χρήση λογικών, ώστε να περιγράψουμε τις αλληλεπιδράσεις των συνιστωσών, τα βάρη αυτών και την αβεβαιότητα αυτών, αντίστοιχα. Έπειτα, και στα τρία πλαίσια μοντελοποιούμε ένα σύστημα ως ένα ζεύγος από ένα σύνολο συνιστωσών και μια αρχιτεκτονική. Το ποιοτικό και ασαφές πλαίσιο υπάγονται στο γενικότερο ποσοτικό πλαίσιο μοντελοποίησης. Αρχικά εισάγουμε μια επεκταμένη προτασιακή λογική αλληλεπιδράσεων και στη συνέχεια μια πρώτης-τάξης επεκταμένη λογική αλληλεπιδράσεων για την φορμαλιστική περιγραφή των αρχιτεκτονικών και των παραμετρικών αρχιτεκτονικών, αντίστοιχα. Οι συγκεκριμένες λογικές επιτυγχάνουν να κωδικοποιήσουν την σειρά εμφάνισης των επιτρεπτών αλληλεπιδράσεων καθώς και την αναδρομική εμφάνιση τους, όπως επιβάλλεται από την εκάστοτε αρχιτεκτονική. Έπειτα, μοντελοποιούμε τις συνιστώσες ενός συστήματος με τα λεγόμενα συστήματα μεταβάσεων με ετικέτες. Έτσι, ένα σύστημα που βασίζεται σε συνιστώσες ορίζεται ως ένα ζεύγος από ένα πεπερασμένο σύνολο συνιστωσών και μια αρχιτεκτονική, και ένα παραμετρικό σύστημα που βασίζεται σε συνιστώσες ορίζεται ως ένα ζεύγος από ένα σύνολο παραμετρικών συνιστωσών και μια παραμετρική αρχιτεκτονική. Στη συνέχεια, παρουσιάζουμε διάφορες αρχιτεκτονικές και παραμετρικές αρχιτεκτονικές οι οποίες μοντελοποιούνται επιτυχώς με την επεκταμένη προτασιακή και την πρώτης-τάξης επεκταμένη λογική αλληλεπιδράσεων, αντίστοιχα. Επιπλέον, για τις προτάσεις της πρώτης-τάξης επεκταμένης λογικής αλληλεπιδράσεων αποδεικνύουμε την αποφασισιμότητα για το πρόβλημα της ισοδυναμίας και της εγκυρότητας τους σε διπλά εκθετικό χρόνο, ενώ η αποφασισιμότητα για το πρόβλημα της ικανοποιησιμότητας τους αποδεικνύεται σε εκθετικό χρόνο. Στη συνέχεια, επαληθεύουμε την ευρωστία της συγκεκριμένης μεθόδου μοντελοποίησης καθώς την επεκτείνουμε στο ποσοτικό πλαίσιο. Συγκεκριμένα, εισάγουμε μια επεκταμένη προτασιακή λογική αλληλεπιδράσεων με βάρη και μια πρώτης-τάξης επεκταμένη λογική αλληλεπιδράσεων με βάρη, με τιμές από αντιμεταθετικούς ημιδακτύλιους, για την μοντελοποίηση των ποσοτικών χαρακτηριστικών των αρχιτεκτονικών και των παραμετρικών αρχιτεκτονικών, αντίστοιχα. Έπειτα, μια ποσοτική συνιστώσα, δηλαδή μία συνιστώσα με βάρη περιγράφεται ως ένα ζεύγος από μία συνιστώσα και μία απεικόνιση βαρών. Συνεπώς, ένα ποσοτικό σύστημα βασισμένο σε συνιστώσες ορίζεται ως ένα ζεύγος από ένα πεπερασμένο σύνολο συνιστωσών με βάρη και μια αρχιτεκτονική με βάρη, και ένα παραμετρικό ποσοτικό σύστημα βασισμένο σε συνιστώσες ορίζεται ως ένα ζεύγος από ένα σύνολο παραμετρικών συνιστωσών με βάρη και μια παραμετρική αρχιτεκτονική με βάρη. Στη συνέχεια, οι δύο παραπάνω λογικές με βάρη εφαρμόζονται για τη μοντελοποίηση διαφόρων αρχιτεκτονικών και παραμετρικών αρχιτεκτονικών, αντίστοιχα, στο ποσοτικό πλαίσιο, λαμβάνοντας υπόψη αν υπάρχει διάταξη και αναδρομή στις αλληλεπιδράσεις τους. Επιπροσθέτως, αποδεικνύουμε ότι το πρόβλημα της ισοδυναμίας των προτάσεων της πρώτης-τάξης επεκταμένης λογικής αλληλεπιδράσεων με βάρη είναι αποφασίσιμο σε διπλά εκθετικό χρόνο για ένα ευρύ σύνολο ημιδακτυλίων, και συγκεκριμένα για το σύνολο (των υπο-ημιδακτυλίων) των skew fields. Έπειτα, εισάγουμε μια ασαφή επεκταμένη προτασιακή λογική αλληλεπιδράσεων και μια ασαφή πρώτης-τάξης επεκταμένη λογική αλληλεπιδράσεων με σκοπό τη μοντελοποίηση της αβεβαιότητας στις αρχιτεκτονικές και στις παραμετρικές αρχιτεκτονικές, αντίστοιχα. Το πεδίο τιμών ασάφειας είναι μια De Morgan άλγεβρα. Στη συνέχεια, ένα ασαφές σύστημα βασισμένο σε συνιστώσες ορίζεται ως ένα ζεύγος από ένα πεπερασμένο σύνολο συνιστωσών και μια ασαφή αρχιτεκτονική, και ένα παραμετρικό ασαφές σύστημα βασισμένο σε συνιστώσες ορίζεται ως ένα ζεύγος από ένα σύνολο παραμετρικών συνιστωσών και μια παραμετρική ασαφή αρχιτεκτονική. Έπειτα, οι δύο παραπάνω ασαφείς λογικές εφαρμόζονται επιτυχώς για τη περιγραφή, στο ασαφές πλαίσιο, διαφόρων αρχιτεκτονικών και παραμετρικών αρχιτεκτονικών, αντίστοιχα, λαμβάνοντας υπόψη την διάταξη και την αναδρομική εμφάνιση των ασαφών αλληλεπιδράσεων τους, όπως επιβάλλεται από την εκάστοτε αρχιτεκτονική. Τέλος, αποδεικνύουμε ότι το πρόβλημα της ισοδυναμίας για μία μεγάλη κλάση των προτάσεων της ασαφούς πρώτης-τάξης επεκταμένης λογικής αλληλεπιδράσεων είναι αποφασίσιμο σε διπλά εκθετικό χρόνο. Για κάθε τέτοια πρόταση, αποδεικνύουμε επιπλέον πως αν η De Morgan άλγεβρα είναι ολικά διατεταγμένη τότε μπορούμε να υπολογίσουμε σε εκθετικό χρόνο το σύνολο των λέξεων των παραμετρικών ασαφών αλληλεπιδράσεων που διασφαλίζουν την αξιοπιστία της πρότασης σύμφωνα με ένα συγκεκριμένο όριο.