Compilação de Código Certificado para Modelos Reo - Grillo, Erick; Lopes, Bruno (Anais da Escola Regional de Informática do Rio de Janeiro (ERI-RJ); 2019: Anais da III Escola Regional de Informática do Rio de Janeiro, 2019)
Sistemas críticos são sistemas que necessitam de alta confiabilidade e estão presentes nos mais variados domínios. Em caso de falha, tais sistemas podem provocar problemas sérios, causando prejuízos financeiros e até morte. A engenharia de software padrão não é o suficiente para garantir o nível requerido de confiabilidade. Reo é uma linguagem gráfica de modelagem baseada em coordenação cujo foco é em modelar a interação de sistemas por meio do uso de primitivas comuns em sistemas distribuídos. Constraint Automata são definidos como a semântica formal primitiva para Reo, providenciando meios formais para raciocinar sobre e provar propriedades acerca de modelos Reo. O presente trabalho descreve uma formalização de Constraint Automata no assistente de provas Coq, onde os principais formalismos da teoria são formalizados, junto de uma operação de composição.