Da especificação à verificação de agentes móveis - Um ambiente gráfico

André Gustavo Andrade (1), Ana C.V. de Melo (1), Marcelo M. Amorim (1)

e-mails: oberon@ime.usp.br, acvm@ime.usp.br, mamorim@ime.usp.br

(1) Universidade de São Paulo - IME São Paulo Brasil

Resumen/Resumo

Neste trabalho, apresentamos um ambiente de especificação e verificação para pi-calculus. O ambiente proposto está inicialmente constituído de dois módulos: (i) especificação e representação gráfica; (ii) simulação e verificação de equivalências. O primeiro módulo permite a especificação de processos em pi-calculus com recursos de visualização e representação gráfica da especificação. O seguinte torna possível a simulação e verificação de bisimulações entre processos descritos em pi-calculus utilizando uma nova abordagem através de técnicas de normalização e bisimulações up-to em verificações baseadas em autômatos.

Palabras Clave/Palavras Chave: Verificação Formal, Agente Móvies, Pi-Calculus, Especificação Formal


BibTex 

@INPROCEEDINGS{andrade04:79,
                  AUTHOR       = {André Gustavo Andrade and Ana C.V. de Melo and Marcelo M. Amorim},
                  TITLE        = {Da especificação à verificação de agentes móveis - Um ambiente gráfico},
                  BOOKTITLE    = {30ma Conferencia Latinoamericana de Informática (CLEI2004)},
                  YEAR         = {2004},
                  editor       = {Mauricio Solar and David Fernández-Baca and Ernesto Cuadros-Vargas},
                  pages        = {236--245},
                  address      = {},
                  month        = Sep,
                  organization = {Sociedad Peruana de Computación},
                  note         = {ISBN 9972-9876-2-0},
                  file         = {http://clei2004.spc.org.pe/es/html/pdfs/79.pdf}
}

pdficon.gif PDF de este artículo
PDF de CLEI2004 (incluye todos los artículos)
Página principal CLEI 2004
Generado por Sociedad Peruana de Computación