Enabling reasoning and verification support for intelligent agent systems, using formal methods

Abstract

Formal methods are techniques, languages and tools based on mathematics, which provide an unambiguous, strict mathematical description or specication which is used for eective design, analysis and verication of desired properties of the system. An important branch of formal methods are algebraic specication languages with a rigorous basis on mathematical logical systems or combinations of them. Such a language is CafeOBJ, an executable, new generation algebraic specication language, member of the OBJ family languages. Its main characteristic, that dierentiates it from other formalisms, is its direct support to behavioural specication paradigm since it embeds special hidden sorts and behavioural operators in its syntax. Behavioural specication is based on hidden algebra and supports an object oriented style of algebraic specication. It also supports specication of distributed complex systems as abstract state machines and verication of safety properties of them through theorem proving techniques such as simultaneous induction and coinduction. The scope of the thesis is the modelling and verication of intelligent agents using algebraic specication techniques. By intelligent agents we refer to the systems used in the New or Semantic Web in order to achieve the need for reactivity, interaction and communication between its various components. An intelligent agent can be dened as an autonomous entity which observes through sensors and acts upon an environment using actuators (i.e. it is an agent) and directs its activity towards achieving goals. Due to the special characteristics of such systems, and their increased development as well as their use in critical domains, the requirements for reliability, security and proper functionality has led to the use of formal methods for their analysis and the development of new methodologies oriented to these systems. To this end, in this thesis an algebraic framework is proposed for the specication and verication of two basic types of intelligent systems, those whose behaviour is expressed in terms of reactive rules (reactive rule-based systems) and those who can sense the changes in their physical environment (context-aware systems), and adapt their behaviour accordingly. In the rst category of intelligent agents, we rst give formal semantics, based on the hidden algebra formalism, to the basic reactive rule families, then we formally analyse and verify reactive rule-based systems using equational logic, next we propose the use of rewriting logic for the detection of structural errors of the rules, such as termination and conuence, and nally we compare the proposed approaches. In the second type of agents, which are usually more complex, the specication of the system, is dened as the composition of the specications of3its components, i.e. the specications which describe data types as visible sorts and the various components of the system as Observational Transition Systems, a kind of behavioural object. In this way the complex interactions of such systems can be expressed in a natural and dynamic way. Based on the specication, verication of properties of the intelligent system using theorem proving techniques is also feasible. The fact that the system is specied as a transition system, using equational or rewriting logic, makes the method easier to read, understand and learn than other related methods, which prerequisite deeper knowledge of theorem proving, or that are based in higher order logic for example. To demonstrate the applicability and eectiveness of the proposed methodologies, a number of case studies are conducted. Security aspects of intelligent systems are of major importance, and it was inevitable to take them into account. To this end we present the verication of the behaviour of various intelligent systems from the literature. In the last section of the thesis, an extension of the specication and verication methodology, supported by the CafeOBJ language, is proposed that provides more automation for the proofs and allows the use of more conventional verication tools, by integrating it with the Athena automated theorem proving system. The proposed methodology is based on the interaction of the two languages so as to be able to exploit the nice properties of each method and thus have better results in the verication process. Finally, a number of applications of the methodology in protocols that are often used as case studies, especially for tools dedicated to the verication of complex systems, are presented.

