Verification of Real Time Systems:The extension of COSPAN in dense time

RDF 

 
Το τεκμήριο παρέχεται από τον φορέα :
Πανεπιστήμιο Κρήτης
Αποθετήριο :
E-Locus Ιδρυματικό Καταθετήριο
δείτε την πρωτότυπη σελίδα τεκμηρίου
στον ιστότοπο του αποθετηρίου του φορέα για περισσότερες πληροφορίες και για να δείτε όλα τα ψηφιακά αρχεία του τεκμηρίου*
κοινοποιήστε το τεκμήριο



Σημασιολογικός εμπλουτισμός/ομογενοποίηση από το EKT
1992 (EL)
Επαλήθευση Συστήματος Πραγματικού Χρόνου - η Επέκταση του COSPAN σε Συνεχή Χρόνο
Verification of Real Time Systems:The extension of COSPAN in dense time

Τζουνάκης, Παναγιώτης (EL)
Tzounakis, Panagiotis (EN)

Κ. Κουρκουμπέτης

Η συχνά τεράστια πολυπλοκότητα παράλληλων συστημάτων πραγματικού χρόνου κάνει πολύ δύσκολη τη σωστή σχεδίαση τους χωρίς κάποιας μορφής βοήθεια μέσω υπολογιστή. Σε αυτή την εργασία παρουσιάζουμε μια επέκταση του πολύ γνωστού μοντέλου επιλογής/απόφασης ( selection/resolution ή απλά ) AKS83a,AC85,GK80,Ku90,ABM86a η οποία συμπεριλαμβάνει χρονικούς περιορισμούς. Η επέκταση μας αποτελείται από μιά υλοποίηση ενός υπάρχοντος μοντέλου για χρονικές υποθέσεις και των αντίστοιχων αλγορίθμων Di89 μέσα στο μοντέλο. Περιγράφουμε τη χρήση και την υλοποίηση ενός νέου προγράμματος αυτόματης επαλήθευσης (verification) για συστήματα πραγματικού χρόνου με πεπερασμένες καταστάσεις το οποίο βασίζεται στο COSPAN, ένα πολύ γνωστό πρόγραμμα επαλήθευσης γιά παράλληλα συστηματα τα οποία είναι ανεξάρτητα από το χρόνο. Επεκτείνουμε το COSPAN προσθέτωντας μιά διεργασία ελεγκτή η οποία δημιουργείται αυτόματα και παρακολουθεί τους χρονικούς περιορισμούς, ώστε να αποκλείει συμπεριφορές του συστήματος που είναι χρονικά ασυνεπείς. Στην εργασία αρχικά παρουσιάζονται το μοντέλο και το COSPAN ως απαραίτητη υποδομή, το μοντέλο πραγματικού χρόνου, και η θεωρία και υλοποίηση των επεκτάσεων μας μέσω των οποίων χειριζόμαστε πληροφορία πραγματικού χρόνου. Στη συνέχεια συζητάμε τα αποτελέσματα της χρήσης του προγράμματος μας για τη λυση μερικών μη τετριμένων προβλημάτων. Το μοντέλο επιλογής/απόφασης είναι ένα μαθηματικό μοντέλο συγχρονισμού για συντρέχουσες διεργασίες, όπου ένα πολύπλοκο σύστημα μπορεί να περιγραφεί σαν ένα σύνολο από μηχανές πεπερασμένων καταστάσεων που συντονίζονται μεταξύ τους. Ενα χαρακτηριστικό, που κάνει το μοντέλο εξαιρετικά ελκυστικό, είναι ότι η σύζευξη των μηχανών περιγράφεται με κατηγορήματα (predicates) πάνω στα σήματα επικοινωνίας. Σε πολλές περιπτώσεις με αυτό τον τρόπο επιτυγχάνονται σύντομες, περιεκτικές και κατανοητές περιγραφές. Το μοντέλο είναι ένα μοντέλο διακριτού γραμμικού χρόνου. Ενας λογισμός ορίζεται πάνω σε διεργασίες οι οποίες συνθέτονται χρησιμοποιώντας τις πράξεις σύγχρονου ή ασύγχρονου γινομένου. Η επαλήθευση γίνεται προσθέτοντας συνθήκες αποδοχής στις διεργασίες εκφράζοντας έτσι επιθυμητές ιδιότητες του συστήματος, και/ή συνθήκες ζωτικότητας (liveness conditions). Το COSPAN HK89,KK86,HK90 είναι ένα εργαλείο λογισμικού για την περιγραφή και επαλήθευση συστημάτων που αποτελούνται από συντονιζόμενες συνιστώσες. Το COSPAN μπορεί να χρησιμοποιηθεί για την ανάπτυξη περιγραφών υψηλού επιπέδου, για την ανάλυση της λογικής και στοχαστικής συμπεριφοράς συστημάτων, και προαιρετικά για την παραγωγή πολύ αποδοτικών υλοποιήσεων σε κατευθείαν από την περιγραφή υψηλού επιπέδου. Το εργαλείο χρησιμοποιεί μια τυπική, ιεραρχική, αναλυτική μέθοδο ανάπτυξης. Η λογική ανάλυση στο COSPAN επιτυγχάνεται μέσω συμβολικού ελέγχου της περιγραφής του συστήματος ως προς την επιθυμητή συμπεριφορά που καθορίζει ο χρήστης. Το σύστημα δεν προσομοιώνεται ούτε υλοποιείται, αλλά κατασκευάζεται μια μαθηματική απόδειξη που επιβεβαιώνει (ή διαψεύδει) την ύπαρξη της υπό εξέταση συμπεριφοράς. Στους αλγόριθμους ανάλυσης του COSPAN χρησιμοποιούνται τυπικές τεχνικές αναγωγής που μπο να ανταπεξέλθουν στο συνήθως τεράστιο πλήθος καταστάσεων των συντονιζόμενων συστημάτων. Το μοντέλο επαυξάνεται ώστε να συμπεριληφθούν περιορισμοί πραγματικού χρόνου. Περιγράφουμε την έννοια των λογικών μετρητών χρόνου ( logical timers ) Di89 που είναι πλασματικές συνιστώσες και χρησιμοποιούνται για την παρακολούθηση των χρόνων κατά τους οποίους συμβαίνουν γεγονότα μέσα στο σύστημα. Με αυτό τον τρόπο είναι δυνατόν να αποκλειστούν υπολογιστικές ακολουθίες που παραβιάζουν τις χρονικές παραδοχές. Ετσι ένα σύστημα που μπορεί να παραβίαζε κάποιες προδιαγραφές συμπεριφοράς σε ένα μοντέλο που δεν λαμβάνει υπόψη τις σχετικές ταχύτητες των συνιστωσών, μπορεί να τις πληρεί κάτω από ορισμένες χρονικές παραδοχές. Στη συνέχεια παρέχουμε όλες λεπτομέρειες σχετικά με την υλοποίηση του μοντέλου διαδικασιών με χρόνο (timed processes) που κατασκευάζουμε χρησιμοποιώντας το COSPAN. Το νέο εργαλείο RTCOSPAN έχει υλοποιηθεί χωρίς τροποποιήσεις της εσωτερικής δομής του COSPAN ή της γραμματικής του δείχνοντας έτσι ότι επεκτάσεις καλά σχεδιασμένων εργαλείων επαλήθευσης είναι δυνατές. Το RTCOSPAN είναι συμβατό με το COSPAN. Παρουσιάζουμε το τμήμα της διασύνδεσης χρήστη-εργαλείου (user-interface) που εισάγει τα νέα χαρακτηριστικά του RTCOSPAN, τη φιλοσοφία σχεδίασης μέσω της οποίας το RTCOSPAN ανταπεξέρχεται το μεγάλο πλήθος καταστάσεων που απαιτούν οι μετρητές χρόνου, και δίνουμε αρκετές λεπτομέρειες των εσωτερικών δομών δεδομένων και αλγορίθμων του εργαλείου. Τέλος αναφέρουμε μερικά προβλήματα και περιορισμούς της τωρινής υλοποίησης μας. Η μέθοδος μας χρησιμοποιείται για την περιγραφή και επαλήθευση δύο συστημάτων. Το πρώτο μας παράδειγμα αποτελεί μιά επέκταση του γνωστού πρωτοκόλλου επικοινωνίας alternating--bit, η οποία περιέχει πληροφορία συνεχούς χρόνου. Το δεύτερο παράδειγμα χρησιμοποιεί δύο παράλληλα κανάλια επικοινωνίας με ακαθόριστη αλλά πεπερασμένη καθυστέρηση μετάδοσης. Για την ευκολία του αναγνώστη οι περιγραφές μας δίνονται με μορφή γράφων αντί για τη γλώσσα περιγραφής του RTCOSPAN, μια και η μετάφραση είναι απλή. Εχουμε δείξει ότι το COSPAN μπορεί να επεκταθεί ώστε να χειρίζεται περιορισμούς πεπερασμένων καθυστερήσεων με φυσικό τρόπο, και ότι το νέο σύστημα είναι σε θέση να επαληθεύσει ενδιαφέροντα παραδείγματα συστημάτων. Η βασική ιδέα του διαχωρισμού της περιγραφής σε τμήματα ανάλογα με την εξάρτηση από τον χρόνο, και η χρήση των περιοχών τιμών μετρητών για το κομμάτι που εξαρτάται από το χρόνο, μπορούν πιθανά να εφαρμοστούν και σε άλλες τεχνικές επαλήθευσης επίσης. (EL)
We present an extension of the well known selection/resolution or simply model to include timing constrains. The model is a mathematical model for concurrent processes, where a complex system may be described as a set of coupled finite state machines. A feature which makes the model extremely attractive is that the coupling between machines is described in terms of predicates on communication signals. In many cases this helps to obtain brief, concise and understandable specifications. The model is a discrete linear time model with trace semantics. A calculus is defined on processes which may be composed using a synchronous or asynchronous product operation. The model contains acceptance conditions in order to express any desired -regular property of the system. Verification consists in proving trace inclusion. Our extension consists of the integration of an existing model of dense time based on COSPAN, a well-known verification tool for concurrent systems over discrete time. COSPAN HK89,KK86,HK90 is a software tool for the specification and the verification of coordinating systems, based on the model. COSPAN may be used to develop high-level specifications, analyze logical and stochastic behavior of a coordinating system and optionally produce very efficient C-code implementations directly derived from the high level specification. The tool employs a formal, hierarchical, top/down development procedure. Logical analysis in COSPAN is carried out through symbolic testing of the specified system against a user-defined behavior. The system is neither simulated nor executed, but a mathematical proof (or disproof) of the stated behavior is produced. Formal reduction techniques are used in COSPANs' analysis algorithms, to cope with the typically vast state spaces that are encountered in coordinating systems. In this work the model is extended to include real-time constraints. We use the concept of logical timers Di89 which are fictitious components used to keep track of the possible times at which events may occur. This way it is possible to exclude computation sequences that violate the timing assumptions. Thus a system that would violate a specification in a purely speed independent model might satisfy it under certain timing assumptions. COSPAN is extended by adding an on-the-fly automatically-generated ``monitor'' process which keeps track of timing constraints so as to exclude system behaviors that are inconsistent with the timing information. We present all the details about the implementation of the verification procedures for the timed process model build using COSPAN. The resulting new tool RTCOSPAN has been implemented without need to modify COSPAN's internal structure or the grammar, showing that dense time extensions of well designed verification tools are possible. RTCOSPAN is backwards compatible with COSPAN. We present the user-interface used to introduce the new features of RTCOSPAN, the design philosophy used to cope with the large state-spaces timers require, and provide enough details of the tool's internal data structures and algorithms. Finally we pinpoint certain bugs and limitations present in our current implementation. Our method is used for the specification and verification of two systems. The first example is an extension of the well known alternating--bit communication protocol which includes timing information, and the second example employs two parallel communication channels with arbitrary but finite transmission delays. To facilitate the reader our specifications are given in terms graphs instead of the RTCOSPAN specification language, since such a translation is straightforward. We have shown that COSPAN can be extended to handle bounded delay constraints in a natural manner, and that the resulting system can verify interesting example systems. The basic approach of separating the timing-independent and timing-dependent parts of the specification, and using the timer region construction for the timing-dependent part, can probably be applied to other verification methods, as well. (EN)

text

Αλγοριθμική και Ανάλυση Συστημάτων

Πανεπιστήμιο Κρήτης (EL)
University of Crete (EN)

1992-09-01
1997-06-2




*Η εύρυθμη και αδιάλειπτη λειτουργία των διαδικτυακών διευθύνσεων των συλλογών (ψηφιακό αρχείο, καρτέλα τεκμηρίου στο αποθετήριο) είναι αποκλειστική ευθύνη των αντίστοιχων Φορέων περιεχομένου.