Solução exata de problemas de escalonamento determinísticos por meio de verificação simbólica de modelos

• Ano de defesa: 2002
• Autor(a) principal: Autran Macedo
• Tipo de documento: Tese
• Tipo de acesso: Acesso aberto
• Idioma: por
• Instituição de defesa: Universidade Federal de Minas Gerais; UFMG
• Palavras-chave em Português: Verificação de modelos; Verificação formal; Programas de computador Verificação
• Link de acesso: http://hdl.handle.net/1843/SLBS-5KKM5J

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.