Formal mutation testing in Circus process algebra

• Ano de defesa: 2018
• Autor(a) principal: Alberto, Alex Donizeti Betez
• Tipo de documento: Tese
• Tipo de acesso: Acesso aberto
• Idioma: eng
• Instituição de defesa: Biblioteca Digitais de Teses e Dissertações da USP
• Palavras-chave em Português: Álgebra de processos; Circus; Espeficicação formal; Formal specification; Mutation testing; Process algebra; Teste de mutação
• Link de acesso: http://www.teses.usp.br/teses/disponiveis/55/55134/tde-04012019-112931/

PROCESS algebras are a family of techniques used in formal specification and analysis of computer systems, specially when independent processes that perform and synchronize in parallel are concerned. The so-called concurrent systems. Circus is a process algebra that aggregates the expressiveness power for concurrent behaviors from CSP, along with the predicative data modelling aspects of Z. Recent publications have established a formal exhaustive symbolic testing theory for specifications modelled in Circus. Aiming to improve the feasibility of applying such tests in practical scenarios, it is convenient to look for criteria that reduces the number of test cases which, by the exhaustive nature of the approach, is often infinite. In the light of this, the work we present proposes the application of mutation testing techniques in Circus specifications, targeting the coverage of faults seeded by well-known mutation operators, along with operators designed with the particularities of the language in mind. Some contributions were produced in the pursuit of these goals, such as establishing a formal theory for mutation testing in Circus specifications and the implementation of a symbolic traces generator for the language.