Modelagem e verificação de escalonabilidade de sistemas de tempo real

DSpace Repository

A- A A+

Modelagem e verificação de escalonabilidade de sistemas de tempo real

Show full item record

Title: Modelagem e verificação de escalonabilidade de sistemas de tempo real
Author: Naspolini, Adriano Correa
Abstract: Apresenta-se uma metodologia para modelagem e análise de sistemas de tempo real com escalonamento utilizando técnicas de verificação de propriedades no contexto do projeto Topcased. Entre as linguagens para descrição de sistemas adotadas em tal projeto, adota-se V-Cotre. A Rede de Petri Temporal com Stopwatch (RPT-Sw) é utilizada como formalismo para exprimir as aplicações de tempo real e os mecanismos de escalonamento. As ferramentas de análise e verificação de Tina para este formalismo servem de base para abordagem proposta. Para validar as proposições apresentadas, três escalonadores clássicos são modelados: Rate Monotonic, Immediate Priority Ceiling Protocol e Earliest Deadline First; mas apenas os dois primeiros são verificados. Constatam-se limitações da linguagem V-Cotre para representação de algumas características destes sistemas e sugere-se um enriquecimento da linguagem como solução para esta limitação. Como a tradução da linguagem V-Cotre para o formalismo de base da verificação ainda não está completamente terminada, modelos simples em RPT-Sw são construídos manualmente para verificação dos dois primeiros tipos de escalonamento citados. Sugere-se um novo formalismo baseado em RPT-Sw de forma a permitir a representação completa destes sistemas. Os resultados de verificações sobre estes modelos com a ferramenta Tina demonstram que a abordagem baseada na verificação produz resultados equivalentes aos dos testes de escalonamento clássicos, sendo que estes podem ser eventualmente complexos em sistemas com muitas tarefas e recursos aninhados. Além disso, os testes efetuados permitem visualizar diversas análises em um nível de abstração "com escalonamento", de forma a aperfeiçoar a utilização de material, permitindo melhores escolhas de tempos relativos aos sistemas de tempo real.
Description: Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico. Programa de Pós-Graduação em Engenharia Elétrica
URI: http://repositorio.ufsc.br/xmlui/handle/123456789/89000
Date: 2006


Files in this item

Files Size Format View
PEEL1043.pdf 1.853Mb PDF View/Open

This item appears in the following Collection(s)

Show full item record

Search DSpace


Browse

My Account

Statistics

Compartilhar