δείτε την πρωτότυπη σελίδα τεκμηρίου στον ιστότοπο του αποθετηρίου του φορέα για περισσότερες πληροφορίες και για να δείτε όλα τα ψηφιακά αρχεία του τεκμηρίου*
A Translation Scheme Between Two Real-Time Formalisms
Ένα Μεταφραστικό Σχήμα Μεταξύ Δύο Μεθόδων Περιγραφής Συστημάτων Πραγματικού Χρόνου
Χατζάκη, Μάγδα
(EL)
Chatzaki, Magda
(EN)
Κ. Κουρκουμπέτης
Computer programs are more and more used to manipulate real-time applications such as telecommunication applications, banking systems etc. The design of ``correct systems'' has become a very important issue. One can state that a system is correct if it preserves a number of properties. Proving correctness is a non-trivial task because of the complex and non deterministic behavior of the systems. Automatic verification methods have been developed in order to answer the question whether the system is correct or not. The four basic elements that an automatic verification method must assume are, a model for the time quantity, a language for modeling the system, a language for modeling the desired properties and a verification algorithm. In this thesis, we deal with two particular automatic verification formalisms. The first formalism uses timed automata (timed graphs) for modeling the system, TCTL formulas for modeling the properties and adopts a symbolic model checking verification algorithm. The verification tool KRONOS implements the above formalism. The second one uses a different version of timed automata, namely the Set/Expire timed automata for modeling real-time systems and their properties and adopts an automata oriented verification algorithm which solves the language inclusion problem. The verification tool RT-COSPAN implements this formalism. The two methods differ in the system description languages and also in the verification algorithms. That is why each formalism is suited better to different cases of real-time systems. In order to compare their efficiency and performance we have to deal with the unification problem of these two formalisms. This thesis addresses the following issues: First of all we propose an extension of the Set/Expire timed automata which improves the expressiveness of the traditional Set/Expire timed automata and has the property that can be analyzed using a slightly different version of RT-COSPAN which we implement. Further more we propose a syntax directed translation scheme that transforms a timed automata specification to a specification written in our model. In this way we can use both verification tools RT-COSPAN and KRONOS on a common description of a real-time system depending on what we want to verify. Finally we try a comparison of the two methods through experimental results.
(EL)
Σχολή/Τμήμα--Σχολή Θετικών και Τεχνολογικών Επιστημών--Τμήμα Επιστήμης Υπολογιστών--Μεταπτυχιακές εργασίες ειδίκευσης
*Η εύρυθμη και αδιάλειπτη λειτουργία των διαδικτυακών διευθύνσεων των συλλογών (ψηφιακό αρχείο, καρτέλα τεκμηρίου στο αποθετήριο) είναι αποκλειστική ευθύνη των αντίστοιχων Φορέων περιεχομένου.
Βοηθείστε μας να κάνουμε καλύτερο το OpenArchives.gr.
