área de pesquisa ANÁLISE DO COMPORTAMENTO DE CANAIS IÔNICOS UTILIZANDO MODEL CHECKING SIMBÓLICO Mirlaine Aparecida Crepalde