We present some original results in the framework of the specification and of the verification of real-time systems. The underlying formal model of computation is the timed automata model. It is formally introduced in detail and within a theory of timed languages. Different aspects and variants of timed automata are exposed. The main verification techniques that have been proposed in the literature are shown in details. Particular attention is dedicated to the simplifications that have been done to the theoretical model of timed automata in order to construct simulators and/or model checking tools. On the side of specification, the thesis presents two extensions of the original model of timed automata:non-instantaneous actions and urgent transitions. The first extension improves the expressive power of the formalism of timed automata and allow more precise specifications. The second one is a very useful tool in the task of the specification of typical behaviors of real-time systems. It allows writing clear and concise specifications. We show that its introduction does not increase the expressive power of timed automata. Both the extensions are defined within the theoretical model of timed automata, but it is shown that they have a similar definition also for the implementable timed automata. Moreover, they are used to specify a classical railway cross example and a multicast protocol for mobile computing. On these example we perform automatic verifications using existing model-checking tools. On the side of verification, we define a timed version of a classical security property defined on untimed systems: the non-interference property. We show how this formulation can be used to state and verify time-dependent security properties of timed systems. The definition of the timed non-interference property is given in two different formulations. The first is the clearer and more natural one, but suffers of a negative result of undecidability. The second one is effectively used in an analysis of the strength of a time-dependent mutual exclusion protocol against timed attacks.
Table of Contents
Full Text: ps ps.gz pdf
Valuation:
| External Referees: |
Danièle Beauquier,
Manfred
Droste |
Accepted |
| Internal Committee: |
Roberto Babuti, Andrea Maggiolo-Schettini,
Stefania Gnesi
|
Accepted |
| External Final Committee: |
Maria
Simonetta Balsamo, Simone
Martini, Luigi Mancini |
Accepted |
Ph.D obtained on May 28 2004
The thesis has been published by Dipartimento di Informatica - Università di Pisa, in an internal series of phd theses, Pisa, 2004.| Home |
Publications |
Research |
Phd |
Phd Thesis |
Curriculum Vitae |
Search |
Luca Tesei Last modified: Sat Oct 16 9:34:22 CEST 2004