Verificação Formal: Aula 1

Verificação de algoritmos não sequenciais

Considere o seguinte algoritmo de exclusão mútua proposto por Peterson.

   var 
     turn : 0..1;
     want0 : boolean = false;
     want1 : boolean = false;

   procedure process0;
   begin
     while true do                           
     begin
       (* idle *) 
       want0 := true; 
       turn := 1;  
       repeat until (not want1 or turn = 0);
       (* critical *) 
       want0 := false 
     end
   end;

   procedure process1;
   begin
     while true do                           
     begin
       (* idle *) 
       want1 := true; 
       turn := 0;  
       repeat until (not want0 or turn = 1);
       (* critical *) 
       want1 := false
     end 
   end;

   process0 || process1

Algumas das propriedades desejadas para este algoritmo são:

• Os dois processos nunca estão na região critica ao mesmo tempo.
• Sempre que um processo pretende aceder à região crítica irá conseguir.
• Ausência de deadlock.

Infelizmente, não conseguimos (pelo menos diretamente) usar lógica de Hoare para especificar e verificar estas propriedades, pois o algoritmo não termina e não pode ser especificado com uma relação entre inputs e outputs. Nesta UC vamos usar várias técnicas para especificar e verificar este tipo de algoritmos. Mas para começar vamos especificar e verificar propriedades de um sistema muito simples, mas com características semelhantes (não terminação), nomeadamente um simples relógio.

Modelação com sistemas de transição de estados

Um dos modelos mais comuns da computação são os sistemas de transição de estados. Um sistema de transição de estados inclui:

• Um conjunto de estados $S$.
• Um conjunto de estados iniciais $I \subseteq S$.
• Uma relação de transição entre estados $R \subseteq S \times S$.

Um comportamento (ou traço) do sistema é uma sequência de estados $\pi = s_0,s_1,s_2,\ldots$ tal que $s_0 \in I$ e $\forall i \in \mathbb{N} \cdot (s_i,s_{i+1}) \in R$. Para simplificar a semântica da lógica temporal que vamos usar para especificar as propriedades destes sistemas, é frequente assumir-se que todos os comportamentos possíveis são infinitos. Para tal exige-se que a relação $R$ seja total, ou seja, $\forall s \in S \cdot \exists s’ \in S \cdot R(s,s’)$.

Um relógio só com horas pode ser modelado pelo seguinte sistema de transição de estados.

Exercício: Quantos comportamentos possíveis tem este sistema?

Um relógio defeituoso que por vezes confunde o meio dia com a meia noite pode ser modelado pelo seguinte sistema de transição de estados.

Exercício: Quantos comportamentos possíveis tem este sistema?

Lógica Temporal Linear

Para especificar propriedades de algoritmos reativos, concorrentes ou distribuídos, é frequente usar-se lógica temporal linear (Linear Temporal Logic). A ideia de especificar propriedades de algoritmos desta natureza usando lógica temporal deve-se a Amir Pnueli, ideia pela qual recebeu um prémio Turing em 1996. As asserções em lógica temporal linear são verificadas em comportamentos, ou seja, sequências de estados possíveis. Um sistema de transição satisfaz uma asserção em lógica temporal sse esta for válida em todos os seus possíveis comportamentos. Para além das conectivas usuais da lógica proposicional, na versão mais simples da lógica temporal temos as conectiva temporais $\square$ (always) e $\bigcirc$ (next ou after), que, quando aplicada a uma proposição, verificam se esta é válida em todos os estados de um comportamento ou no estado seguinte, respetivamente. A gramática desta lógica é então definida como

\[\begin{array}{lcl} \mathit{formula} & \doteq & \mathit{predicate}\\ & \mid & \neg \mathit{formula}\\ & \mid & \mathit{formula} \wedge \mathit{formula}\\ & \mid & \bigcirc\ \mathit{formula}\\ & \mid & \square\ \mathit{formula} \end{array}\]

onde $\mathit{predicate}$ é um predicado arbitrário envolvendo as variáveis que definem os estados.

