Model checking CSPZ: Techniques to overcome state explosion
AUTOR(ES)
Alexandre Cabral Mota
DATA DE PUBLICAÇÃO
2001
RESUMO
Hoje em dia, notamos um crescente interesse na tÃcnica de verificaÃÃo de modelos por acadÃmicos e por profissionais da indÃstria. A razÃo disso talvez esteja na habilidade dos verificadores de modelos|implementaÃÃes de algoritmos de verificaÃÃo de modelos|serem totalmente automÃticos: nÃo hà intervenÃÃo do usuÃrio durante a anÃlise. Com certeza, trata-se de uma vantagem ausente em provadores de teoremas, por razÃes teÃricas. Obviamente, porÃm, uma limitaÃÃo importante da verificaÃÃo de modelos|o problema da explos~ao exponencial de estados - à sà poder ser aplicada a sistemas finitos. Assim, verificaÃÃo de modelos e prova de teoremas podem ser considerados tÃcnicas ortogonais e complementares. Uma outra tendÃncia à o reÃso formal de recursos disponÃveis. Normalmente, consegue-se reÃso pela integraÃÃo formal de teorias e ferramentas bem difundidas. A razÃo à quase Ãbvia: obtÃm-se uma teoria e/ou ferramenta mais expressiva com menor esforÃo, quando comparado a desenvolver tal teoria e/ou ferramenta do nada. O ponto-chave nesta Ãrea de pesquisa à produtividade; conceito bem conhecido para profissionais da indÃstria. Por exemplo, integrar verificadores de modelos e provadores de teoremas està sendo visto como um esforÃo crucial para a anÃlise de sistemas. Nesta tese, nosso objetivo maior à mostrar como aplicar verificaÃÃo de modelos para CSPZ . CSPZ à uma linguagem formal que integra duas linguagens difundidas: a Ãlgebra processos CSP e o formalismo baseado em modelos Z. PorÃm, em vez de criar uma tÃcnica de verificaÃÃo de modelos para CSPZ do nada, nÃs seguimos a mesma abordagem usada em CSPZ : uma estratÃgia de verificaÃÃo de modelos para CSPZ onde reÃsa-se a tÃcnica de verificaÃÃo de modelos para CSP jà existente. Basta mostrar como um processo CSPZ pode ser visto como um em CSP. Tendo a habilidade natural de lidar com tipos de dados infinitos, à normal CSPZ criar sistemas infinitos. Isso evita a aplicaÃÃo direta de verificaÃÃo de modelos. Pesquisando soluÃÃes para esse problema, obtivemos duas contribuiÃÃes distintas mas complementares. Caracterizamos como os processos infinitos de CSPZ podem ser tratados aplicando duas abordagens diferentes. Uma à baseada no trabalho de Lazic que lida com a parte em CSP, fundamenta-se no conceito de independÃncia de dados. A outra à baseada em interpretaÃÃo abstrata e lida com a parte em Z. AlÃm disso, nÃs encontramos uma maneira de mecanizar a abordagem baseada em interpretaÃÃo abstrata, visto que os trabalhos na literatura requerem que o usuÃrio proponha a abstraÃÃo de dados. Apesar da abordagem acima ser eficaz, o sistema abstraÃdo ainda pode ser muito complexo (apesar definito) para ser analisado por verificaÃÃo de modelos. EntÃo, fizemos um esforÃo adicional para adaptar uma abordagem manual para anÃlise modular de deadlock|originalmente concebida para CSP. Mecanizamos parte dessa anÃlise e a adaptaÃÃo foi provada formalmente. Finalmente, consideramos um sistema real como estudo de caso. NÃs mostramos como este sistema pode ser analisado aplicando as abordagens investigadas e refinamento de dados para Z atravÃs de uma metodologia geral proposta. Enquanto as abordagens de refinamento de dados e abstraÃÃo de dados mostraram-se promissoras no sentido de obter um sistema finito, a abordagem modular revelou um ganho impressionante comparado a uma anÃlise global do mesmo sistema
ASSUNTO(S)
especificaÃÃo formal ciencia da computacao anÃlise prova de teoremas verificaÃÃo de modelos
