Teste de software concorrente orientado por modelo formal

Abstract

Sistemas multitarefa são sistemas que executam diversas tarefas concorrentemente, e estão presentes em sistemas operacionais, computação de alto desempenho, ser- vidores e sistemas embarcados. Pelo fato de as tarefas serem concorrentes, defeitos como condição de corrida, deadlock e inanição podem ocorrer, e dependem da ordem específica em que o escalonador intercala as tarefas em cada execução. Tais defeitos escapam aos testes convencionais, uma vez que uma implementação incorreta pode produzir, em uma execução isolada, a mesma saída de uma implementação correta, o que torna insuficiente a simples comparação entre saída obtida e saída esperada. Este trabalho desenvolve um sistema de testes para software multitarefa, utilizando um modelo formal em UPPAAL como oráculo de verificação. O desenvolvimento par- tiu do levantamento de requisitos e da modelagem do estudo de caso em UPPAAL, com a verificação das propriedades temporais relevantes em lógica temporal CTL. Em seguida, foi implementado em Python um framework de caixa-preta que compila e executa a implementação sob teste — ou consome diretamente os registros de exe- cução que ela produz — captura esses registros e os confronta com o espaço de estados derivado do modelo. A consistência do carregador foi validada por compara- ção cruzada com os rastros oficiais gerados pelo verificador do UPPAAL. O jantar dos filósofos foi adotado como estudo de caso por reunir os três fenômenos de interesse em um modelo de tamanho tratável.

Multitasking systems execute several tasks concurrently and are present in operating systems, high-performance computing, servers, and embedded systems. Because these tasks run concurrently, defects such as race conditions, deadlock, and starvation may arise, and they depend on the specific order in which the scheduler interleaves the tasks in each execution. Such defects escape conventional testing, since an in- correct implementation may produce, in an isolated execution, the same output as a correct one, which makes a simple comparison between the obtained output and the expected output insufficient. This work develops a testing system for multitasking soft- ware, using a formal UPPAAL model as a verification oracle. The development began with requirements elicitation and the modeling of the case study in UPPAAL, followed by the verification of the relevant temporal properties expressed in CTL (Computation Tree Logic). Next, a framework was implemented in Python that compiles the imple- mentation under test, runs the binary (one or more times, as configured), captures the execution traces, and confronts them with the state space derived from the model. The consistency of the loader was validated through cross-comparison with the offi- cial traces generated by the UPPAAL verifier. The dining philosophers problem was adopted as the case study because it brings together the three phenomena of interest in a model of tractable size.