quinta-feira, 8 de maio de 2008

Como instalar o model-checking em sistema operacional LINUX, distribuição Debian/GNU Etch

1) Baixe o arquivo no link: http://www.fmi.uni-stuttgart.de/szs/tools/mckit/mckit-bin_linux-040921.tar.gz
2) Como root descompacte o arquivo em: /usr/local
# cd /usr/local
# tar -zxvf
mckit-bin_linux-040921.tar.gz
3) Inclui o diretório bin do kit no PATH:
#export PATH=/usr/local/mckit/bin:${PATH}
4) Para rodar utilize:
# ./check

OBS.: Indo na pasta examples terá um arquivo com o nome test.pl, ao executar esse arquivo, ele fará um teste em todas as ferramentas que compõem o model-checking, mas será observado que não encontrará a ferramenta spin e nem a pep, que necessitam que seja instaladas separadamente.

Como acrescentar a ferramenta SPIN no model-checking

1) Baixe o arquivo do spin no site: http://spinroot.com/spin/Src/spin515.tar.gz
2) Como root descompacte o arquivo em: /usr/local
3) Entre no diretorio, /usr/local/Spin/Src, e altere:
Primeiro a main.c
Onde tem a "include <io.h>" colocar "include </usr/include/sys/io.h>"
Segundo o makefile
Onde tem "CC=cc -DNXT" colocar "CC=cc -DNXT -DPC"
4) Instalar o pacote bison para obter yacc
5) Dar um make na pasta
6) Depois de feito o dito acima edite o arquivo make_pc
7) No arquivo make_pc na linha que tem "mv spin.exe /usr/bin" mude para "mv spin /usr/bin"
8) Pronto, feito tudo basta dar um ./make_pc

Pronto o model-checking já está com o spin, para testar entre em /usr/local/mckit/examples
Depois dê um ./test.pl, verá que ele encontrará as ferramentas spin.

------------------------------------

A explicação sobre como instalar a ferramenta PEP ainda não está pronta, pois ainda estou tendo problemas, caso alguém que leia isto já tenha conseguido instalar, por favor me envie e-mail. Espero ter ajudado.

Nenhum comentário: