Show simple item record

dc.contributor.advisorNunes, Daltro Josept_BR
dc.contributor.authorGalli, Jaqueline Kleinpt_BR
dc.date.accessioned2020-09-29T04:01:42Zpt_BR
dc.date.issued2020pt_BR
dc.identifier.urihttp://hdl.handle.net/10183/213850pt_BR
dc.description.abstractIn the last recent years, there was a noticeable increase in the use of formal verification by the industry, and the reason for that is because the formal languages are each time more enhanced, and the tools that support those languages were developed. Although there is a higher use in critical systems, the application can also avoid execution errors and, consequently, update the system with bugs’ correction as a goal. The extension of these languages makes them wider in their applicability and the creation of tools makes the use easier for lay or lack of experience users. The use of formal languages in a critical systems development ensures the operation to work and, at the same time, the benefit-cost of the time used in a formal verification of a system specification, is lower when a tool is available. The formal -Calculus method is largely used in labeled transition and mobile systems, because it shows competition, mobility and creation of new links. Even with a wide applicability, it presents some limitations for the user, for example, there is neither formal language nor tools that can support it. -Calculus is an extension of CCS (Calculus of Communication System) that shows operation semantics, however, no value passing. In this dissertation, is presented a denotational semantic for the -Calculus, based in the mapping of syntactic phrases in semantics domain through semantics function, that gives structure for a creation of a formal language. Besides that, the denotational approach makes the tools implementation much easier, as it is the case of LOTOS and Maude. Along the denotational approach, we introduce the concepts of local memory (storage), temporary memory (environment) and types of environment, providing the ideal conditions so is possible to demonstrate how the -Calculus values passing occur. Thereby it was possible to verify, in an objective way, the mobility in this method, once that is clear how the communication channels passing works, peculiarity not found at CCS.en
dc.description.abstractNos ú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.pt_BR
dc.format.mimetypeapplication/pdfpt_BR
dc.language.isoengpt_BR
dc.rightsOpen Accessen
dc.subjectPi-Calculusen
dc.subjectMetodos formaispt_BR
dc.subjectSemantica denotacionalpt_BR
dc.subjectValues Passingen
dc.subjectLinguagens formaispt_BR
dc.subjectDesenvolvimento de sistemaspt_BR
dc.titleCalculus semantic with values passing in the denotational approachpt_BR
dc.title.alternativeSemântica do cálculo com passagem de valores na abordagem denotacional pt
dc.typeDissertaçãopt_BR
dc.identifier.nrb001118447pt_BR
dc.degree.grantorUniversidade Federal do Rio Grande do Sulpt_BR
dc.degree.departmentInstituto de Informáticapt_BR
dc.degree.programPrograma de Pós-Graduação em Computaçãopt_BR
dc.degree.localPorto Alegre, BR-RSpt_BR
dc.degree.date2020pt_BR
dc.degree.levelmestradopt_BR


Files in this item

Thumbnail
   

This item is licensed under a Creative Commons License

Show simple item record