logo SBA

ETD

Archivio digitale delle tesi discusse presso l’Università di Pisa

Tesi etd-05182014-204315


Tipo di tesi
Tesi di dottorato di ricerca
Autore
MEZZETTI, GIANLUCA
URN
etd-05182014-204315
Titolo
Nominal Context-Free Behaviour
Settore scientifico disciplinare
INF/01
Corso di studi
SCIENZE DI BASE
Relatori
tutor Degano, Pierpaolo
relatore Prof. Ferrari, Gian Luigi
Parole chiave
  • automata
  • model-checking
  • nominal
Data inizio appello
16/06/2014
Consultabilità
Completa
Riassunto
This thesis investigates and proposes models for programming and verifying adaptive software at different abstraction levels.
First, we design the kernel of a programming language, endowed with primitives for programming the adaptation to different working environments.
We provide the language with a type and effect system that allows us to statically prove properties of the behaviour of the program when plugged in different execution environments.
Then we extend our language to program the use of the resources currently available in the environment.
In this case, the identity and the number of resources is unknown a-priori.
The previous analysis technique needs to be extended to capture the behaviour of these programs.
We exploit nominal techniques in the literature to propose novel automata models that represent the behaviour and the properties of programs that use an unbounded number of unknown resources as (regular and context-free) set of traces.
The theoretical properties of these automata are investigated and related with static program verification.
We prove that we are able to check regular properties of the usage patterns of the resources when resource reuse is inhibited.
File