Calculus semantic with values passing in the denotational approach

Abstract

In 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.

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.