A Verificação de Modelos

Verificação de Modelos

Abstract. This paper aims to explain and demonstrate the practical use of TLA tool in model checking process.

Key-words: tla, pluscal, specification.

Resumo. Este trabalho tem como objetivo explicar e demonstrar de forma prática o uso da ferramenta TLA no processo de verificação de modelos.

Palavras-chave: tla, pluscal e especificação.

1. Introdução

Na disciplina de métodos formais para computação foi desenvolvido um trabalho sobre a verificação de modelos formais com suas aplicações. Para demonstrar a verificação formal, será utilizada a ferramenta a TLA. Assim, será feito um tutorial sobre como utilizar a ferramenta e sua linguagem de programação chamada PlusCal. O exemplo utilizado será o Algoritmo de Euclides.

1. Definição do conceito de verificação de modelos e principais áreas de aplicação

A verificação de modelos é uma das técnicas de verificação formal que tem como objetivo a confiabilidade em sistemas que não podem ter falhas. Esta verificação testa sistemas concorrentes e distribuídos com estados finitos.

Existem três etapas para aplicar esta verificação em um projeto:

1.Modelagem: para esta etapa construir um modelo formal do sistema e ter todos os comportamentos possíveis do sistema.

2.Especificação: para esta etapa é necessário verificar todos os comportamentos desejáveis do sistema. Como para um sistema de hardware e de software pode-se usar a lógica temporal ou máquinas de estados.

3.Verificação: para esta etapa coloca-se em uma ferramenta o modelo e as especificações. Esta ferramenta gera um valor negativo ou positivo e quando negativo gera um contra exemplo para que o especialista identificar onde está o erro.

As aplicações, hoje em dia, são cada vez mais críticas e não podem ocorrer falhas, então utilizar a verificação de modelos para ajudar a encontrar falhas que causaram grandes problemas. Exemplos de sistemas ou empresas que utilizam esta técnica: Amazon, Google, missões da nasa, sistema de comércio eletrônico e entre outros.

1. Apresentação da ferramenta TLA+

TLA+ é uma linguagem de especificação para sistemas concorrentes e distribuídos que combina a lógica temporal com a lógica de primeira ordem completa e teoria dos conjuntos de Zermelo-Fraenkel.

Algumas características de TLA+ são:

1. TLA+ tem uma estrutura modular que permite um processo de escrita por incrementos sucessivos, de acordo com o grau de abstração ou de detalhe desejado;
2. Uma especificação em TLA+ é parecida com código de programas, e portanto, pode oferecer uma base sólida para a implementação de softwares;
3. O verificador de modelo TLC permite verificar automaticamente a especificação, assim como as propriedades temporais associadas;
4. Dotado do verificador de modelo TLC, TLA+ permite a especificação e a verificação tanto de protocolos de “hardware” quanto de sistemas distribuídos.

Numa especificação em TLA+, uma computação de um sistema é representada por uma sequência de estados, também chamada de comportamento. Para caracterizar os estados do sistema, uma especificação define o conjunto de variáveis (VARIABLES) utilizado para descrever o sistema e o conjunto de constantes (CONSTANTS), que são utilizadas para definir os valores eventualmente atribuídos às variáveis. Um estado do sistema é definido pela atribuição de valores constantes as variáveis da especificação.

Um par de estados consecutivos, suponha i e f em referência a inicial e final, é chamada de passo e é denotado i → f . O operador linha ‘’ ′ ” é utilizado para distinguir os valores de variáveis num passo. Considerando um certo passo P : i → f, e uma variável v, a ocorrência de v sem linha (v) faz referência ao valor de v em i, enquanto a ocorrência de v com linha (v’) faz referência ao valor de v em  f .

Uma função de estado é uma expressão na qual aparecem somente variáveis sem linhas. Tal função associa valores constantes aos estados de um comportamento. As funções de estado a valores booleanas são chamadas de predicados de estado.

Uma função de transição é uma expressão na qual aparecem variáveis sem linhas e com linhas. Portanto, denotando P o conjunto dos passos de um sistema, uma função de transição F é um mapeamento de P sobre F(P). Por exemplo, seja um passo P : i → f e v uma variável, tal como v = 0 no estado i e v = 1 no estado f , e seja F a função de transição definida por F(P) = v′ − v, tem-se F(P) = 1.

Finalmente, uma ação é, por definição, uma função de transição a valores booleanos. Portanto, uma ação é um mapeamento de P sobre {V , F}, onde V e F correspondem aos valores de verdade e falso da lógica de predicados. Considerando o exemplo apresentado acima, a ação A, definida pela expressão A ≜ v ′ = v +1, na qual o símbolo TLA+ significa “igual, por definição”, é verdadeira no passo P. Para um dado passo P, a relação de sucessão do estado i para o estado f, usualmente chamada de função de transição de estado no formalismo das Máquinas de Estado Finitos, é definida pelo conjunto de ações definidas sobre o passo P. Este conjunto também é uma ação, pois uma ação pode ser composta de várias ações.

As fórmulas temporais de TLA+, como por exemplo, a relação de transição entre estados, são asserções booleanas sobre comportamentos. Diz-se que um comportamento satisfaz uma fórmula F se F é uma asserção verdadeira deste comportamento. O operador da lógica temporal □ é utilizado para escrever as fórmulas temporais. A semântica do operador □ é definida da seguinte maneira. Para algum comportamento Σ, e alguma ação A, a fórmula temporal F = □ [A]vars  é verdadeira – ou simplesmente “ Σ satisfaz F ” – se e somente se, para qualquer passo P : i → f de Σ que altera o conjunto vars de todas as variáveis, A é verdadeira em P.

 

3.1 A fórmula principal Spec

• Spec − A fórmula Spec, apresentada na figura 1, é a fórmula principal de uma especificação em TLA+.

[pic 1]

Figura 1. A fórmula spec

Init é o conjunto dos estados iniciais, □ [Next]vars é a relação de sucessão, e Liveness é uma condição de evolução do sistema. Next é o conjunto de ações que podem ser verdadeiras num certo passo de um comportamento. Consequentemente, um comportamento Σ satisfaz Spec se e somente se o primeiro estado de Σ é um elemento de Init e todos os passos de Σ satisfazem Next e a condição Liveness.