Calculus semantic with values passing in the denotational approach

• Ano de defesa: 2020
• Autor(a) principal: Galli, Jaqueline Klein
• Orientador(a): Nunes, Daltro Jose
• Tipo de documento: Dissertação
• Tipo de acesso: Acesso aberto
• Idioma: eng
• Palavras-chave em Português: Metodos formais; Semantica denotacional; Linguagens formais; Desenvolvimento de sistemas
• Palavras-chave em Inglês: Pi-Calculus; Values Passing
• Link de acesso: http://hdl.handle.net/10183/213850

Nos últimos anos nota-se um aumento significativo na utilização de verificação formal pela indústria, pois as linguagens formais estão cada vez mais aprimoradas e ferramentas que suportem essas linguagens foram desenvolvidas. Embora tenha maior utilização em sistemas críticos, a sua aplicação também pode evitar erros de execução e, consequentemente, a atualização de sistemas com propósito de correções de bugs. As extensões dessas linguagens as tornam mais abrangentes em sua aplicabilidade e a criação de ferramentas faz com que seu uso seja mais fácil para usuários leigos ou pouco experientes no assunto. O uso de linguagens formais no desenvolvimento de sistemas críticos assegura o funcionamento do sistema e, ao mesmo tempo, o custo/benefício do tempo usado na verificação formal de uma especificação de um sistema é menor quando se tem uma ferramenta. O método formal -Cálculo é muito usado em sistemas de transição rotulada e sistemas móveis, pois apresenta concorrência, mobilidade e criação de novos links. Por mais abrangente que seja sua aplicabilidade, apresenta algumas limitações ao usuário como, por exemplo, não possui uma linguagem formal e nem ferramenta que o suporte. O -Cálculo é uma extensão do CCS (Cálculo de Sistemas de Comunicação) que apresenta semântica operacional, entretanto sem passagens de valores. Nesta dissertação, apresentamos uma semântica denotacional para o -Cálculo baseada no mapeamento de frases sintáticas em domínios semânticos através de funções semânticas, que dá estrutura para a criação de uma linguagem formal. Além disso, a abordagem denotacional facilita muito a implementação de ferramentas, como no caso do LOTOS e do Maude. Juntamente com a abordagem denotacional introduzimos os conceitos de memória (local), ambiente (temporária) e ambiente de tipos, proporcionando as condições necessárias para que pudéssemos demonstrar como se dá a passagem de valores no -Cálculo. Assim foi possível verificar de forma objetiva a mobilidade nesse método uma vez que fica claro como se dá a passagem de canais de comunicação, particularidade não encontrada no CCS.