Bando per assegno di ricerca
Titolo del progetto di ricerca in italiano | Model-checking di logiche stocastiche e applicazione alla verifica dei sistemi |
---|---|
Titolo del progetto di ricerca in inglese | Model-checking di logiche stocastiche e applicazione alla verifica dei sistemi |
Settore Concorsuale | 01 - Scienze matematiche e informatiche |
S.S.D | - |
Descrizione sintetica in italiano | Obiettivo della ricerca e' arrivare ad una categorizzazione delle logiche stocastiche esistenti e, sulla base di questa, individuare le possibili applicazioni per la verifica dei sistemi. Per quanto riguarda la categorizzazione delle logiche, verranno prese in considerazione diverse logiche stocastiche, fra cui CSL, asCSL, CSLTA a clock singolo e CSLTA a clock multipli. L'obiettivo e' confrontare i diversi poteri espressivi di queste logiche per l'espressione di proprieta' di cammino e sviluppare algoritmi comuni per il model-checking di queste logiche. In particolare si provera' ad applicare recenti tecniche di soluzione per processi stocastici rigenerativi Markoviani a clock multiplo per il model checking di CSLTA. Per quanto riguarda la verifica dei sistemi gli sforzi si concentreranno sulla relazione fra le proprieta' stocastiche di cammino e le tecniche di analisi "tagged customer" nonche' sulla generazione automatica di tali proprieta' a partire da specifiche UML. |
Descrizione sintetica in inglese | The research is aimed at a categorization of the existing stochastic logics, and of its possible application to system verification. For what concern the comparison of the logics, we shall consider at least CSL, asCSL, CSLTA single clock and CSLTA with multiple clocks. The objective is to compare the expressive power of the logics in describing path properties and to develop common algorithms for the model-checking of the studied logics. In particular we shall investigate the possibility of exploiting recent results on the analysis of Markov regenerative and non-regenerative processes for the model-checking of CSLTA with multiple clocks. For what concerns the applicaiton to system verification, the objective is to investicate the relationship and the use of path properties in the systems' analysis based on tagged customer and on the derivation of path properties from UML specifications. |
Data del bando | 14/11/2012 |
Numero di assegnazioni per anno | 1 |
Paesi in cui può essere condotta la ricerca |
Italy |
Paesi di residenza dei candidati |
All |
Nazionalità dei candidati |
All |
Sito web del bando | https://www.serviziweb.unito.it/albo_ateneo/ |
Destinatari dell'assegno di ricerca (of target group) |
Early stage researcher or 0-4 yrs (Post graduate) |
---|---|
Il contratto prevede la copertura delle prestazioni sociali? | yes |
Importo annuale | 19367 |
Valuta | Euro |
Comprende lo stipendio dell'assegnista | yes |
Comprende vitto e spese di viaggio | yes |
Comprende il costo della ricerca | yes |
Altri costi in italiano | \ |
Altri costi in inglese | \ |
Massima durata dell'assegno (mesi) | 24 |
Criteri di selezione in italiano (breve descrizione) | Il bando e le modalità di iscrizione/partecipazione alla selezione sono disponibili su https://www.serviziweb.unito.it/albo_ateneo/ |
Criteri di selezione in inglese (breve descrizione) | The call and how to apply are available at the following address: https://www.serviziweb.unito.it/albo_ateneo/ |
Processo di selezione in italiano (breve descrizione) | per titoli e colloquio |
Processo di selezione in inglese (breve descrizione) | qualifications and interview (in Turin) |
Nome dell'Ente finanziatore | Universita' degli Studi di Torino |
---|---|
Tipologia dell'Ente | Public research |
Paese dell'Ente | Italy |
Città | Turin |
Sito web | http://www.unito.it/ |
arearicerca-assegni@unito.it | |
Telefono | 0 |
L'assegno finanziato/cofinanziato attraverso un EU Research Framework Programme? | No |
---|
Data di scadenza del bando | 29/11/2012 |
---|---|
Come candidarsi | https://loginmiur.cineca.it/ |