Return to search

Metodologia para verificação funcional antecipada de software embarcado combinado plataformas virtuais e verificação formal

Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico, Programa de Pós-Graduação em Engenharia Elétrica, Florianópolis, 2016. / Made available in DSpace on 2016-09-20T04:52:02Z (GMT). No. of bitstreams: 1
339513.pdf: 5400520 bytes, checksum: a39771aa9d2c178cd0cc3b145f47c8fe (MD5)
Previous issue date: 2016 / O crescente volume e complexidade de software sendo utilizado em aplicações embarcadas introduz novos desafios para verificação. Além disso, cada vez mais sistemas controlados por software são inseridos diariamente nas nossas vidas, criando novas formas de interação e trazendo preocupações gradativas quanto integridade. Esse cenário pode ser observado pelo recente número de padrões destinados a fornecer mecanismos de segurança funcional, como exemplos os padrões ISO 26262 na área automotiva, IEC 61513 na área de geração de energia e IEC 62304 na assistência médica. Percebe-se que muitos sistemas que antes não eram tratados como críticos, devem ser desenvolvidos e verificados de tal forma atualmente. Associado a esse ponto de vista técnico, o mercado atual demanda alta produtividade e reduzido time-to-market. Assim, são necessárias alternativas que forneçam suporte ao desenvolvimento de software embarcado, considerando verificação ainda em fases iniciais do projeto. É importante perceber que isso não é somente uma exigência do mercado, pois a quantidade de erros de implementação introduzidos é muito maior durante a programação dos dispositivos do que em fases de especificação e elaboração. Levando em conta essas características, este trabalho expõe uma metodologia de desenvolvimento de software embarcado voltado para verificação nas fases iniciais de projeto, considerando ferramentas e abordagens atuais. Por parte de desenvolvimento são consideradas plataformas virtuais de simulação do sistema, as quais fornecem suporte para desenvolvimento mesmo antes do hardware final estar disponível. Essas mesmas plataformas permitem simulação de software dependente de hardware através de camadas de isolamento e modelagem de periféricos. Como a criação de plataformas virtuais é uma tarefa árdua, a linguagem de descrição de arquiteturas ArchC é utilizada para fornecer suporte a implementação de simuladores de conjunto de instruções. Do ponto de vista de verificação são utilizados métodos estáticos (i.e., Model Checking), para exploração de erros de implementação e verificação funcional com propriedades temporais. No entanto, apesar dos recentes avanços em Model Checking, limitações com relação a complexidade podem comprometer a verificação de sistemas complexos. Nesses casos, simulações e testes do sistema são conduzidos, através de plataformas virtuais, para obter maior cobertura e estresse do sistema, além é claro de fornecer informações valiosas quanto ao seu comportamento. Como resultados é demonstrado: o desenvolvimento e a verificação de um modelo baseado no microcontrolador MSP430; dois cenários de verificação híbrida de um sistema de controle de injeção de combustível; uma plataforma virtual de simulação de um sistema de controle mecânico, considerando modelos físicos integrados; e por fim, a especificação, implementação e teste de um computador de bordo de um CubeSat, um sistema consideravelmente complexo, constituído de três unidades de processamento e com um sistema operacional de tempo real. Esses resultados servem como demonstração do potencial da metodologia e evidenciam a importância de verificação nas fases iniciais de projeto.<br> / Abstract: The growing size and complexity of software being used in embedded applications introduce new verification challenges. Moreover, software-controlled systems are being inserted more and more into our daily routines, causing new forms of interaction and producing frequently integrity concerns. This outline is noticeable in the recent number of standards intended to provide functional safety mechanisms, examples are the ISO 26262 standard in the automotive industry, IEC 61513 for power generation and IEC 62304 in health care. One can see that many systems that were not treated as critical before must be treated similarly in the current situation. Associated with this technical point of view, the current market demands high productivity and reduced time-to-market. Thus, alternatives are required to provide support for the development of embedded software, considering verification even in early design stages of the project. It is important to realize that this is not only a market demand, the amount of errors of implementation introduced during programming is much higher than in specification and conceptual design. Given these aspects, this work presents an embedded software development methodology, focused on early verification considering current tools and approaches. On the development point of view, full system simulation is achieved through virtual platforms, which provide support for the development even before the final hardware is accessible. These same platforms enable simulation of hardware dependent software on isolation layers and model of the system peripherals. As virtual platform development can be a daunting task, the ArchC architecture description language is used to support the implementation of the instruction set simulators. On the verification viewpoint, static methods (i.e., Model Checking) are used to explore implementation errors and functional verification with temporal properties. Despite recent advances in model checking, limitations on the complexity could jeopardize the verification of complex systems. In such cases, simulations and tests are conducted to achieve greater coverage and stress of the system, and of course to provide valuable information about its behavior. As results are presented: the development and verification of an Instruction set Simulator for the MSP430 microcontroller; two hybrid verification scenarios of a fuel injection control system; a virtual platform simulation of a mechanical control system, considering physical models of the process; and finally, the specification, implementation, and testing of an onboard computer of a CubeSat, a rather complex system consisting of three processing units and a real-time operating system. These results serve as a demonstration of the potential of the methodology and demonstrate the importance of verification in the early stages of design.

Identiferoai:union.ndltd.org:IBICT/oai:repositorio.ufsc.br:123456789/168089
Date January 2016
CreatorsPaludo, Rogério
ContributorsUniversidade Federal de Santa Catarina, Lettnin, Djones Vinicius
Source SetsIBICT Brazilian ETDs
LanguagePortuguese
Detected LanguagePortuguese
Typeinfo:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis
Format127 p.| il., grafs., tabs.
Sourcereponame:Repositório Institucional da UFSC, instname:Universidade Federal de Santa Catarina, instacron:UFSC
Rightsinfo:eu-repo/semantics/openAccess

Page generated in 0.003 seconds