Desenvolvimento de Software Embarcado Utilizando UPPAAL para uma Máquina de Selective Laser Melting

Abstract

Trabalho desenvolvido no Fraunhofer - Institut für Produktionsanlagen und Konstruktions- technik (IPK), Berlim - Alemanha. A empresa oferece soluções de sistemas orientados às

aplicações industriais. Este trabalhado tem como objetivo a modelagem de uma máquina de Selective Laser Melting (SLM) em autômatos temporizados, tradução de requisitos em lógica temporal, modelagem dos sistemas e, por fim, programação em sistemas embarcados. O projeto teve início com estudos teóricos. Com o conhecimento adquirido, iniciou-se o processo de entendimento dos diversos sistemas que faziam parte da máquina. Após esse mapeamento foram verificados quais eram os principais inputs e outputs de cada um deles, entendendo a interação de cada um com os demais. Os modelos em autômatos temporizados foram gerados através do software UPPAAL. Então utilizou-se o model checker desse mesmo programa para verificar formalmente se os requisitos do sistema estavam sendo atendidos. Após a verificação formal, iniciou-se a etapa de comunicação serial com Arduino. Com o objetivo de simular com cada uma das placas eletrônicas um sistema da máquina de SLM e emular seu funcionamento. Os resultados foram satisfatórios, com todos os sistemas da máquina mapeados, modelados, verificados formalmente, e comunicando com o computador central e programação em C operando de forma satisfatória.

Report developed at Fraunhofer - Institut für Produktionsanlagen und Konstruktionstech- nik (IPK), Berlin - Germany. The company offers application-oriented system solutions

covering industrial usage. This report’s objective is the modelling of a Selective Laser Melt- ing machine (SLM) using timed automaton and programming in embedded systems. The

project began with theoric studies.With the knowledge required, the process to understand the several systems from the machine began.After the process mapping it was verified what were the main inputs and outputs from each one of them, understanding the interaction among them.The models with timed automaton were generated through UPPAAL software. Moreover, the Model Checker was used from the same software to formally verify if the requirements were being attended. With the properties verification concluded the project’s second step began, the serial communication in Arduino.The objective was to simulate with each Arduino a system from the SLM Machine and emulate its operation. The results were satisfactory, with all the machine’s system mapped, modelled, with properties verified, communication with the central computer working and modeling programmed in C operating in a satisfactory way.