Embedded systems verification and validation

Abstract

This thesis aims to bridge the gap between natural language requirements specification and formal analysis by introducing a methodology based on ontological semantics to enhance the accuracy, consistency, and reliability of critical embedded systems. Requirements in natural language are often characterized by ambiguities and inconsistencies, which make their transformation into formal models challenging. The proposed methodology addresses this issue by defining strict semantic frameworks for the specification of requirements and, through a semi-automated process, transforming them into formal models suitable for analysis. A key aspect of the approach is the development of tools that support the formulation, analysis, and visualization of requirements, enabling engineers to identify errors and verify properties such as completeness and safety from the early stages of development. The methodology was tested in real-world scenarios within the domain of space systems, demonstrating its usability and practical value. By automating critical stages and providing tools for the analysis and verification of requirements, the thesis facilitates a systematic and reliable transition from requirements specification to system design, reducing the time and resources required. Furthermore, the work paves the way for new research directions, building confidence in the transition from natural language specifications to formal design, with applications in domains that demand high levels of reliability and safety.

Η διατριβή αυτή στοχεύει στη γεφύρωση του χάσματος μεταξύ της προδιαγραφής απαιτήσεων σε φυσική γλώσσα και της τυπικής ανάλυσης, εισάγοντας μια μεθοδολογία που βασίζεται στην οντολογική σημασιολογία για την ενίσχυση της ακρίβειας, της συνέπειας και της αξιοπιστίας κρίσιμων ενσωματωμένων συστημάτων. Οι απαιτήσεις σε φυσική γλώσσα χαρακτηρίζονται συχνά από ασάφειες και ασυνέπειες, δυσχεραίνοντας τη μετατροπή τους σε τυπικά μοντέλα. Η προτεινόμενη μεθοδολογία επιλύει αυτό το πρόβλημα, ορίζοντας αυστηρά σημασιολογικά πλαίσια για τη διατύπωση απαιτήσεων, ενώ μέσω μιας ημιαυτόματης διαδικασίας, μετασχηματίζει τις απαιτήσεις σε τυπικά μοντέλα κατάλληλα για ανάλυση. Ένα βασικό στοιχείο της προσέγγισης είναι η ανάπτυξη εργαλείων που υποστηρίζουν τη διατύπωση, ανάλυση και οπτικοποίηση απαιτήσεων, επιτρέποντας στους μηχανικούς να εντοπίζουν σφάλματα και να επαληθεύουν ιδιότητες όπως η πληρότητα και η ασφάλεια ήδη από τα πρώτα στάδια της ανάπτυξης. Η μεθοδολογία δοκιμάστηκε σε πραγματικά σενάρια από τον τομέα των διαστημικών συστημάτων, αποδεικνύοντας τη χρηστικότητα και την πρακτική της αξία. Με την αυτοματοποίηση κρίσιμων σταδίων και την παροχή εργαλείων για την ανάλυση και την επαλήθευση των απαιτήσεων, η διατριβή διευκολύνει τη συστηματική και αξιόπιστη μετάβαση από τη διατύπωση απαιτήσεων στη σχεδίαση συστημάτων, μειώνοντας τον χρόνο και τους πόρους που απαιτούνται. Παράλληλα, η εργασία ανοίγει νέους δρόμους για την έρευνα, ενισχύοντας την εμπιστοσύνη στη μετάβαση από φυσικές προδιαγραφές σε τυπική σχεδίαση, με εφαρμογές σε τομείς που απαιτούν υψηλά επίπεδα αξιοπιστίας και ασφάλειας.