Isaque Dias Bressy dos Santos

Idiomas

Áreas de atuação

Participação em eventos

Projetos de pesquisa

• 2007 - 2008

  Uma análise de aspectos relacionados ao projeto de sistemas e verificação de propriedades a partir de especificações em TLA e RT-Promela, Descrição: O objetivo deste trabalho é desenvolver uma especificação formal do protocolo DORIS em RT-Promela, que é uma linguagem para especificação formal utilizada pelo verificador de modelos RT-SPIN. Concluídas a especificação e verificações, estas servirão de base ao projeto do orientador, sendo realizadas comparações entre a especificação gerada e outra, em TLA (Temporal Logic of Actions), realizada pelo autor do protocolo. A idéia é que aspectos próprios de cada linguagem sejam analisados quanto a facilidades para a especificação de protocolos de comunicação com restrições temporais. A especificação em RT-Promela também servirá de base para uma implementação em linguagem de programação (C, por exemplo) para comparar com um protótipo feito a partir de TLA.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (1) . , Integrantes: Isaque Dias Bressy dos Santos - Integrante / Aline Maria Santos Andrade - Coordenador.

Projetos de desenvolvimento

• 2007 - 2008

  Especificação do Protocolo de Comunicação DoRiS em RT-Promela, Descrição: Este trabalho tem como escopo a verificação de modelos formais, a especificação de protocolos e a comunicação de Sistemas de Tempo-Real. Estes sistemas devem ter comportamentos determinísticos e previsíveis, fornecendo resultados corretos em tempos pré-determinados. A utilização de métodos formais para especificar estes sistemas vem auxiliar no seu funcionamento correto. Para tanto, é gerado um modelo do sistema, através de uma linguagem formal, realizando posteriores verificações. Verificadores de modelos são utilizados para realizarem a verificação de forma automática. Um protocolo de comunicação de sistemas críticos e não-críticos, chamado DoRiS, será o objeto de nosso estudo. Este protocolo tem como finalidade gerenciar a comunicação nestes sistemas híbridos, fornecendo garantias temporais, provendo a previsibilidade necessária e otimizando o uso do canal compartilhado. Sendo assim, este trabalho tem como objetivo gerar uma especificação formal de DoRiS em RT-Promela, realizando verificações de propriedades relativas à correção deste protocolo. , Situação: Concluído; Natureza: Desenvolvimento. , Alunos envolvidos: Graduação: (1) . , Integrantes: Isaque Dias Bressy dos Santos - Coordenador / Aline Maria Santos Andrade - Integrante., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Bolsa.

• 2007 - 2008

  Especificação do Protocolo de Comunicação DoRiS em RT-Promela, Descrição: Este trabalho tem como escopo a verificação de modelos formais, a especificação de protocolos e a comunicação de Sistemas de Tempo-Real. Estes sistemas devem ter comportamentos determinísticos e previsíveis, fornecendo resultados corretos em tempos pré-determinados. A utilização de métodos formais para especificar estes sistemas vem auxiliar no seu funcionamento correto. Para tanto, é gerado um modelo do sistema, através de uma linguagem formal, realizando posteriores verificações. Verificadores de modelos são utilizados para realizarem a verificação de forma automática. Um protocolo de comunicação de sistemas críticos e não-críticos, chamado DoRiS, será o objeto de nosso estudo. Este protocolo tem como finalidade gerenciar a comunicação nestes sistemas híbridos, fornecendo garantias temporais, provendo a previsibilidade necessária e otimizando o uso do canal compartilhado. Sendo assim, este trabalho tem como objetivo gerar uma especificação formal de DoRiS em RT-Promela, realizando verificações de propriedades relativas à correção deste protocolo. , Situação: Concluído; Natureza: Desenvolvimento. , Alunos envolvidos: Graduação: (1) . , Integrantes: Isaque Dias Bressy dos Santos - Coordenador / Aline Maria Santos Andrade - Integrante., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Bolsa.