Correct by construction model based design for systems and software

Abstract

This thesis introduces correctness-by-construction techniques for rigorous system design. In particular, we focused on how to produce and validate a functional application model from a set of requirements or from application code. First, we dealt with the early validation of system requirements and design, in order to eliminate the need for a-posteriori verification at the later stages of development. Second, we focused on the automated generation of functional application models from programs with nested syntax, while maintaining the program semantics. Finally, we proposed a design flow that aims to maintain the consistency between the application model and the application code, using a new domain-specific language that focuses on the design of resource-constrained applications for the Internet of Things.

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