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

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.