DESENVOLVIMENTO DE SISTEMAS CORRETOS
BISI, Nícolas Nogueira
Universidade Federal de Pelotas
[email protected]
FOSS, Luciana; COSTA, Simone André da
Universidade Federal de Pelotas
[email protected], [email protected]
1 - INTRODUÇÃO
Atualmente boa parte de nossa vida está relacionada de alguma forma
com algum tipo de software, como por exemplo, computadores, celular,
agenda eletrônica, controle de tráfego aéreo, etc. Nesse sentido, por
questões de eficiência e segurança a certificação de que tais softwares sejam
executados da forma desejada, se faz necessária. Este trabalho tem por
objetivo apresentar uma investigação sobre a importância do
desenvolvimento de sistemas corretos, e algumas perspectivas de pesquisa
da linha de métodos formais no projeto intitulado Núcleo de Excelência em
Engenharia de Software para Sistemas Embarcados, coordenado pelo
professor Flávio Wagner Rech (UFRGS) e desenvolvido em cooperação com
pesquisadores da UFRGS, UFPEL e UNIPAMPA.
Trata-se de uma pesquisa em estado inicial, em que propomos
algumas considerações sobre a importância da certificação formal para o
alcance de um software de alto padrão de qualidade. Em geral, para garantir
que um sistema satisfaça certos requisitos, surge a necessidade de utilizar
modelos que permitam uma descrição precisa do mesmo. Em particular,
quando esses sistemas são bastante complexos, devemos optar por modelos
que forneçam construções abstratas que facilitem o entendimento e a
especificação desse sistema de forma modular. A linguagem de
especificação adotada, gramática de grafos, detalhada na seção 2, cumpre
tais requisitos.
A adoção de um método de especificação formal para a descrição de
um sistema permite que propriedades desejadas (requisitos) sejam
verificadas antes mesmo do desenvolvimento completo do sistema. Uma das
técnicas de verificação mais utilizadas hoje em dia é a técnica de model
checking [1]. Ferramentas que utilizam esta técnica recebem como entrada
um modelo finito que representa o sistema a ser analisado e uma
propriedade a ser verificada neste modelo. Uma busca exaustiva no espaço
de estados do sistema verifica se a propriedade é válida para o modelo
descrito. O processo é automático, em muitos casos, eficiente e pode ser
utilizado para verificar especificações parciais. Em alguns casos, quando as
propriedades são violadas, contra-exemplos podem ser produzidos, provendo
informações importantes para análise de erros de uma especificação.
Para verificação formal de propriedades de sistemas especificados em
gramática de grafos [2], utilizou-se o GROOVE [4], um programa que além de
verificação formal, permite realizar simulações nos sistemas especificados.
Esta ferramenta é brevemente apresentada na seção 3. Considerações finais
e trabalhos futuros serão descritos na seção 4.
2 – Gramática de Grafos
Gramáticas são uma forma de representação matemática que permite
especificar linguagens, através de um conjunto de regras capaz de gerar
todas as palavras da linguagem. Gramáticas de grafos são uma
generalização de gramáticas de Chomsky, substituindo strings por grafos.
Pesquisas nessa área começaram a ocorrer a partir da década de 70,
sendo seus resultados utilizados amplamente no campo da informática, como
na teoria de linguagens formais, no reconhecimento e geração de imagens,
na construção de compiladores, na engenharia de software, na teoria de
banco de dados, entre outros [3].
Diferenciando-se das gramáticas de Chomsky, uma regra de uma
gramática de grafos é constituída de dois grafos, um grafo esquerdo e um
grafo direito, e de um (homo)morfismo parcial de grafos, que mapeia os
elementos do lado esquerdo aos do lado direito de forma compatível. Uma
regra especifica elementos que são preservados, criados e/ou deletados. Os
elementos preservados são os elementos que pertencem ao lado direito e
são mapeados para o lado esquerdo. Os elementos criados são os
elementos do lado direito da regra que não são imagem do lado esquerdo.
Os elementos deletados são os elementos do lado esquerdo da regra que
não são mapeados para o lado direito.
A Figura 1 ilustra uma gramática de grafos que modela (parcialmente)
o jogo Come-Come (PacMan) [5]. O grafo Ini ilustra o estado inicial do jogo, e
as regras moveP, moveG, eat e kill modelam o seu comportamento. As
regras moveP e moveG especificam o deslocamento do PacMan e do
Fantasma, respectivamente; quando o PacMan se encontra no mesmo local
que a maçã, a regra eat pode ser aplicada, removendo a maçã para fora do
jogo; já a regra kill descreve a situação quando o PacMan e o fantasma se
encontram no mesmo local, na qual o PacMan morre, restando apenas o
fantasma. A mesma especificação poderia ter sido feita usando strings ao
invés de grafos, mas a gramática resultante certamente seria muito menos
intuitiva.
Figura 1. Especificação do Come-Come usando Gramática de Grafos.
O comportamento (semântica) de um sistema especificado usando
gramática de grafos é descrito via aplicação de regras. Uma regra é aplicada
a um grafo estado (estado atual), determinado uma mudança no estado do
sistema. A Figura 2 mostra a aplicação da regra moveP no grafo Ini. De
acordo com a regra, a seta que aponta para o local 8 é deletada (lado
esquerdo) e a seta que aponta para o local 7 é criada (no lado direito), ou
seja, o PacMan se move do local 8 para o 7, alterando o estado do sistema
para o grafo Out.
Figura 2. Aplicação da regra moveP no grafo Ini.
3 – Especificação e Verificação no GROOVE
Para realizarmos simulações, utilizamos a ferramenta GROOVE,
desenvolvida pela universidade de Twente, Países Baixos, onde de uma
maneira simples, é inserido um modelo especificado em gramática de grafos.
A Figura 3 apresenta a interface da ferramenta com o exemplo do
PacMan. No centro está especificado um possível estado inicial do sistema e
na esquerda podemos acessar as regras que compõem a gramática.
Figura 3. Interface do GROOVE.
Na Figura 4 é detalhada a regra kill, em que o PacMan (PacM) é
deletado caso se encontre no mesmo local (b) que o fantasma (Ghost).
Figura 4. Regra kill especificada no GROOVE.
Esta ferramenta nos permite também fazer a verificação automática
(model-checking) de propriedades de um sistema. A especificação destas
propriedades é feita usando lógica temporal, que nos permite descrever
comportamentos do sistema no decorrer de sua evolução. Para realizarmos a
verificação de uma propriedade, deve-se gerar o espaço de estados do
sistema e o verificador varre este espaço de estados verificando se a
propriedade é válida. Para o exemplo do PacMan, podemos garantir, por
exemplo, que até morrer o PacMan poderá sempre se mover (propriedade
desejada no jogo).
4 - CONCLUSÕES
A aplicabilidade das certificações formais permite o desenvolvimento
de sistemas corretos e confiáveis. A adoção de tais métodos em sistemas
críticos se torna ainda mais importante, permitindo prevenir erros e
problemas graves. Por exemplo, acidentes em sistemas ferroviários e aéreos
podem ser evitados, falhas em sistemas bancários, como cobranças
indevidas, podem ser identificadas, entre outros.
A proposta futura do projeto é a aplicação da certificação formal em
sistemas embarcados, visando o projeto destes sistemas em um tempo
reduzido, garantindo qualidade e eficiência. Em particular, quer se investigar
modelos que possuam abstrações capazes de descrever adequadamente os
diversos requisitos de sistemas embarcados, nas diferentes fases do seu
desenvolvimento, bem como definir transformações entre esses modelos. Os
modelos e as transformações serão especificados formalmente para permitir
diversos tipos de análise e prover garantias tanto nos modelos quanto nas
respectivas transformações.
5 - REFERÊNCIAS
[1]
DWYER, M.; HATCLIFF, J.; ROBBY; PASAREANU, C. E VISSER, W. Formal
Software Analysis Emerging Trends in Software Model Checking. In: Formal
Software Analysis Emerging Trends in Software Model Checking, p.1-17, 2007.
[2]
EHRIG, H. Introduction to the algebraic theory of graph grammars (a survey). In:
Graph-Grammars and Their Application to Computer Science and Biology, Bad
Honnef, October 30 - November 3, 1978. Lecture Notes in Computer Science, vol 73.
Springer Berlin/Heidelberg, 1979. Pg. 1-69.
[3]
EHRIG, H.; ENGELS, G.; KREOWSKI, H.-J.; ROZENBERG, G. Handbook of graph
grammars and computing by graph transformation: vol. 2: applications,
languages, and tools. World Scientific: 1998.
[4]
GROOVE, GRaphs for Object-Oriented Verification. Novembro de 2010. Disponível
em http://groove.sourceforge.net/groove-index.html.
[5]
RIBEIRO, L. Métodos Formais de Especificação: Gramáticas de Grafos. In: SBC Sul.
(Org.). VIII Escola de Informática da SBC-Sul. Porto Alegre: Editora da UFRGS,
2000, p. 1-33.