Il linguaggio Alloy come ausilio nella specifica formale di modelli UML

UML è ampiamente considerato lo standard de facto nella fase iniziale di modellazione di sistemi software basati sul paradigma Object-Oriented; il suo diagramma delle classi è utilizzato per la rappresentazione statica strutturale di entità e relazioni che concorrono alla definizione delle specifiche del sistema; in questa fase viene utilizzato il linguaggio OCL per esprimere vincoli semantici sugli elementi del diagramma. Il linguaggio OCL però soffre della mancanza di una verifica formale sui vincoli che sono stati definiti. Il linguaggio di modellazione Alloy, inserendosi in questa fase, concettualmente può sopperire a questa mancanza perchè può descrivere con le sue entità e relazioni un diagramma delle classi UML e, tramite propri costrutti molto vicini all'espressività di OCL, può specificare vincoli semantici sul modello che verranno analizzati dal suo ambiente l'Alloy Analyzer per verificarne la consistenza. In questo lavoro di tesi dopo aver dato una panoramica generale sui costrutti principali del linguaggio Alloy, si mostrerà come è possibile creare una corrispondenza tra un diagramma delle classi UML e un modello Alloy equivalente. Si mostreranno in seguito le analogie che vi sono tra i costrutti Alloy e OCL per la definizione di vincoli formali, e le differenze, offrendo nel complesso soluzioni e tecniche che il modellatore può utilizzare per sfruttare al meglio questo nuovo approccio di verifica formale. Verranno mostrati anche i casi di incompatibilità. Infine, come complemento al lavoro svolto verrà mostrata, una tecnica per donare una dinamicità ai modelli statici Alloy.

Development of a novel heat treatment for high performances L-PBF Ti6Al4V alloy: microstructural and mechanical characterization

This work presents the experimental development of a novel heat treatment for a high performance Laser Powder Bed Fusion Ti6Al4V alloy. Additive manufacturing production processes for titanium alloys are particularly of interest in cutting-edge engineering fields, however, high frequency laser induced thermal cycles generate a brittle as built microstructure. For this reason, heat treatments compliant with near net shape components are needed before their homologation and usage. The experimental campaign focused on the development of a multi-step heat treatment leading to a bilamellar microstructure. In fact, according to literature, such a microstructure should be promising in terms of mechanical properties both under static and cyclic loads. The heat treatment development has asked for the preliminary analyses of samples annealed and aged in laboratory, implementing several cycles, differing for what concerns temperatures, times and cooling rates. Such a characterization has been carried out through optical and electron microscopy analyses, image analyses, hardness and tensile tests. As a result, the most suitable thermal cycle has been selected and performed using industrial equipment on mini bending fatigue samples with different surface conditions. The same tests have been performed on a batch of traditionally treated samples, to provide with a comparison. This master thesis activity has finally led to the definition of a heat treatment resulting into a bilamellar microstructure, promising in terms of fatigue performances with respect to the traditionally treated alloy ones. The industrial implementation of such a heat treatment will require further improvements, particularly for what concerns the post annealing water quench, in order to prevent any surface alteration potentially responsible for the fatigue performances drop. Further development of the research may also include push-pull fatigue tests, crack grow propagation and residual stresses analyses.