Bruno Pinna (brunopinna@ieee.org) Bruno Pinna è nato a Cagliari l'11 Agosto 1987. Ha conseguito la Laurea Magistrale in Ingegneria Elettronica a Novembre del 2014 presso il Dipartimento di Ingegneria Elettrica ed Elettronica dell'Universitá degli Studi di Cagliari. Ha sviluppato la sua tesi di laurea magistrale presso il Centre de Recherche en Automatique de Nancy (CRAN) dell'ENSEM, Université de Lorraine.

Tesi di Laurea Magistrale / Master Thesis

Deterministic and probabilistic dependability assessments of a critical system [pdf] [slides]

Relatori / Advisors

• Prof. Alessandro Giua (DIEE-UNICA)
• Prof. Nicolae Brînzei (CRAN-Université de Lorraine)
• Prof. Jean-François Pétin (CRAN-Université de Lorraine)
• Ph.D. Génia Babykina (CRAN-Université de Lorraine).

Software

CPN Tools

• Software
• Model

Pubblicazioni

• [ESREL13] B. Pinna, G. Babykina, N. Brinzei, J.-F. Pétin, "Deterministic and stochastic dependability analysis of industrial systems using Coloured Petri Nets approach", Annual Conference of the European Safety and Reliability Association, ESREL 2013, Sep 2013.
• [DCDS13] B. Pinna, G. Babykina, N. Brinzei, J.-F. Pétin, "Using Coloured Petri Nets for integrated reliability and safety evaluations", 4th IFAC Workshop on Dependable Control of Discrete Systems, DCDS'13, Sep 2013.

Riconoscimenti

EFNMS Excellence Award 2014
Best Master thesis in maintenance: Joint-Winner, Mr.Bruno Pinna

Deterministic and probabilistic dependability assessments of a critical system

Abstract

The aim of the present work is to build a Coloured Petri net (CPN) model of a critical system and to perform two tasks: an analysis of the system's performance and a formal verication of the model. The case study system used for these purposes is composed of two components functioning in a parallel conguration, thus allowing to improve the whole system's reliability. The physical model of system's behaviour (with failures and reparations) and the logical model of its behaviour are implemented as two dierent CP nets in a software named CPN Tools. We will see that a single CPN model is not sucient to perform the two tasks. Thus, two model are developed. The rst model is used to carry out the performance analysis and the second CPN model will be used to carry out the formal model verication. While the system's performance analysis can be performed using CPN Tools and MATLAB, the formal verication is performed by three dierent tools: the CPN Tools integrated state space tool, ASAP tool, and the software ProM. We will see that the formal model verication is quite complicated and none of the three tools perform a reliable, formal, easily implemented analysis. We can however perform a formal model verication, but the improvements of the available documentation (especially for ASAP) are necessary to exploit all the capabilities of these tools.

Deterministic and probabilistic dependability assessments of a critical system

Sommario

Lo scopo di questo lavoro di tesi é quello di realizzare un modello di Rete di Petri Colorata (CPN) per un sistema critico con due obiettivi : l'analisi delle prestazioni temporali del sistema e la verica formale del modello. Il caso di studio del sistema discusso in questo lavoro di tesi é composto da due componenti disposti in congurazione parallela, questo ci permette di migliorare l'affidabilitá complessiva del sistema. Il modello del sistema é descritto da due reti CPN, uno per il comportamento sico (con i guasti e le riparazioni) ed uno per la parte logica (esempio, la partenza e lo stop delle macchine) il tutto é stato implementato con il software CPN Tools. Abbiamo visto che, un solo modello di sistema con reti CPN non era suciente per vericare i nostri due obiettivi. Perciò, sono stati sviluppati due modelli. Il primo medello é usato per l'analisi delle prestazioni temporali e il secondo modello invece per la verica formale. L'analisi delle prestazioni del sistema sono state fatte usando CPN Tools e MATLAB, mentre la verica formale é stata eettuata con tre diversi software: lo state space tool integrato in CPN tool, l'estensione ASAP ed il software ProM. Abbiamo visto che la verica formale é abbastanza complessa e nessuno di questi tre tools ci permette di ottenere risultati adabili, formali e facili da ottenere. In ogni caso possiamo fare delle prove di verica formale , ma il miglioramento della documentazione disponibile (sopratutto per il tool ASAP) é una condizione indispensabile per poter sfruttare al massimo le capacitá di questi tools.

back