Solução exata de problemas de escalonamento determinísticos por meio de verificação simbólica de modelos
Carregando...
Arquivos
Data
Autor(es)
Título da Revista
ISSN da Revista
Título de Volume
Editor
Universidade Federal de Minas Gerais
Descrição
Tipo
Tese de doutorado
Título alternativo
Primeiro orientador
Membros da banca
Carlos Roberto V de Carvalho
Henrique Pacca Loureiro Luna
Henrique Pacca Loureiro Luna
Resumo
Problemas de Escalonamento (scheduling) ocorrem em ambientes de escassez de recursos. O problema consiste em determinar um compartilhamento dos recursos entre as tarefas que necessitam usá-los. Esse compartilhamento, ou escalonamento, consiste de uma seqüência de execução das máquinas ao longo do tempo, que deve estar em conformidade com um critério de otimização. Por sua vez, verificação simbólica de Modelos (VSM) é uma técnica de verificação formal proposta originalmente para sistemas concorrentes, que podem ser modelados por um conjunto finito de estados. VSM é composto de um modelo de representação, uma lógica temporal e algoritmos de verificação. Uma vez modelado um sistema em VSM podemos verificar se o modelo atende certas propriedades. Essa verificação ocorre de modo automático.Tradicionalmente, solução exata para Problemas de Escalonamento é obtida por meio de uma técnica conhecida como Branch-and-Bound. A tese apresenta uma abordagem de solução exata por meio de VSM enfocando: (a) um arcabouço para problemas de escalonamento, mais especificamente problemasJob-Shop; (b) resolução de várias instâncias de Job-Shop; (c) novos algoritmos de verificação queestendem a versatilidade de VSM; (d) a aplicação de VSM ao problema de integração entre o planejamento dos níveis tático e operacional.
Abstract
Assunto
Programas de computador Verificação
Palavras-chave
Verificação de modelos, Verificação formal