1. Skip to Menu
  2. Skip to Content
  3. Skip to Footer

Defesa de Dissertação de Mestrado - Erick Simas Grilo

29/06/2021, 10:00h, por videoconferência. Link para defesa: https://meet.google.com/jxq-hrmj-asy

ReLo: a Dynamic Logic to Reason About Reo Circuits

Resumo:

Sistemas críticos requerem alta confiabilidade e estão presentes nos mais variados domínios. Em suma, são sistemas cuja falha em atender requisitos específicos podem levar a perdas financeiras e até mesmo de vidas. Técnicas padrão de engenharia de software não são o suficiente para garantir a ausência de falhas inaceitáveis e/ou que requisitos críticos sejam satisfeitos.

Reo é uma linguagem de modelagem baseada em componentes cujo objetivo é prover um framework para a construção de software baseada em sistemas já existentes, abordagem esta que costuma ser usada em uma variedade de domínios. As semânticas formais de Reo permitem que sistemas baseados em modelos Reo possam ter suas propriedades desejadas verificadas. Estas verificações podem ser feitas no sistema como um todo ou apenas considerando parte dele.

As abordagens existentes para raciocinar sobre models Reo utilizando lógicas requerem a conversão de uma semântica formal para um framework lógico. ReLo é uma lógica dinâmica que naturalmente subsume a semântica de Reo  e propicia meios para o raciocínio sobre modelos Reo.

Este trabalho apresenta ReLo, uma lógica dinâmica projetada para raciocinar sobre modelos Reo, denotando uma semântica formal para Reo, apresentando suas provas de corretude e completude, um procedimento de provas sintáticas baseado em Tableaux, a prova de corretude e completude deste sistema, e uma implementação de ReLo no assistente de provas Coq, permitindo a modelagem e o raciocínio sobre modelos Reo em automatizada através de ReLo em um ambiente computacional.

Abstract:

Critical systems require high reliability and are present in many domains. In other words, systems which failure may result in financial damage or even loss of lives. Standard techniques of software engineering are not enough to ensure the absence of unacceptable failures and/or that critical requirements are fulfilled.

Reo is a component-based modelling language that aims to provide a framework to build software based on existing pieces of software, which has been used in a wide variety of domains. Its formal semantics provides grounds to certify that systems based on Reo models satisfy specific requirements. It enables the modelling of systems that require guarantees regarding specific properties that they must meet. These guarantees may be obtained by formal verification of the system (or its required parts).

Current logical approaches for reasoning over Reo require the conversion of a formal semantics into a logical framework. ReLo is a dynamic logic that naturally subsumes Reo's semantics. It provides an environment to reason over Reo circuits.

This work proposes ReLo, a dynamic logic tailored to reason over Reo models which serves as a Reo formal semantics, presenting its soundness and completeness proofs, a Tableaux-based deductive system followed by its soundness and completeness proofs, and an implementation of ReLo in the Coq proof assistant, leading to the modelling and verification of ReLo models in a computational environment.

Banca  examinadora:

Prof. Bruno Lopes Vieira, UFF – Presidente
Prof. Mario Roberto Folhadela Benevides, UFF
Prof. Igor Machado Coelho, UFF
Prof. Cláudia Nalon, UnB
Prof. Edward Hermann Haeusler, PUC-Rio

PESQUISA PELO SITE

MENU

Início Instituto Laboratórios Departamento
Pesquisa Pós-Graduação Graduação Fale Conosco

CONTATO

IC-Mapa

Av. Gal. Milton Tavares de Souza, s/nº
São Domingos - Niterói - RJ
CEP: 24210-346

IC-UFF-Telefone-icone Fale Conosco

 Como Chegar

CONECTE-SE

IC-Conecte-se-Facebook IC-Conecte-se-Twitter

LINKS

Faperj Lattes Finep SBC PROGRAD
CAPES CNPQ SIAPENET IDUFF NDC

 

Desenvolvido por pela equipe de Suporte Técnico do Instituto de Computação - suporte.ic.uff.br - Web Designer: Emanuel Machado