VerificaÃÃo de modelos para programas em um subconjunto de JCSP

AUTOR(ES)
DATA DE PUBLICAÇÃO

2006

RESUMO

A veriÂcaÂc~ao de modelos formais gerados a partir de programas concorrentes tem sido bem aceita na indÃstria e na academia durante a fase de testes. A busca por qualidade de software tem motivado este uso, principalmente pelo fato de que testar programas concorrentes nÃo à uma tarefa trivial e à suscetÃvel a erros. Os modelos sÃo descritos atravÃs de linguagem de especificaÃÃo formal para sistemas concorrentes como, por exemplo, CSP. Esta linguagem possui padrÃes para a descriÃÃo de interaÃÃo entre sistemas concorrentes. Ela à baseada na troca de mensagens entre os componentes do sistema especificado, os processos. Cada processo à descrito atravÃs de eventos e operadores. Eventos representam as possÃveis aÃÃes do usuÃrio para com o processo ou com o ambiente (O ambiente representa o conjunto de todos os eventos visÃveis aos usuÃrios do sistema, assim como tudo o que possa interagir com os processos envolvidos no sistema { outros processos ou usuÃrios). A biblioteca JCSP à uma biblioteca Java que possui construtores baseados em CSP. Ela prove um bom nÃvel de abstraÃÃo para a escrita de programas concorrentes sem precisarmos utilizar a estrutura de semÃforos que Java oferece. Neste trabalho propomos um mapeamento entre JCSP e CSP com o intuito de estudarmos as propriedades do modelo formal gerado. Utilizamos o famoso exemplo do Jantar dos FilÃsofos para demonstrar a aplicaÃÃo das regras, bem como suas particularidades. Propomos como estudo de caso uma modelagem para uma rede de celulares. Neste estudo apresentamos a derivaÃÃo de processo regra a regra a partir de JCSP. EntÃo analisamos o modelo gerado com o uso de FDR, um verificador de modelos para especificaÃÃes concorrentes, com o objetivo de estudarmos suas propriedades clÃssicas (detecÃÃo de deadlocks, livelocks e nÃo-determinismo) ou especÃficas da aplicaÃÃo. Como principais contribuiÃÃes deste trabalho podemos destacar o mapeamento de comandos Java/JCSP que possuem um maior grau de complexidade durante o mapeamento (while, atribuiÃÃo, composiÃÃo seqÃencial de comandos), visto que CSP nÃo oferece o conceito de passagem de estado entre os comandos, como as linguagens de programaÃÃo o fazem. TambÃm podemos mencionar os construtores JCSP que nÃo sÃo mapeados diretamente para CSP (Alternative)

ASSUNTO(S)

regras jcsp jcsp refinamento refinement abstraction csp rules fdr csp fdr abstraÃÃo ciencia da computacao

Documentos Relacionados