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

• Main Author: Autran Macedo
• Other Authors: Sergio Vale Aguiar Campos
• Format: Others
• Language: Portuguese
• Published: Universidade Federal de Minas Gerais 2002
• Online Access: 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 problemas Job-Shop; (b) resolução de várias instâncias de Job-Shop; (c) novos algoritmos de verificação que estendem 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.