A semântica da lógica temporal linear é definida sobre sistemas de transição de estados. Uma fórmula é válida num sistema de transição sse for válida em todos os seus comportamentos. O facto de uma fórmula $F$ ser válida num comportamento $s_0,s_1,\ldots$ é denotado por $s_0, s_1, \ldots \models F$. Esta noção de validade pode ser definida recursivamente na estrutura das fórmulas da seguinte forma ($F$ e $G$ representam fórmulas arbitrárias e $P$ um predicado arbitrário).

\[\begin{array}{lcl} s_0,s_1,\ldots \models P & \equiv & s_0 \models P\\ s_0,s_1,\ldots \models \neg F & \equiv & s_0,s_1,\ldots \not\models F \\ s_0,s_1,\ldots \models F \wedge G & \equiv & s_0,s_1,\ldots \models F \wedge s_0,s_1,\ldots \models G\\ s_0,s_1,\ldots \models \bigcirc F & \equiv & s_1,s_2,\ldots \models F\\ s_0,s_1,\ldots \models \square F & \equiv & \forall i \ge 0 \cdot s_i,s_{i+1},\ldots \models F \end{array}\]

Usando estas conectivas podemos definir alguns operadores derivados, por exemplo, $F \vee G \doteq \neg (\neg F \wedge \neg G)$ ou $F \Rightarrow G \doteq \neg F \vee G$. Temos também o operador derivado $\lozenge$ (eventually), que se define como $\lozenge F \doteq \neg \square \neg F$. Também podemos definir diretamente a semântica deste operador da seguinte forma.

\[\begin{array}{lcl} s_0,s_1,\ldots \models \lozenge F & \equiv & \exists i \ge 0 \cdot s_i,s_{i+1},\ldots \models F \end{array}\]

Alguns exemplos de fórmulas LTL e a respetiva semântica informal (onde $P$ e $Q$ representam predicados de estado arbitrários):

• $P$, o predicado $P$ é verdade em todos os estados iniciais.
• $\square P$, o predicado $P$ é verdade em todos os estados de todos os comportamentos.
• $\lozenge P$, o predicado $P$ será inevitavelmente verdade nalgum estado de todos os comportamentos.
• $\square (P \Rightarrow \lozenge Q)$, sempre que $P$ é verdade $Q$ terá que inevitavelmente ser verdade depois.
• $\lozenge \square P$, em todos os comportamentos vai-se atingir um estado onde a partir do qual $P$ é sempre verdade.
• $\square \lozenge P$, o predicado $P$ é recorrentemente verdade em todos os comportamentos.

No sistema de transição do nosso relógio só com horas, as seguintes propriedades são válidas:

• $\square (h \neq 24)$, o relógio nunca marca as 24 horas.
• $\lozenge (h = 12)$, o relógio vai inevitavelmente marcar as 12 horas.
• $\square \lozenge (h = 0)$, o relógio vai recorrentemente marcar as 0 horas.

Exercício: Estas propriedades são todas válidas no relógio defeituoso?

Safety vs Liveness

As propriedades do relógio especificadas acima são de uma natureza bastante diferente:

• A primeira é uma propriedade de safety que proíbe certos estados “maus” de acontecerem (aqueles onde o relógio marca as 24 horas). Um contra-exemplo para esta propriedade teria um prefixo que termina num estado “mau”, não importando o que acontece depois (qualquer comportamento com o mesmo prefixo será um contra-exemplo).
• A segunda e a terceira são propriedades de liveness que forçam certos estados “bons” a acontecerem (no caso da segunda propriedade, queremos assegurar que o relógio vai marcar as 12 horas). Um contra-exemplo para estas propriedades tem que ser um comportamento completo (infinito) onde o estado “bom” nunca chega a acontecer.

Model checking explícito

O model checking é uma técnica para verificar automaticamente se uma fórmula em lógica temporal é válida num sistema de transição de estados que modela o comportamento de um sistema. Para que tal seja possível, o sistema de transição de estados tem que ser finito. Um model checker tenta encontrar um contra-exemplo para a fórmula, e se não o encontrar então a fórmula é válida.