Οι τυπικές μέθοδοι είναι τεχνικές, γλώσσες και εργαλεία με ισχυρό μαθηματικό υπόβαθρο, οι οποίες μας δίνουν τη δυνατότητα μιας αυστηρής, μαθηματικά ορισμένης, χωρίς ασάφειες, περιγραφής ή προδιαγραφής των συστημάτων, η οποία χρησιμοποιείται για το σχεδιασμό τους, την ανάλυση, και την επαλήθευση επιθυμητών ιδιοτήτων τους. Ένας πολύ σημαντικός κλάδος των τυπικών μεθόδων είναι οι γλώσσες αλγεβρικών προδιαγραφών, οι οποίες έχουν ως μαθηματικό υπόβαθρο κάποιο μαθηματικό λογικό σύστημα ή και συνδυασμούς λογικών συστημάτων. Μια τέτοια εκτελέσιμη αλγεβρική γλώσσα προδιαγραφών νέας γενιάς, η οποία είναι απόγονος των ιστορικών γλωσσών OBJ, είναι η CafeOBJ. Το βασικότερο χαρακτηριστικό της γλώσσας αυτής, που τη διακρίνει από αντίστοιχους φορμαλισμούς, είναι η άμεση υποστήριξη που παρέχει για συμπεριφοριακές προδιαγραφές, με την ενσωμάτωση στο συντακτικό της ειδικών τύπων και τελεστών. Η συμπεριφοριακή προδιαγραφή, η οποία έχει τις βάσεις της στην άλγεβρα με κρυμμένους τύπους, ενισχύει την αλγεβρική προδιαγραφή με αντικείμενα ή αφηρημένες μηχανές καταστάσεων, δίνοντας έτσι τη δυνατότητα περιγραφής σύνθετων δυναμικών συστημάτων. Παράλληλα, με τη χρήση τεχνικών επαλήθευσης που βασίζονται στη συμπεριφοριακή προδιαγραφή, η CafeOBJ μας δίνει τη δυνατότητα απόδειξης ιδιοτήτων ασφαλείας των συστημάτων που έχουν προδιαγραφεί. Αντικείμενο της διατριβής αποτελεί η μοντελοποίηση και η επαλήθευση της συμπεριφοράς έξυπνων συστημάτων με χρήση τεχνικών αλγεβρικών προδιαγραφών. Με τον όρο έξυπνα συστήματα (ή έξυπνοι πράκτορες) αναφερόμαστε στα συστήματα τα οποία χρησιμοποιούνται στον Νέο ή Σημασιολογικό Ιστό ώστε να εξασφαλίζεται η ανάγκη για αντιδραστικότητα (reactivity), αλληλεπίδραση και επικοινωνία μεταξύ των διαφόρων συστατικών του. Ένα έξυπνο σύστημα μπορεί να οριστεί σαν μία αυτόνομη οντότητα η οποία παρατηρεί μέσω αισθητήρων το περιβάλλον του και έπειτα με βάση τις παρατηρήσεις δρα κατάλληλα σε αυτό, κατευθύνοντας δηλαδή τις δραστηριότητές του προς την επίτευξη των στόχων του. Λόγω της ιδιαιτερότητας των συστημάτων αυτών, και εξαιτίας της αύξησης της ανάπτυξής τους καθώς και της χρήσης τους σε κρίσιμα συστήματα, οι απαιτήσεις για αξιοπιστία, ασφάλεια και λειτουργικότητα έχουν οδηγήσει στην ανάγκη για χρήση τυπικών μεθόδων για την ανάλυση τους και στην ανάπτυξη νέων μεθοδολογιών προσανατολισμένων συγκεκριμένα σε αυτά τα συστήματα. Σε αυτήν την διατριβή προτείνεται ένα πλαίσιο προδιαγραφής και επαλήθευσης δύο βασικών κατηγοριών έξυπνων πρακτόρων, εκείνων των συστημάτων των οποίων η συμπεριφορά ορίζεται μέσω αντιδραστικών κανόνων (reactive rules) καθώς και εκείνων των οποίων οι ενέργειες εξαρτώνται από το περιβάλλον τους (context-aware systems) καθώς προσαρμόζουν τη συμπεριφορά τους ανάλογα με τις αλλαγές που παρατηρούν. Στην πρώτη κατηγορία συστημάτων αρχικά προτείνεται μία τυπική σημασιο1λογίατωναναδραστικώνκανόνων, βασισμένηστηνάλγεβραμεκρυφούςτύπους, έπειτα μελετάται η τυπική ανάλυση και επαλήθευση των έξυπνων συστημάτων που ορίζονται μέσω αναδραστικών κανόνων με χρήση εξισωτικής λογικής, στη συνέχεια προτείνεται η χρήση λογικής βασισμένης στην αναγραφή όρων για την ανακάλυψη λαθών στη δομή των αναδραστικών κανόνων, όπως τερματισμού και σύγκλισης, και τέλος συγκρίνονται οι προτεινόμενες προσεγγίσεις. Στη δεύτερη κατηγορία συστημάτων, τα οποία κατά κανόνα είναι και πιο σύνθετα, ορίζουμε την προδιαγραφή τους ως τη σύνθεση των προδιαγραφών των επιμέρους συστατικών τους, δηλ. των προδιαγραφών που περιγράφουν τους τύπους δεδομένων και τα συστατικά του συστήματος σαν Παρατηρήσιμα Συστήματα Μετάβασης - ένα είδος συμπεριφοριακού αντικειμένου - ώστε να μπορέσει να εκφραστεί κατάλληλα η αλληλεπίδραση των συστατικών των συστημάτων αυτών. Στη συνέχεια με βάση τις προδιαγραφές και κάνοντας χρήση τεχνικών απόδειξης θεωρήματος είναι δυνατή η επαλήθευση ιδιοτήτων των συστημάτων. Το ότι ο δυναμικός χαρακτήρας του συστήματος προδιαγράφεται με κανόνες μετάβασης και χρησιμοποιώντας εξισωτική λογική ή λογική αναγραφής, κάνει τη μέθοδο αυτή καλύτερα κατανοητή και ευκολότερη από αντίστοιχες μεθόδους που προαπαιτούν βαθύτερη γνώση των τεχνικών απόδειξης θεωρήματος ή που βασίζονται σε λογικές ανώτερου επίπεδου. Η εφαρμογή των προτεινόμενων μεθόδων παρουσιάζεται μέσα από τη μελέτη μιας σειράς περιπτώσεων που αντιστοιχούν σε σχετικά συστήματα και πρωτόκολλα. Τα ζητήματα ασφαλείας για ένα έξυπνο σύστημα είναι μεγάλης κρισιμότητας και γι’ αυτό το λόγο δεν θα μπορούσαν να παραλειφθούν. Στα πλαίσια αυτά έχουν προδιαγραφεί και επαληθευθεί συστήματα έξυπνων πρακτόρων από τη διεθνή βιβλιογραφία. Στο τελευταίο κομμάτι της διατριβής προτείνεται μια επέκταση της μεθοδολογίας μοντελοποίησης και απόδειξης ιδιοτήτων που υποστηρίζεται από τη γλώσσα CafeOBJ, κατάλληλη για την αυτοματοποίηση των αποδείξεων και τη χρήση πιο σύγχρονων εργαλείων ανάλυσης προδιαγραφών, με χρήση του συστήματος αυτόματης απόδειξης Athena. Προτείνεται μία μεθοδολογία αλληλεπίδρασης των δύο συστημάτων απόδειξης, ώστε να είμαστε σε θέση να εκμεταλλευτούμε τα πλεονεκτήματα του καθενός ξεχωριστά, και παρουσιάζονται παραδείγματα εφαρμογών της προτεινόμενης προσέγγισης σε πρωτόκολλα που μελετώνται συχνά για τη δοκιμή εργαλείων επαλήθευσης σύνθετων συστημάτων.