Επαλήθευση και επιβεβαίωση αρχιτεκτονικής (υλικό +λογισμικό) αρχιτεκτονικής συστήματος ελέγχου υβριδικού ηλεκτρικού οχήματος
Creators: name: Ντάνη, Χριστίνα Ιπποκράτη
Publisher: name: Aristotle University of Thessaloniki
Year: 2013
Subjects: χρονικά αυτόματα
μοντελοποίηση υποσυστημάτων υβριδικού-ηλεκτρικού οχήματος
κεντρική ελεγκτική μονάδα υβριδικού-ηλεκτρικού οχήματος
timed automata
modeling of critical components of a hybrid-electric vehicle
UPPAAL

description: Η παρούσα εργασία αποβλέπει στη δημιουργία ενός τυπικού μαθηματικού μοντέλου της αρχιτεκτονικής σχεδίασης του ελεγκτή της λειτουργίας των κρίσιμων μονάδων ενός υβριδικού ηλεκτρικού οχήματος, με στόχο της την επαλήθευση των απαιτήσεων που πρέπει να ικανοποιεί η αρχιτεκτονική. Η επαλήθευση αυτή γίνεται προσομοιώνοντας τη συμπεριφορά του μοντέλου αυτού και ελέγχοντας τη μετάβαση του, σε καταστάσεις που μπορούν να συνδεθούν με τις απαιτήσεις που πρέπει να ικανοποιεί ο ελεγκτής κάτω από διάφορα πιθανά σενάρια λειτουργίας του οχήματος. Ο μαθηματικός φορμαλισμός που επιλέχθηκε για την μοντελοποίηση της αρχιτεκτονικής του ελεγκτή, είναι αυτός των χρονικών αυτομάτων. Η εργασία διαρθρώνεται ως εξής: αρχικά περιγράφεται το πρόβλημα που τέθηκε, όπως αυτό αποτυπώνεται από τις λειτουργικές απαιτήσεις του κατασκευαστή. Ακολουθεί μία αναφορά στη θεωρία των χρονικών αυτομάτων και μία προσέγγιση μέσω βιβλιογραφικής έρευνας, της αιτίας, που τα χρονικά αυτόματα επιλέχθηκαν ως ο καταλληλότερος φορμαλισμός, για την επιβεβαίωση των προδιαγραφών του συστήματος. Στη συνέχεια περιγράφεται το εργαλείο UPPAAL ως ένα πιθανό εργαλείο με το οποίο μπορεί κανείς να μοντελοποιήσει, να προσομοιώσει και να επαληθεύσει την ορθή λειτουργία ενός μοντέλου του συστήματος, που βρίσκεται στη φάση της αρχιτεκτονικής του σχεδίασης. Στο τέλος, περιγράφονται όλα τα βήματα που ακολουθήθηκαν αναλυτικά, τα μοντέλα που δημιουργήθηκαν και τα κατηγορήματα που προέκυψαν, προκειμένου να επιβεβαιωθεί κατά πόσον η αρχιτεκτονική σχεδίαση του συστήματος που προτείνεται, ικανοποιεί τις τεθείσες προδιαγραφές.
description: This postgraduate thesis describes a mathematical formalism that was created in order to simulate the operation of the control unit and the operation of the critical components of a hybrid electric vehicle that are controlled by this unit. The purpose of this model was the verification of the specifications that were defined during design. In order to verify the validity of the model, the operation was simulated and the transitions to states related to possible vehicle conditions as specified by the manufacturer were checked with the use of possible operational scenarios. The mathematical formalism that was chosen for modeling the control unit and the operation of the critical components of the hybrid electric vehicle is the timed automata. This postgraduate thesis is composed by four parts: first the architecture of the control unit and that of the critical components of the vehicle are described, as these were provided in the manufacturer’s specifications. Also a general description of the basic principles of the operation of the hybrid electric vehicles based to bibliographical sources is provided. Secondly, an analysis of the theory of the timed automata follows, where it is justified through bibliographical research, the reason that the timed automata were chosen as the appropriate formalism for the verification of this model. Thirdly, the software tool UPPAAL which is used for modeling with timed automata is described since it was also used for the simulation and the verification of this model. Finally, all the actions required for modeling the operation of the control unit and the operation of the critical components of the vehicle are described and all the models and the scenario’s created in order to verify that the design of the model is according to the specifications are provided and explained thoroughly.
description: Σε συνεργασία με το τμήμα Λογιστικής και Χρηματοοικονομικής (Πανεπιστήμιο Μακεδονίας)