No caso das propriedades de safety basta encontrar um prefixo que leva a um estado “mau”, logo a técnica de model checking é muito simples: basta fazer uma travessia no sistema de transição e verificar se esse estado “mau” é alcançável a partir de um estado inicial. Se quisermos garantir que é mostrado o contra-exemplo mais curto possível basta usar uma travessia breadth first. A verificação de uma propriedade de safety pode então ser feita em tempo linear no tamanho do sistema de transição.

Para encontrar um contra-exemplo para uma propriedade de liveness temos que encontrar um comportamento completo (infinito) onde o estado “bom” nunca acontece. Obviamente, se quisermos mostrar esse contra-exemplo ao utilizador, ele terá que ser representado de forma finita: um prefixo finito de estados seguido de um segmento finito que se repete para sempre (um traço com um ciclo). Note que nem todos os comportamentos de um sistema de transição podem ser representados de forma finita, mas um dos resultados mais importantes da lógica temporal é que se uma fórmula não é válida então terá que ter pelo menos um contra-exemplo que pode ser representado de forma finita, pelo que o model checking pode restringir a sua procura a este tipo de comportamentos. Na prática, para encontrar contra-exemplos para uma propriedade de liveness temos que encontrar ciclos no sistema de transição onde o estado “bom” nunca acontece.

Considere, por exemplo, a propriedade de liveness $\lozenge P$. Uma forma eficiente de encontrar contra-exemplos para esta propriedade (comportamentos com um ciclo onde todos os estados satisfazem $\neg P$) consiste em usar a seguinte técnica:

• Restringir o sistema de transição apenas aos estados que satisfazem $\neg P$.
• Calcular os componentes fortemente ligados deste sistema de transição restrito.
• Usar uma única travessia para ver se algum dos componentes fortemente ligados não triviais (componentes com mais de um estado ou com apenas um estado com um lacete) é acessível a partir de um estado inicial.
• Se tal for possível então temos um contra-exemplo, pois dentro de um componente fortemente ligado não trivial conseguimos ter um ciclo infinito.

Esta técnica pode ser generalizada para verificar qualquer fórmula em lógica temporal linear e pode ser executada em tempo linear devido ao algoritmo de calculo de componentes fortemente ligados inventado por Robert Tarjan, pelo qual recebeu um prémio Turing em 1986 (entre outros algoritmos). A ideia de usar este algoritmo para fazer model checking eficiente de fórmulas em lógica temporal deve-se a Edmund Clarke, Ernerst Emerson e Joseph Sifakis, pela qual também receberam um prémio Turing em 2007.

Esta técnica de model checking designa-se de explícita, porque constrói explicitamente o sistema de transição em memória (o espaço de memória que consome é linear). Como o número de estados cresce exponencialmente com o número de variáveis usadas para descrever o estado, esta técnica não pode ser aplicada quando temos muitas variáveis. Existe uma técnica alternativa, designada de model checking simbólico, onde o sistema de transição não é construído explicitamente, mas representado implicitamente através de fórmulas, e que tem normalmente melhor eficiência nesses casos. O Alloy é um exemplo de uma linguagem onde a análise é feita usando model checking simbólico.

Exercício: No sistema de transição do relógio defeituoso dê exemplos de comportamentos que podem ser representados de forma finita e comportamentos que não podem ser representados de forma finita.

Exercício: No sistema de transição do relógio defeituoso indique um possível contra-exemplo que seria retornado por um model-checker para a propriedade $\lozenge (h = 12)$.

Temporal Logic of Actions

O problema com a lógica temporal linear é que apenas pode ser usada para especificar as propriedades desejadas para o sistema modelado. Na maioria dos model checkers o sistema de transição é descrito recorrendo a uma linguagem de domínio específico. Ou seja, a modelação e a especificação são feitas com linguagens diferentes. Leslie Lamport, que também recebeu um prémio Turing em 2013, propôs uma variante da lógica temporal linear, designada Temporal Logic of Actions (TLA), que permite especificar não só as propriedades desejadas mas também o próprio sistema de transição. A grande novidade do TLA é a possibilidade de especificar predicados de transição (designados actions) que referem não só as variáveis do algoritmo, mas também o valor destas variáveis no estado seguinte (usando o nome da variável com uma plica). Combinando actions com o operador $\square$ conseguimos especificar quais os comportamentos válidos de um sistema de transição. A especificação de uma action tem tipicamente fórmulas de três naturezas distintas: guardas, que especificam quando é que pode ocorrer; efeitos, que especificam como se alteram certas variáveis quando ocorre; e frame conditions, que especificam quais as variáveis que não se alteram.

