Pós-Graduação em Ciência da Computação – UFPE
Defesa de Dissertação de Mestrado Nº 2.143
Aluna: Vitória Maria Pena Mendes
Orientador: Prof. Gustavo Henrique Porto de Carvalho
Título: An Updated Theory for Communicating Sequential Processes in Coq
Data: 30/04/2024
Hora/Local: 8h – Auditório do CIn
Banca Examinadora:
Prof. Juliano Manabu Iyoda (UFPE / Centro de Informática)
Prof. Sidney de Carvalho Nogueira (UFRPE / Departamento de Computação)
Prof. Gustavo Henrique Porto de Carvalho (UFPE / Centro de Informática)
RESUMO:
A habilidade de um sistema realizar operações simultâneas é conhecida como
concorrência. Em sistemas concorrentes, o grande número de maneiras nas
quais os componentes podem interagir entre si eleva significativamente a
complexidade de analisar o comportamento desses sistemas. CSP
(\emph{Communicating Sequential Processes}) introduz uma notação
conveniente para descrever precisamente sistemas concorrentes. Ao longo dos
anos, ferramentas computacionais foram desenvolvidas para permitir a
análise de especificações em CSP, tais como: a ferramenta
\emph{Failures-Divergence Refinement} (FDR) e teorias em Isabelle (por
exemplo, CSP-Prover, HOL-CSP). Anteriormente, uma caracterização inicial de
CSP foi desenvolvida em Coq: CSP${\text{Coq}}$. Aqui, estendeu-se
significativamente as possibilidades de usar CSP para raciocinar sobre
concorrência em Coq. Agora, há suporte para comunicações compostas,
processos parametrizados e operadores de CSP que não foram considerados
previamente. Condições de boa formação são também formalizadas em Coq e
táticas de automação de prova são fornecidas. Além disso, foi desenvolvida
uma extensão para o VSCode que converte automaticamente especificações em
CSP${\text{M}}$ (o dialeto em ASCII de CSP) para CSP$_{\text{Coq}}$.
Palavras-chave: Communicating Sequential Processes, CSP, Coq, Assistente de
provas, Extensão para o VSCode
Comentários desativados