Corso di Laurea Magistrale in Ingegneria dell’Automazione DM 270 Formal modeling of system properties for simulation-based verification of requirements: an integrated tool-chain and its application to the aerospace context Modellazione formale di proprietà di sistema per Modellazione formale di proprietà di sistema per la verifica dei requisitimediante simulazione: la verifica dei requisiti mediante simulazione: una soluzione integrata ed una sua applicazione una soluzione integrata ed una sua applicazione inambito aerospaziale in ambito aerospaziale Relatore Candidato Prof. Alfredo Garro Francesco Aiello, matricola n. 167479 Anno Accademico 2016 - 2017 Copyright c held by the author 1 abstract Modeling of system properties deals with formally expressing constraints and requi- rements that influence and determine the structure and behavior of a system. System Property Models enable the verification of system properties through real or simulated experiments so as to support their evaluation during system design and their monito- ring during system operation. However, several challenges should be addressed to effectively handle systems properties with the support of an integrated tool-chain. In this context, the thesis work, developed through an internship at Siemens PLM Software in Belgium, has the purpose to study and experiment solutions useful to enable the formal modeling of system properties, for the simulation-based verification of requirements. A tool-chain based on Modelica and a related workflow have been implemented to experiment a reference approach to the aerospace context. The ap- proach for simulation-based verification of requirements, comes from the MODRIO project. The solution is applied to evaluate different design variants of a trailing-edge high-lift system. In particular, two ways to feed the requirements model are explored: in an early phase, data series are used to evaluate the requirements themselves; then a co-simulation of the requirements model with the 3D-model of the system is used to evaluate and identify what design variants best meet the system requirements. introduzione Per affermarsi nel mercato competitivo di oggi, le imprese devono adattarsi a cam- biamenti tecnologici rapidi e soddisfare una continua richiesta di nuovi prodotti e tecnologie. Le innovazioni accrescono la complessità dei sistemi cyber-fisici. La com- plessità deriva dai sottosistemi che li costituiscono, in quanto essi sono sempre più eterogenei, interdipendenti e interconnessi. Si pensi ad esempio ai sistemi nel campo aerospaziale o automotive: essi sono caratterizzati da architetture fisicamente distri- buite e funzionalmente integrate, che includono componenti meccanici, elettronici e software soggetti a continuo rinnovamento. È intuibile come i requisiti correlati e le proprietà da soddisfare diventino articolati e numerosi. Essi solitamente sono guidati dalle aspettative dei clienti, le restrizioni sulla sicurezza, le normative soprattutto di tutela ambientale. Mantenere la coerenza tra i requisiti e il sistema nelle varie fasi di progetto diventa pro- gressivamente difficile e improduttivo se si adotta un approccio basato su documenti e specifiche in linguaggio naturale. Ciò non consente di scoprire errori e/o inconsisten- ze di integrazione che si manifestano solo nelle fasi avanzate di sviluppo, generando costi per la loro correzione. Per affrontare queste sfide, le metodologie ingegneristiche finalizzate al progetto di sistemi complessi fanno crescente uso di strumenti software di modellazione e simulazione al fine di anticipare il comportamento, ancor prima di realizzare un prototipo. I principali obiettivi mirano a supportare la validazione fun- zionale, la verifica del progetto rispetto i requisiti, il test, il collaudo, l’analisi in caso di guasti e/o anomalie. La modellazione di proprietà tratta vincoli espressi formalmente 2 nonché requisiti che influenzano e determinano la struttura e il comportamento di un sistema. I modelli di proprietà abilitano la verifica dei requisiti attraverso esperimenti reali o simulati, al fine di supportare la loro valutazione durante le fasi di progetto e il monitoraggio in sede di operatività. contributo del lavoro di tesi Nel contesto appena delineato, il lavoro di tesi, svolto in larga parte presso Siemens PLM Software in Belgio, nell’ambito di un tirocinio semestrale, si propone di studiare e sperimentare soluzioni che consentano la modellazione formale di proprietà di sistema, per la verifica dei requisiti mediante simulazione. Le domande chiave cui bisogna rispondere sono: Il software Teamcenter è in gra- do di supportare la verifica di requisiti tramite simulazione? In caso negativo, quali sforzi dovrebbero esser compiuti per integrare tale caratteristica nel portfolio software Siemens? Com’è definita la tool-chain che consente la verifica tramite simulazione? In quale ambiente software vengono modellati formalmente i requisiti? In quale avviene la simulazione? Quali caratteristiche del sistema possono essere considerate per questo tipo di analisi? È possibile definire delle regole, buone norme, linee guida per tracciare un modello formale di proprietà a partire da delle specifiche di requisiti informali e in linguaggio naturale? L’elaborato affronta tali tematiche presentando una possibile soluzione. In un primo stadio, il lavoro ha previsto lo studio e la sperimentazione di Teamcenter (software Sie- mens atto a semplificare la gestione del ciclo di vita dei sistemi), al fine di investigarne le potenzialità rispetto una metodologia di progetto e proporre possibili evoluzioni attuabili da Siemens. Nella seconda fase, è stata messa a punto una tool-chain che per- mette la modellazione di requisiti in linguaggio Modelica e la loro susseguente verifica basata su simulazione, con gli strumenti software del portfolio Siemens. La soluzione è stata sperimentata nel contesto aerospaziale per valutare diverse va- rianti di progetto del dispositivo di incremento della portanza di un velivolo da tra- sporto commerciale, rispetto i requisiti prestabiliti. La simulazione distribuita (Co- Simulation) tra il modello dei requisiti e il modello 3D del sistema, definiti in due ambienti software differenti, ha consentito di determinare quale variante di design rispettasse meglio i requisiti, dunque la possibilità di confrontare le diverse soluzioni. Parte dei risultati del lavoro di tesi è stata divulgata mediante una pubblicazione su rivista scientifica: [9] F. Aiello, A. Garro, Y. Lemmens, S. Dutré. Simulation-based verification of system requirements: an integrated solution. Proceedings of the 2017 IEEE 14th International Conference on Networking, Sensing and Control (ICNSC 2017), Calabria, Italy, May 16-18, 2017. 3 organizzazione tesi L’elaborato è strutturato nel modo seguente: il secondo capitolo (Ingegneria dei Sistemi) presenta le problematiche affrontate dal- l’Ingegneria dei Sistemi, scienza che mira a fornire soluzioni per la progettazione, creazione e gestione di sistemi complessi. Sono riportate alcune metodologie di progettazione, lo stato dell’arte e la letteratura a riguardo. il terzo capitolo (Linguaggi di modellazione e strumenti di simulazione utilizzati) for- nisce una panoramica su quanto adoperato nel prosieguo dell’elaborato per ot- tenere una soluzione in grado di rispondere agli obiettivi posti. Ci si sofferma pertanto sulla modellazione formale dei requisiti e una possibile implementazio- ne in Modelica. Vengono descritti gli ambienti software del portfolio Siemens utilizzati per la modellazione e simulazione. il quarto capitolo (Progettazione RFLP in Siemens Teamcenter) tratta la sperimenta- zione del software Teamcenter al fine di investigarne le potenzialità rispetto ad un particolare approccio di progettazione. Vengono discussi i punti di forza e le possibili evoluzioni che Siemens potrebbe attuare al fine di integrare la verifica dei requisiti. il quinto capitolo (Verifica di requisiti di sistema basata su simulazione) contiene tutto ciò che concerne la soluzione che abilita la modellazione formale di requisiti in Modelica e la loro verifica basata su simulazione, nonché la sua concreta speri- mentazione al fine di valutare diverse varianti di progetto del componente di un velivolo da trasporto commerciale. Si presenta dunque il modello del sistema uti- lizzato con le sue caratteristiche, i requisiti implementati ed infine le simulazioni, coi risultati ottenuti e le considerazioni del caso. conclusioni sintetizza il lavoro svolto, mettendo insieme le diverse scoperte e dedu- cendo le loro implicazioni. Vengono delineati i possibili lavori futuri. l’appendice riporta gli artefatti definiti per la sperimentazione compiuta con il soft- ware Teamcenter e l’articolo scientifico [9] pubblicato negli atti della “14th IEEE International Conference on Networking, Sensing and Control May 16-18, 2017, Cala- bria, Southern Italy”, risultato dell’attività di tesi.