Por exemplo, o sistema de transição do relógio com horas pode ser especificado pela seguinte fórmula.

\[\mathit{HClock} \doteq (h = 0) \wedge \square ((h < 23 \wedge h' = h + 1) \vee (h = 23 \wedge h' = 0))\]

Esta especificação pode ser simplificada usando o resto da divisão.

\[\mathit{HClock} \doteq (h = 0) \wedge \square (h' = (h + 1) \% 24)\]

Para verificar se um sistema satisfaz uma determinada propriedade bastará então verificar se a mesma é implicada por esta fórmula que descreve o seu comportamento. Por exemplo, para verificar que o nosso relógio marca recorrentemente as 0 horas basta verificar a validade da seguinte fórmula.

\[\mathit{HClock} \Rightarrow \square \lozenge (h = 0)\]

Exercício: Especifique o sistema de transição do relógio defeituoso com uma fórmula em TLA.

Refinamento e Stuttering

O TLA também permite verificar se um sistema é um refinamento de outro, isto é, se um sistema é uma implementação de outro sistema mais abstrato. O refinamento mais típico consiste em acrescentar mais variáveis e transições que afetem apenas essas novas variáveis. Por exemplo, um relógio com horas e minutos é um refinamento de um relógio com apenas horas. Um relógio com horas e minutos pode ser especificado em TLA da seguinte forma.

\[\mathit{HMClock} \doteq (h = 0 \wedge m = 0) \wedge \square ((m = 59 \wedge h' = (h + 1) \% 24 \wedge m' = 0) \vee (m < 59 \wedge h' = h \wedge m' = m + 1))\]

Para verificar que este relógio especificado por $\mathit{HMClock}$ é de facto um refinamento do relógio especificado por $\mathit{HClock}$ basta verificar a seguinte implicação, que obriga a que todos comportamentos do relógio mais refinado são também comportamentos válidos do relógio mais abstrato.

\[\mathit{HMClock} \Rightarrow \mathit{HClock}\]

No entanto, esta implicação não é válida. Algumas das transições possíveis no relógio com minutos não são possíveis no relógio só com horas. Nomeadamente, as transições onde apenas os minutos se alteram não tem nenhuma transição correspondente no relógio só com horas, onde todas as transições implicam uma alteração na hora. Para permitir verificar refinamentos, qualquer especificação comportamental deve permitir que existam sempre passos de stuttering, onde nenhuma variável muda de valor, passos esses que irão corresponder às transições que afetam apenas as novas variáveis introduzidas pelo refinamento.

Para obrigar que existam sempre passos de stuttering o TLA não deixa usar as actions de qualquer forma. Em particular quando uma action é usada dentro do operador $\square$ irá sempre ser enquadrada numa disjunção que também admite um passo de stuttering. Dada uma action $A$, a action $[A]_t \doteq A \vee t’ = t$ significa que ou $A$ ocorreu ou a expressão $t$ manteve o seu valor ($t’$ é a expressão que resulta de acrescentar uma plica a todas as variáveis em $t$). Em particular se usarmos como expressão um tuplo com todas as variáveis de estado, então $[A]_t$ será válida sse $A$ for válida ou ocorreu um passo de stuttering, onde todas as variáveis mantiveram o seu valor. Pela mesma razão o TLA também não suporta o operador $\bigcirc$, pois com esse operador seria possível escrever fórmulas que impediriam o stuttering nalgumas situações.

As especificações dos nossos relógios em TLA seriam então as seguintes.

\[\mathit{HClock} \doteq (h = 0) \wedge \square [(h' = (h + 1) \% 24)]_h\] \[\mathit{HMClock} \doteq (h = 0 \wedge m = 0) \wedge \square [((m = 59 \wedge h' = (h + 1) \% 24 \wedge m' = 0) \vee (m < 59 \wedge h' = h \wedge m' = m + 1))]_{\langle h,m \rangle}\]

Com estas especificações a implicação que especifica o refinamento já é válida, como seria de esperar.

Note que o sistema de transição correspondente à especificação $\mathit{HClock}$ é agora o seguinte, onde temos lacetes em todos os estados.

O refinamento é uma técnica muito poderosa que permite o desenvolvimento incremental de um sistema, começando com uma especificação abstrata à qual vamos acrescentando detalhe até chegar a uma implementação. Uma das vantagens de usar este desenvolvimento incremental é que propriedades que já tenham sido verificadas numa especificação mais abstrata são necessariamente válidas na especificação mais refinada, e, como o sistema de transição mais abstrato é tipicamente muito mais pequeno, a sua verificação é muito mais eficiente.

Sintaxe e Semântica do TLA

Como já vimos as actions poderem ser usadas no operador $\square$ desde que haja garantias de que o stuttering é possível. O TLA também permite utilizar actions dentro do operador $\mathsf{ENABLED}$, que transforma uma action $A$ num predicado normal que verifica se $A$ pode ocorrer num estado. Por exemplo $\mathsf{ENABLED}\ (h = 23 \wedge h’ = 0) \equiv h = 23$.

Outra diferença do TLA em relação à lógica temporal linear apresentada anteriormente é que o TLA é uma lógica de primeira ordem, ou seja permite a utilização de quantificadores. A gramática da lógica TLA é então definida da seguinte forma.

\[\begin{array}{lcl} \mathit{formula} & \doteq & \mathit{predicate}\\ & \mid & \mathsf{ENABLED}\ \mathit{action}\\ & \mid & \neg \mathit{formula}\\ & \mid & \mathit{formula} \wedge \mathit{formula}\\ & \mid & \exists \mathit{variable} \cdot \mathit{formula}\\ & \mid & \square\ \mathit{formula}\\ & \mid & \square [\mathit{action}]_\mathit{expr} \end{array}\]

Nesta definição, $\mathit{predicate}$ representa um predicado arbitrário envolvendo variáveis de estado (variáveis flexíveis) ou variáveis quantificadas (variáveis rígidas), $\mathit{action}$ é um predicado de transição arbitrário envolvendo variáveis de estado (com ou sem plica) ou variáveis quantificadas, e $\mathit{expr}$ é uma expressão arbitrária envolvendo variáveis de estado (tipicamente um tuplo com todas as variáveis de estado).

A semântica do TLA pode ser definida da seguinte forma (onde $F$ e $G$ representam fórmulas arbitrárias, $P$ um predicado arbitrário, e $A$ uma action arbitrária). Note que, ao contrário dos predicados normais, a validade das actions tem que ser determinada em pares de estados consecutivos.

\[\begin{array}{lcl} s_0,s_1,\ldots \models P & \equiv & s_0 \models P\\ s_0,s_1,\ldots \models A & \equiv & s_0,s_1 \models A\\ s_0,s_1,\ldots \models \mathsf{ENABLED}\ A & \equiv & \exists s_1 \cdot s_0,s_1 \models A\\ s_0,s_1,\ldots \models \neg F & \equiv & s_0,s_1,\ldots \not\models F \\ s_0,s_1,\ldots \models \exists x \cdot F & \equiv & \exists x \cdot s_0,s_1,\ldots \models F \\ s_0,s_1,\ldots \models F \wedge G & \equiv & s_0,s_1,\ldots \models F \wedge s_0,s_1,\ldots \models G\\ s_0,s_1,\ldots \models \square F & \equiv & \forall i \ge 0 : s_i,s_{i+1},\ldots \models F \\ s_0,s_1,\ldots \models \square [A]_t & \equiv & \forall i \ge 0 : s_i,s_{i+1},\ldots \models A \vee t' = t \end{array}\]

Tal como na lógica temporal linear podemos ter operadores derivados, nomeadamente o operador $\lozenge$ definido como $\lozenge F \doteq \neg \square \neg F$.

Condições de justiça

Infelizmente, nenhuma das propriedades de liveness especificadas acima são válidas na especificação $\mathit{HClock}$ que admite stuttering. Por exemplo, a propriedade $\lozenge (h = 12)$ é inválida porque um dos comportamentos possíveis é o sistema fazer stuttering para sempre no estado inicial.

Embora permitir o stuttering seja desejável, não é razoável que o sistema, tendo possibilidade de executar uma action opte por fazer stuttering para sempre. Para eliminar estes comportamentos não razoáveis, ou não “justos” para as actions na medida em que estas não tem oportunidade de executar, podemos impor o que designa de condições de justiça (fairness) no sistema. O objetivo destas condições de justiça é garantir que quando uma action está “permanentemente” enabled ela irá inevitavelmente ocorrer. Dependendo da definição de “permanentemente” podemos ter duas variações das condições de justiça: a justiça fraca (weak fairness), onde “permanentemente” significa continuamente; e a justiça forte (strong fairness), onde “permanentemente” significa recorrentemente.

Dada uma action $A$ a condição de justiça fraca pode ser especificada da seguinte forma:

\[\square (\square \mathsf{ENABLED} A \Rightarrow \lozenge A)\]

Esta fórmula é equivalente à seguinte:

\[\lozenge \square \mathsf{ENABLED} A \Rightarrow \square \lozenge A\]

Infelizmente esta fórmula não pode ser usada diretamente para impor a justiça fraca porque não é uma fórmula TLA (relembre que as actions não podem ser usadas de forma arbitrária). No entanto, a seguinte variante já é uma fórmula em TLA, onde $\langle A \rangle_t \doteq A \wedge t’ \neq t$ significa que $A$ ocorreu e teve algum efeito no estado.

\[\lozenge \square \mathsf{ENABLED} \langle A \rangle_t \Rightarrow \square \lozenge \langle A \rangle_t\]

Esta variante é uma fórmula em TLA devido à dualidade entre os operadores $\square$ e $\lozenge$, pois $\square \lozenge \langle A \rangle_t \equiv \neg \lozenge \square [\neg A]_t$.

A justiça forte pode ser especificada da seguinte forma.

\[\square \lozenge \mathsf{ENABLED} \langle A \rangle_t \Rightarrow \square \lozenge \langle A \rangle_t\]

Como estas condições são muito comuns, o TLA tem abreviaturas para as mesmas, nomeadamente $\mathsf{WF}_t(A)$ e $\mathsf{SF}_t(A)$.

Para garantir que as propriedades de liveness são válidas na especificação do relógio basta impor a justiça fraca, sendo a especificação final do mesmo a seguinte.

\[\mathit{HClock} \doteq (h = 0) \wedge \square [(h' = (h + 1) \% 24)]_h \wedge \mathsf{WF}_h(h' = (h + 1) \% 24)\]

A linguagem TLA+

A lógica TLA está na base da linguagem de especificação TLA+, que enriquece a lógica base com primitivas para estruturação de especificações de grande dimensão. Por exemplo, permite introduzir definições auxiliares e tem um sistema de módulos. É uma linguagem não tipada, podendo as variáveis tomar valores tais como inteiros, conjuntos, funções, tuplos ou records. A maioria dos operadores tem uma sintaxe ASCII relativamente standard, sendo que para alguns é usada a sintaxe do LaTeX (também criado por Leslie Lamport). Para usar algumas operações pode ser necessário importar um dos módulos pré-definidos. Um sumário da sintaxe do TLA+ pode ser encontrado aqui.

Uma especificação em TLA+ tem que ser escrita entre os delimitadores ---- MODULE name ---- e ==== (podem ser usados mais - e =). Para introduzir uma definição usa-se o ==. A sintaxe dos vários operadores usados nas definições pode ser consultada no documento referido acima. Para além de permitir introduzir definições, o TLA+ tem as seguintes palavras reservadas:

• EXTENDS, que serve para importar módulos.
• CONSTANTS, que serve para declarar quais os nomes dos parâmetros constantes do algoritmo.
• ASSUME, que serve para especificar assunções sobre os referidos parâmetros.
• VARIABLES, que serve para declarar quais as variáveis flexíveis que definem o estado do algoritmo.

Como a linguagem é não-tipada, tuplos e sequências são equivalentes e escrevem-se entre os delimitadores << e >>. Dentro de uma action se quisermos especificar que uma expressão mantém o seu valor entre o pré- e o pós-estado podemos usar a palavra reservada UNCHANGED. Quando usada com um tuplo de variáveis permite facilmente especificar frame conditions.

O relógio só com horas pode ser especificado em TLA+ da seguinte forma. Nesta especificação é importado o módulo Naturals para se poderem usar as operações aritméticas.

----- MODULE HourClock -----

EXTENDS Naturals

VARIABLES h

Init == h = 0

Tick == h' = (h + 1) % 24

HClock == Init /\ [][Tick]_h /\ WF_h(Tick)

Prop1 == [] (h /= 24)
Prop2 == <> (h = 12)
Prop3 == []<> (h = 0)

============================

A ferramenta TLA+ Toolbox permite, entre outras funcionalidades, validar a correção sintática de especificações em TLA+. No entanto, nesta UC recomendamos utilizar a extensão do TLA+ para o VSCode, cuja interface é mais amigável.

Exercício: Instale a extensão do TLA+ para o VSCode e valide a sintaxe da especificação anterior.

Exercício: Especifique em TLA+ o relógio defeituoso.

O model checker TLC

A linguagem TLA+ tem um model checker associado, designado TLC, que pode ser usado para verificar propriedades temporais de numa especificação. Este model checker utiliza uma técnica explícita semelhante à que foi descrita acima, mas implementada de uma forma extremamente eficiente tirando partido do paralelismo permitido pela maioria dos processadores atuais.

O TLC não consegue verificar qualquer propriedade especificada em TLA+. Quer a especificação do algoritmo quer a especificação da propriedade tem que seguir um certo padrão, que iremos descrever brevemente a seguir (mais detalhes podem ser encontrados no capítulo 14 do livro Specifying Systems). No entanto, este padrão é bastante permissivo e incluí a maioria das propriedades relevantes em algoritmos.

No caso da especificação do comportamento o TLC assume que a mesma segue o padrão Init /\ [][Next]_vars, onde Next é uma disjunção de actions (possivelmente no contexto de um quantificador existencial). A restrição mais importante é que quer no predicado Init, quer nas várias actions, tem que ser definido o valor de todas as variáveis usando uma atribuição ou uma escolha não determinística da forma x \in S (no predicado Init) ou x' \in S (nas actions), sendo que S é um conjunto finito de valores. Numa action, a expressão no lado direito de uma atribuição ou escolha não determinística podem fazer referência ao novo valor de outra variável, desde que este tenha sido definido anteriormente. Este “anteriormente” significa que o TLC interpreta as conectivas lógicas numa action de forma sequencial. Todos os quantificadores usados têm também que ser bounded, ou seja a variável quantificada tem que iterar sobre um conjunto finito.

Quanto às propriedades a verificar, as mesmas têm que ser a conjunção de fórmulas TLA que pertencem às seguintes classes:

• Predicados de estado, sem quantificadores temporais nem plicas (podem incluir predicados da forma $\mathsf{ENABLED}\ A$, onde $A$ é uma action).
• Invariantes da forma $\square\ P$, onde $P$ é um predicado de estado.
• Invariantes de transição da forma $\square [A]_t$, onde $A$ é uma action e $t$ uma expressão envolvendo as variáveis de estado.
• Fórmulas temporais simples, isto é, qualquer fórmula em lógica temporal linear clássica sem actions (combinação de predicados de estado usando conectivas lógicas e operadores temporais), ou combinações deste tipo de fórmulas com fórmulas do tipo $\lozenge \square [A]_t$ usando conectivas lógicas.

Para usar o TLC é necessário começar por criar um ficheiro de configuração (com o mesmo nome do ficheiro com a especificação TLA+, mas com a extensão .cfg em vez de .tla) que define o valor de todas os parâmetros constantes, qual a fórmula que especifica o comportamento e quais a propriedade ou propriedades a verificar. Para verificar as três propriedades do relógio com horas teremos que criar o seguinte ficheiro de configuração.

SPECIFICATION HClock
PROPERTIES Prop1 Prop2 Prop3

Neste caso, tal como esperado, todas as propriedades são válidas.

Exercício: Use o TLC para verificar se as 3 propriedades são válidas no relógio defeituoso.

Verificação de refinamento com o TLC

Considere agora a seguinte especificação do relógio com horas e minutos em TLA+.

----- MODULE HourMinuteClock -----

EXTENDS Naturals

VARIABLES h,m

Init == h = 0 /\ m = 0

Tick == (m = 59 /\ h' = (h + 1) % 24 /\ m' = 0) \/ (m < 59 /\ UNCHANGED h /\ m' = m + 1)

HMClock == Init /\ [][Tick]_<<h,m>> /\ WF_<<h,m>>(Tick)

============================

Para verificar que esta especificação é um refinamento da especificação do relógio apenas com horas poderíamos copiar a especificação do mesmo para este módulo e usar o TLC para verificar que a mesma é satisfeita. No entanto, para evitar repetir especificações, podemos também simplesmente importar essa especificação do módulo HourClock. No entanto não podemos fazer isso usando o EXTENDS pois essa keyword importa não só as definições mas também as declarações e iríamos ficar uma declaração repetida da variável h (de facto também as definições Init e Tick ficariam duplicadas o que originaria um erro). Em alternativa podemos utilizar a keyword INSTANCE para importar um módulo. Neste caso apenas as definições são importadas, pelo que teremos que dizer como é que as variáveis e constantes declaradas no módulo importado se definem à custa das variáveis e constantes declaradas no módulo que faz a importação. Esse mapeamento é feito com a keyword WITH. Neste caso queremos que a variável h declarada no módulo HourClock corresponda à variável h declarada no módulo HourMinuteClock pelo que podemos fazer a importação usando o comando INSTANCE HourClock WITH h <- h. Quando uma declaração do módulo importado é mapeada na mesma declaração podemos omitir o respetivo mapeamento, logo neste caso podemos simplesmente usar o comando INSTANCE HourClock. No entanto, como temos definições repetidas nos dois módulos (Init e Tick) temos que fazer a importação para um namespace diferente (algo que o EXTENDS também não permite) e aceder à especificação qualificando a mesma com o namespace definido. A especificação final do módulo HourMinuteClock seria a seguinte.

----- MODULE HourMinuteClock -----

EXTENDS Naturals

VARIABLES h,m

Init == h = 0 /\ m = 0

Tick == (m = 59 /\ h' = (h + 1) % 24 /\ m' = 0) \/ (m < 59 /\ UNCHANGED h /\ m' = m + 1)

HMClock == Init /\ [][Tick]_<<h,m>> /\ WF_<<h,m>>(Tick)

Abstract == INSTANCE HourClock

HClock == Abstract!HClock

============================

Podemos agora usar o TLC para verificar que a propriedade HClock é válida, ou seja, o relógio com minutos é de facto um refinamento do relógio só com horas, e, por isso, as três propriedades que eram válidas continuam a ser válidas (não sendo necessário repetir a verificação das mesmas).

A possibilidade de fazer mapeamentos no INSTANCE permite que haja refinamentos mais sofisticados, onde não são simplesmente acrescentadas novas variáveis. Podemos, por exemplo, especificar um relógio em que as horas são apresentadas no formato AM/PM e verificar que esse relógio é também um refinamento do relógio inicial. Para verificar este refinamento temos que especificar como é que as horas no formato de 24 horas são calculadas a partir das horas no formato de 12 horas mais a indicação se estamos no período AM ou PM. A especificação desse relógio em TLA+ seria a seguinte.

----- MODULE AmPmHourClock -----

EXTENDS Naturals

VARIABLES h,am

Init == h = 0 /\ am = TRUE

Tick == (h = 11 /\ h' = 0 /\ am' = ~am) \/ (h < 11 /\ h' = h + 1 /\ UNCHANGED am)

AmPmHClock == Init /\ [][Tick]_<<h,am>> /\ WF_<<h,am>>(Tick)

Abstract == INSTANCE HourClock WITH h <- IF am THEN h ELSE h + 12

HClock == Abstract!HClock

============================