FenixEdu™

Dissertação

{pt_PT=Coverage-based validation of embedded systems} {} EVALUATED

Detalhes: {pt=Os sistemas embebidos tornaram-se ao longo do tempo cada vez mais enraizados em vários campos de aplicação e consecutivamente mais complexos e especializados. Um exemplo disto são os equipamentos médicos, dos quais dependem vidas humanas. Assim, é crucial ter uma garantia de funcionamento adequado destes sistemas antes da sua instalação. O objetivo deste trabalho é a implementação de uma metodologia de validação para sistemas embebidos baseados numa cobertura particular. Dados uma descrição de alto nível do sistema embebido em SystemC e um nível quantitativo de cobertura com base em observabilidade, indicado pelo utilizador, o objetivo é desenvolver uma ferramenta que determina os vetores de entrada que exercem caminhos de execução, a fim de obter o nível especificado de cobertura. A solução proposta consiste inicialmente na computação de um conjunto mínimo de caminhos que alcançam o nível especificado de cobertura e, em seguida, determinar quais vetores de entrada que exercitam cada um desses caminhos. O trabalho consistirá no seguinte método recursivo: (a) Obter o grafo dirigido, sem ciclos, a partir da descrição SystemC; (b) Usando esse grafo, obter o caminho potencialmente mais abrange; (c) Obter os vetores de entrada que exerce o caminho; (d) Calcular a cobertura obtida com estes vetores. (e) Se o caminho não alcançar a cobertura desejada, repetir o procedimento para outro caminho. Da abordagem mencionada acima, conseguimos implementar com sucesso a interpretação, emulação da descrição SystemC, conseguindo assim gerar os grafos do sistema. No entanto, nesta fase a conversão de instruções para SMT ainda é feita manualmente. , en=Embedded systems have become over time increasingly rooted in various fields of application and also more complex. An example is medical equipment that human lives depend on. Therefore, it is crucial to have a guarantee of proper operation of these systems prior to installation. The aim of this work is to implement a validation methodology for embedded systems based on a particular coverage. Given a high-level description of the embedded system in SystemC and a quantitative level of coverage based on observability, specified by the user, the objective is to develop a tool that determines the input vectors exercising execution paths in order to obtain the specified level of coverage. The proposed solution consists in initially computing a minimal set of paths that reach the specified level of coverage, and then determine which input vectors exercise each of these paths. The work will consist of the following recursive method: (a) Get the corresponding directed graph without cycles, from the SystemC description; (b) Using the graph, obtain the path that potentially covers more lines of code in the SystemC description; (c) Get the input vectors that exercise the path obtained; (d) Calculate the coverage obtained with these input vectors. (e) If the path does not achieve the desired coverage, repeat procedure. From the methodology mention above, we successfully implemented the System C description interpretation and emulation in order to generate the graph. Still, we were unable to automate the conversion to SMTs to get the input vectors. }
Keywords: {pt=SystemC, Verificação, Validação, Sistemas Embebidos, en=SystemC, Verification, Validation, Embedded Systems}

Discussão: maio 29, 2015, 9:0