Translating extended goal models into goal management controllers in PRISM

Abstract

Os sistemas autoadaptativos (SAS) frequentemente combinam a avaliação de objetivos e a seleção de estratégias em uma única camada arquitetural, o que limita sua capacidade de adaptação em tempo de execução. A arquitetura MORPH resolve essa questão estruturando a adaptação em três camadas de controle: Gerenciamento de Objetivos, Gerenciamento de Estratégias e Implementação de Estratégias. Nesse contexto, a estrutura EDGE (ExtenDed Goal modEling) aprimora a camada de Gerenciamento de Objetivos ao introduzir uma nova notação de modelagem, orientada por cinco desideratos que oferecem suporte ao raciocínio dinâmico de objetivos, síntese de planos e memória de decisões. O EDGE também permite a geração de modelos de Processo de Decisão de Markov (MDP) na linguagem PRISM, representando controladores de objetivos capazes de monitorar conquistas e calcular planos de adaptação em condições de incerteza. No entanto, alinhar modelos de objetivos de alto nível com controladores de gerenciamento de objetivos formalmente verificáveis continua sendo um desafio central. À medida que os sistemas evoluem, a falta de transformações automatizadas que preservem a semântica muitas vezes leva à divergência entre os requisitos e a lógica executável, prejudicando as garantias e a manutenção do sistema. Para resolver essa lacuna, propomos uma ferramenta que sintetiza automaticamente controladores de objetivos EDGE rastreáveis e verificáveis em PRISM a partir de modelos EDGE anotados. Alinhada com os desideratos do EDGE, a ferramenta suporta a tradução automatizada, modular e escalável de modelos i* estendidos para código PRISM, reduzindo o esforço manual e reforçando a conexão entre a intenção a nível de objetivos e a adaptação em tempo de execução.