A strategy for local analysis of determinism

• Ano de defesa: 2018
• Autor(a) principal: OTONI, Rodrigo Benedito
• Orientador(a): SAMPAIO, Augusto Cezar Alves
• Tipo de documento: Dissertação
• Tipo de acesso: Acesso aberto
• Idioma: eng
• Instituição de defesa: Universidade Federal de Pernambuco
• Programa de Pós-Graduação: Programa de Pos Graduacao em Ciencia da Computacao
• País: Brasil
• Palavras-chave em Português: Engenharia de software; Linguagem de programação
• Link de acesso: https://repositorio.ufpe.br/handle/123456789/31427

Nondeterminism is an inevitable constituent of any theory that describes concurrency. For the validation and verification of concurrent systems, it is essential to investigate the presence or absence of nondeterminism, just as much as it is in the case of properties such as deadlock and livelock. CSP is a well established process algebra that offers rich semantic models, capable of capturing a wide range of sources of nondeterminism. The approach taken by the main tool for practical use of CSP, the model checker FDR, it to check for determinism through global analysis, which limits its scalability. In this dissertation we propose a local analysis strategy to check for determinism in specifications written in a practical subset of CSP. Our goal is to provide an efficient and scalable method of checking for determinism. We use a compositional approach in which we start from basic deterministic processes and check whether any of the composition operators used in the specification can introduce nondeterminism. The use of controlled subsets of selected notations is a common feature of local analysis, with the subset of CSP captured by our strategy containing most of the main operators of CSP, and thus being capable of modelling real world systems. Furthermore, our strategy is sound, according to our empirical evaluation, but not complete; giving up completeness is also a usual compromise of compositional approaches to analysis, as a way to improve efficiency. We present here our strategy, the prototype developed to allow its automation, and the results of a number of experiments. There are two main aspects of our strategy: its metadata, and its algorithms. After a process of the CSP specification is checked to be deterministic, we gather metadata about it. The metadata stores all the information of a process that is relevant to our strategy, and is the only element used when checking further compositions. For each composition operator available in our subset of CSP, we have developed a specific algorithm to check if the composition is deterministic. By the use of metadata, we remove the need to check the operands at each composition, relying only on the information previously gathered, and thus achieving an efficient compositional approach. A number of case studies, both toy problems and systems described in the literature, have been performed. We compared our prototype with FDR in all the experiments. For most examples our prototype is capable of analysing instances that FDR is not able to, due to lack of memory resulting from the state explosion. In some cases, our prototype is capable of analysing instances up to three orders of magnitude higher. For most instances in which both tools provide a result, besides the trivial ones, our prototype is more efficient than FDR, with some cases where FDR takes more than twenty minutes to reach a result, and our prototype requires only a few seconds.