Μοντελοποίηση και επαλήθευση προδιαγραφών ενσωματωμένων συστημάτων

Abstract

The first aim of this work was to propose a framework for modeling and verifying the safety and performance requirements of an embedded system design, that is, a physical entity that consists of a continuous time part and an embedded computing part that controls the operation of the continuous time part. The proposed framework considers the phases of the selection of the appropriate formalism for modeling the system, the development of the model, the analysis of its computation complexity, the expression of requirements in mathematical logic predicates and the identification of the state trajectories of the model that satisfy the requirements. For the formalism selection, depending on the form of the differential equations that describe the continuous part of the hybrid system, guidelines have been issued for the selection of the most suitable timed automata or hybrid automata formalism or proposed extensions of them. For the model complexity the decidability of the system state space derivation is determined. For the requirements verification a search in the state space of the model is performed to check if the states that correspond to the requirements are reachable or not. A new method developed and proposed within the framework of this thesis, for state space trajectory search, that the states corresponding to the desired specifications on the models created by the proposed formalisms. The applicability of the proposed framework and the proposed search method as well as the efficiency of the proposed method to compute reachable states of the hybrid automaton from an initial state are demonstrated by four application examples.

Αντικείμενο της παρούσας διατριβής είναι η μελέτη των ενσωματωμένων συστημάτων, δηλαδή πολύπλοκα ψηφιακά συστήματα που έχουν ως βασικά τους στοιχεία προγραμματιζόμενα υπολογιστικά μέσα και συνιστούν είτε τμήμα ενός μεγαλύτερου συστήματος που αλληλεπιδρά με τον άνθρωπο ή με άλλα φυσικά συστήματα που πολλές φορές επιτελούν κρίσιμες από άποψη ασφάλειας λειτουργίες. Κατά τη σχεδίαση και κατασκευή των ενσωματωμένων συστημάτων ιδιαίτερη βαρύτητα δίνεται στην επαλήθευσή τους ώστε να ελεγχθεί εάν η βασική σχεδίαση μπορεί να οδηγήσει στην κατασκευή συστήματος που ικανοποιεί συγκεκριμένες προδιαγραφές λειτουργίας. Η διατριβή αυτή προσπάθησε να συμβάλλει στην αποτελεσματικότητα της καθιερωμένης συστηματικής μεθοδολογίας που εφαρμόζεται για την επαλήθευση ενσωματωμένων συστημάτων. Ειδικότερα, προτείνονται βελτιώσεις για την καλύτερη αυτοματοποίηση της δημιουργίας του τυπικού μοντέλου ενός ενσωματωμένου συστήματος. Στη συνέχεια προτείνεται ένας νέος φορμαλισμός μοντελοποίησης που συνδυάζει διακριτές και συνεχούς χρόνου καταστάσεις. Πιο συγκεκριμένα επεκτείνεται ο φορμαλισμός των χρονικών αυτομάτων και των υβριδικών αυτομάτων έτσι ώστε να καταστεί δυνατή η μοντελοποίηση συστημάτων που ενσωματώνονται σε περιβάλλοντα διακριτής και μη γραμμικής συμπεριφοράς που δεν καλύπτονται από τους προταθέντες μέχρι τώρα τύπους χρονικών και υβριδικών αυτομάτων. Για τη βελτίωση της μεθοδολογίας επαλήθευσης των προδιαγραφών προτείνεται ένας οδηγός επιλογής του φορμαλισμού περιγραφής του μοντέλου ανάλογα με τον τύπο του υπό μελέτη συστήματος και η εισαγωγή ενός νέου βήματος στο οποίο εκτιμάται η πολυπλοκότητα του χώρου καταστάσεων του μοντέλου. Τέλος, εισάγεται ένας νέος αλγόριθμος αναζήτησης καταστάσεων που αντιστοιχούν στις επιθυμητές προδιαγραφές σε μοντέλα που δημιουργούνται με τους προτεινόμενους φορμαλισμούς. Από την εφαρμογή των προτεινόμενων αλλαγών σε τέσσερις αντιπροσωπευτικές εφαρμογές ενσωματωμένων συστημάτων προκύπτει η επιβεβαίωση της εφαρμοσιμότητας της προτεινόμενης μεθοδολογίας καθώς και η αποτελεσματικότητα των προτεινόμενων βελτιώσεων.