Παρουσίαση ΔΕ Σ. Μαρτίνι
η παρουσίαση της ΔΕ του κ. Σταύρου Μαρτίνι θα γίνει Δευτέρα (25 Μαίου) στις 13:00 στο εργαστήριο ISCA-Lab.
Σύνοψη Διπλωματικής Εργασίας
Η συντονισμένη λειτουργία διακριτής λογικής λήψης αποφάσεων με συνεχή έλεγχο σε πραγματικό χρόνο αποτελεί μία από τις μεγαλύτερες προκλήσεις στα ενσωματωμένα συστήματα. Κανονικά, η διακριτή λογική και ο συνεχής έλεγχος αναπτύσσονται ξεχωριστά με διαφορετικά εργαλεία και ενωτίζονται χειροκίνητα, όπου προκύπτουν τα περισσότερα λογικά σφάλματα. Η παρούσα εργασία προτείνει διμερή αρχιτεκτονική βασισμένη στη τυπική σύνθεση επιβλέποντος ελεγκτή με χρήση του Eclipse ESCET toolkit.
Στο ανώτερο επίπεδο, το ESCET μοντελοποιεί κάθε υποσύστημα ωςExtended Finite Automaton (EFA) στη γλώσσα CIF. Οι απαιτήσεις ασφαλείας και συντονισμού εκφράζονται ως τυπικοί περιορισμοί, και το ESCET συνθέτει αυτόματα επιβλέποντα ελεγκτή με μαθηματικές εγγυήσεις: ελεγχιμότητα, μη αποκλεισιμότητα και μέγιστη επιτρέψιμη συμπεριφορά. Πριν την παραγωγή κώδικα, επαληθεύονται πρόσθετες ιδιότητες, όπως περιορισμένος χρόνος απόκρισης και σύγκλιση.
Στο κατώτερο επίπεδο, κάθε κινητήρας εκτελεί field-oriented control (FOC) με τη βιβλιοθήκη SimpleFOC με συχνότητα 20 kHz, πλήρως ανεξάρτητα από τον δικτυακό επιβλέποντα. Η επικοινωνία μεταξύ επιπέδων πραγματοποιείται μέσω ελάχιστης, τυπικά ορισμένης διεπαφής: οι εισόδοι CIF λαμβάνουν δεδομένα αισθητήρων που πυροδοτούν μη ελεγχόμενα γεγονότα, ενώ τα ελεγχόμενα γεγονότα παράγουν συναρτήσεις επανακάλεσης (callbacks) για αποστολή εντολών επενεργητών στους τοπικούς κόμβους. Οι κόμβοι διαχειρίζονται αυτοτελώς τις αντιδράσεις ασφαλείας χωρίς αναμονή έγκρισης από τον επιβλέποντα.
Η αρχιτεκτονική δοκιμάστηκε σε φυσικό δίκτυο δύο κόμβων BLDC κινητήρων συνδεδεμένων σε δίκτυο CAN 2.0B, υλοποιώντας σύστημα Αερισμού με Ανάκτηση Θερμότητας (Heat Recovery Ventilation). Η εφαρμογή απαιτούσε 46 τυπικές προδιαγραφές για συντονισμένη εκκίνηση, διαδοχική βαθμονόμηση, ανάκαμψη βλαβών με περιορισμένους επαναληπτικούς κύκλους και αυστηρή λειτουργία «όλα ή τίποτα» στους ανεμιστήρες. Εισήχθησαν ηλεκτρικές βλάβες, θερμικές βλάβες και διακοπή τροφοδοσίας εν λειτουργεία. Σε όλες τις περιπτώσεις, ο επιβλέπων ελεγκτής συμπεριφέρθηκε ακριβώς όπως προέβλεπε το τυπικό μοντέλο, χωρίς αποκλεισμούς ή παραβιάσεις προδιαγραφών.
Η προτεινόμενη προσέγγιση μειώνει δραστικά τα λογικά σφάλματα ενσωμάτωσης και παρέχει εμπορικά βιώσιμη λύση από τις τυπικές προδιαγραφές έως τον ενσωματωμένο κώδικα.
Abstract
Coordinating logical decision-making with real-time physical control is one of the toughest challenges in embedded systems. Typically, the discrete logic and continuous control are developed separately using different tools, then manually stitched together. Most logic errors happen during this manual integration step. This thesis proposes a two-layer architecture based on formal supervisory control synthesis to solve this problem.
The upper layer uses the Eclipse ESCET toolkit and CIF specification language. Each subsystem is modeled as an Extended Finite Automaton (EFA). Safety and coordination requirements are written as formal constraints, and ESCET automatically synthesizes a supervisor. The resulting supervisor has mathematical guarantees: it is controllable, non-blocking, and maximally permissive. Before code generation, we verify additional properties like bounded response time and confluence.
The lower layer handles real-time control. Each motor node runs field-oriented control (FOC) using the SimpleFOC library at 20 kHz, completely independent of the network supervisor. Communication between layers happens through a minimal, formally-defined interface: CIF input variables receive sensor data that trigger uncontrollable events, while controllable events generate callbacks that send actuator commands to local nodes. Importantly, local nodes handle their own safety reactions without waiting for supervisor approval.
We tested the architecture on a physical two-node BLDC motor network connected via CAN 2.0B, implementing a Heat Recovery Ventilation (HRV) system. The application required 46 formal requirements covering coordinated startup, sequential calibration, fault recovery with bounded retries, and strict “both or nothing” fan operation. We injected electrical faults, thermal faults, and power loss on live hardware. In all cases, the supervisor behaved exactly as the formal model predicted—no deadlocks, no requirement violations.