VerificaÃÃo de modelos para programas em um subconjunto de JCSP
AUTOR(ES)
Carla Maria Pinheiro do Nascimento
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
- Modelos de verificaÃÃo à flexÃo de estruturas protendidas
- ComposiÃÃo de biometrias para sistemas multimodais de verificaÃÃo de identidade pessol
- Virtual.Prob - Ambiente virtual para auxÃlio e verificaÃÃo do aprendizado
- IVM: uma metodologia de verificaÃÃo funcional interoperÃvel, iterativa e incremental
- Contratos formais para derivaÃÃo e verificaÃÃo de componentes paralelos.