Proposta de um método de verificação por tempo global com redes de Petri no desenvolvimento de software embarcado e em tempo real

Abstract

Resumo: Sistemas embarcados de tempo real são sistemas restritos quanto às funcionalidades e recursos disponíveis. Nesses sistemas, requisitos temporais são tão importantes quanto requisitos funcionais. Nas fases de análise e projeto do software embarcado, um modelo analítico pode auxiliar em atividades de verificação, reduzindo o tempo de desenvolvimento e aumentando a garantia do comportamento correto do sistema. Este trabalho propõe a aplicação da técnica de tempo global de redes de Petri na verificação de software embarcado de tempo real. Um algoritmo da técnica de tempo global foi proposto e implementado. Um método geral de aplicação desta técnica e uma instanciação deste método foram propostos. Modelos de mapeamento de tarefas em redes de Petri foram desenvolvidos e um modelo de geração de cenários de comportamento para a análise de escalonabilidade para as políticas de prioridade fixa e earliest deadline first foi determinado e implementado. A execução e análise de experimentos permitiram observar o método e modelos. O método proposto neste trabalho objetiva identificar cenários de comportamento que não respeitam as restrições temporais do sistema modelado. No caso de sistemas embarcados e em tempo real esta é uma das principais preocupações das equipes de desenvolvimento de software. Como resultado, desenvolvemos um método que permite a verificação temporal de software embarcado de tempo real com relógios global e relativo, que é um passo relevante para facilitar a aplicação de redes de Petri no contexto do desenvolvimento destes sistemas.

Abstract: Real time embedded systems are function and time constrained. In these systems, time constraints are as important as functional. An analytical model can help in the verification activities during embedded software analysis and design, reducing development time and increasing assurance of proper system behavior. This work proposes the application of global time technique of Petri nets as an alternative to the verification of real time embedded software. An algorithm of global time technique was proposed and implemented. We proposed a general method of application of this technique and an instantiation of this method. We developed models for the mapping of tasks in Petri nets and we determined and implemented a model for the generation of scenarios for the schedulability analysis considering fixed priority and earliest deadline first policies. The implementation and analysis of experiments allowed us to observe the method and models. The method proposed in this thesis aims to identify behavioral scenarios which do not meeting the time constraints of the modeled system. This is a major concern for software development teams about embedded and real time systems. As a result, we developed a method allowing time verification of real-time mbedded software using global and relative clocks, which is an important step to facilitate the application of Petri nets in the development of these systems.