ETD system

Electronic theses and dissertations repository

 

Tesi etd-05182014-204315


Thesis type
Tesi di dottorato di ricerca
Author
MEZZETTI, GIANLUCA
URN
etd-05182014-204315
Title
Nominal Context-Free Behaviour
Settore scientifico disciplinare
INF/01
Corso di studi
SCIENZE DI BASE
Commissione
tutor Degano, Pierpaolo
relatore Prof. Ferrari, Gian Luigi
Parole chiave
  • model-checking
  • automata
  • nominal
Data inizio appello
16/06/2014;
Consultabilità
completa
Riassunto analitico
This thesis investigates and proposes models for programming and verifying adaptive software at different abstraction levels.<br>First, we design the kernel of a programming language, endowed with primitives for programming the adaptation to different working environments.<br>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.<br>Then we extend our language to program the use of the resources currently available in the environment.<br>In this case, the identity and the number of resources is unknown a-priori.<br>The previous analysis technique needs to be extended to capture the behaviour of these programs.<br>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.<br>The theoretical properties of these automata are investigated and related with static program verification.<br>We prove that we are able to check regular properties of the usage patterns of the resources when resource reuse is inhibited.<br>
File