FORÇAMENTO DE OPACIDADE DE ESTADO ATUAL POR MEIO DE TROCAS DAS OBSERVAÇÕES DE EVENTOS

Abstract

Opacidade é uma propriedade que garante que qualquer comportamento secreto do sistema permaneça Escondido de um Intruso. Neste trabalho será considerado o problema da opacidade de estado atual e será proposto um Forçado de Opacidade capaz de permutar adequadamente a ordem de observação dos eventos Ocorridos no sistema de forma que o Intruso seja enganado e sempre estime, erroneamente, pelo menos um estado não secreto. Condições necessárias e suficientes para verificar se a síntese do Forçado de Opacidade é factível e dois algoritmos para construção do autômato que implementa a estratégia usada pelo Forçado de Opacidade são propostos. Os resultados do artigo são ilustrados utilizando-se um exemplo retirado da literatura.