Model Checking: Exploração Exaustiva do Espaço de Estados

• Descrever o model checking com estados explícitos como um algoritmo de busca em grafo que opera sobre estados alcançáveis, e não como um procedimento de amostragem.
• Explicar como a checagem de segurança se reduz a uma simples busca de alcançabilidade e reconstruir um contraexemplo a partir da própria informação de predecessores da busca.
• Explicar por que a checagem de vivacidade exige raciocinar sobre ciclos e ligar isso aos contraexemplos em laço (lasso) apresentados para a LTL.
• Explicar o que a checagem "on-the-fly" ganha na prática, e por que ela importa quando um contraexemplo é muito menor que o espaço de estados completo.
• Distinguir uma execução de simulação aleatória de um model checking exaustivo genuíno.

transition-systems-and-kripke-structures forneceu o objeto a ser checado (um grafo finito e rotulado de estados e transições), e linear-temporal-logic-ltl, junto com ctl-and-branching-time-logic, forneceu as linguagens para enunciar o que deve ser verdade sobre ele. Este conceito é onde essas duas peças de fato se encontram: o model checking é o algoritmo que recebe um sistema de transição finito e uma propriedade de lógica temporal e transforma a combinação dos dois em uma pergunta concreta que um computador consegue responder por completo, por busca, e não por prova simbólica.

A palavra "exaustivo" aqui não é linguagem de marketing, e vale se deter exatamente no que ela compra, porque é o motivo inteiro de o model checking ser de natureza diferente dos testes, do mesmo jeito que uma prova em lógica de Hoare é. Ao contrário dos testes, que amostram um subconjunto escolhido à mão dos comportamentos possíveis de um sistema e nunca conseguem, por construção, excluir uma falha escondida em algum lugar fora dessa amostra, um model checker com estados explícitos visita todo estado alcançável a partir dos estados iniciais do modelo, sem nenhuma amostragem em parte alguma do processo; se a busca terminar e relatar que a propriedade vale, isso de fato significa que a propriedade vale em todo estado alcançável e em todo caminho alcançável, e não só nos estados que alguém calhou de pensar em checar.

O model checking LTL on-the-fly do SPIN é a ilustração concreta em que esta disciplina se ancora para mostrar como isso fica como ferramenta de engenharia real e utilizável, e não como um algoritmo puramente teórico: ele recebe um modelo de um sistema concorrente e uma propriedade LTL e produz ou uma prova de que a propriedade vale em todo o espaço de estados explorado, ou um rastro de contraexemplo genuíno e concreto que um engenheiro pode percorrer passo a passo; exatamente o tipo de evidência acionável que testing-shows-presence-proof-shows-absence já defendeu ser mais valiosa que uma mensagem abstrata de "verificação falhou".

Exploração com estados explícitos

O esqueleto algorítmico por baixo do model checking com estados explícitos é uma busca em grafo comum, adaptada à estrutura específica de uma estrutura de Kripke. Ela começa nos estados iniciais do modelo e calcula repetidamente os sucessores (os estados alcançáveis por uma transição a partir de estados já descobertos), acrescentando cada estado recém-descoberto a um conjunto de visitados. Esse conjunto de visitados não é um detalhe de contabilidade incidental; é o que impede a busca de revisitar estados sem fim sempre que o grafo de transições contém ciclos, o que os espaços de estados de sistemas reais muitas vezes contêm (um sistema que consegue voltar a um estado em que já esteve é, afinal, exatamente o que torna possível o comportamento reativo ou de longa duração). Em cada estado que a busca visita, ela checa a condição de estado ruim ou a condição do produto com o autômato temporal em que a propriedade sendo verificada se traduz, e a busca termina quando todo estado alcançável foi visitado e checado.

Checagem de segurança

Checar uma propriedade de segurança como AG ¬bad ou □ ¬bad se reduz, como o exemplo de segurança global de ctl-and-branching-time-logic já mostrou para a CTL, a uma única pergunta de alcançabilidade: algum estado rotulado bad é alcançável a partir dos estados iniciais? Se a busca visitar todo estado alcançável e nunca encontrar um rotulado bad, a propriedade de segurança vale, de forma completa e exaustiva, com a própria busca constituindo a prova. Se um estado rotulado bad for encontrado, a busca não se limita a relatar a falha: como ela naturalmente registra, para cada estado visitado, a partir de qual estado ele foi alcançado, essa cadeia de predecessores pode ser percorrida de volta do estado ruim encontrado até um estado inicial, reconstruindo um rastro de contraexemplo concreto, passo a passo, que corresponde exatamente ao padrão de prefixo ruim finito já estabelecido para violações de segurança em linear-temporal-logic-ltl.

Checagem de vivacidade

Propriedades de vivacidade resistem a essa mesma redução porque sua violação, como já estabelecido, não é um fato sobre um único prefixo finito: é um fato sobre toda a cauda infinita de um caminho, testemunhado concretamente por um laço: um prefixo finito que leva a um ciclo em que o evento prometido nunca ocorre. Encontrar esse laço é um problema de busca genuinamente diferente de encontrar um único estado ruim, porque exige que a busca reconheça não só "este estado é ruim", mas "este ciclo, tomado como um todo, evita o evento bom para sempre". A busca em profundidade aninhada (nested depth-first search) é a técnica clássica, com estados explícitos, construída exatamente para isso: ela faz uma busca em profundidade externa sobre os estados alcançáveis e, para cada estado pelo caminho que poderia plausivelmente iniciar um ciclo ruim, faz uma busca em profundidade interna procurando especificamente um caminho de volta a esse mesmo estado (ou a um equivalente) que nunca passe pelo evento bom; encontrar esse ciclo é precisamente encontrar o laço que testemunha a violação de vivacidade.

Checagem on-the-fly

Um model checker não precisa construir o grafo de estados inteiro de antemão, de uma vez, antes de começar a procurar uma violação; é exatamente essa a ideia de eficiência a que "on-the-fly" se refere, e é exatamente o que dá nome à abordagem do SPIN. Em vez disso, os sucessores são gerados de forma preguiçosa, só quando a busca de fato precisa deles, e a busca pode relatar um contraexemplo no momento em que o encontra, sem nunca ter explorado o resto de um espaço de estados que pode ser imensamente maior que a parte de fato necessária para localizar o bug. Essa distinção acaba importando muito na prática, e não só como um detalhe de implementação: muitos bugs reais são alcançáveis por uma sequência comparativamente curta de transições a partir do estado inicial, mesmo dentro de modelos cujo espaço de estados alcançável total é grande demais para ser enumerado por completo; a busca on-the-fly consegue encontrar esse bug rápido explorando só a parte relevante do grafo, enquanto uma abordagem que insistisse em construir o grafo completo primeiro precisaria pagar o custo inteiro do problema da explosão do espaço de estados, que state-space-explosion-and-symbolic-model-checking trata como o obstáculo central de engenharia da disciplina, antes mesmo de começar a procurar.

Erro alcançável

Considere um sistema de transição com estado inicial Idle e transições Idle → Busy e Busy → Error (mais, digamos, Busy → Idle para um caminho normal de conclusão, embora isso seja irrelevante para esta checagem específica). Checando a propriedade de segurança "nunca Error" por busca com estados explícitos: o algoritmo visita Idle primeiro, descobre Busy como sucessor e o visita, depois descobre Error como sucessor de Busy e o visita também; nesse ponto, a busca percebe que Error carrega o rótulo proibido. Percorrer a cadeia de predecessores de volta a partir de Error (Error foi alcançado a partir de Busy, que foi alcançado a partir de Idle, o estado inicial) reconstrói o rastro de contraexemplo concreto Idle, Busy, Error, que corresponde exatamente ao padrão de prefixo ruim finito de uma violação de segurança e dá a um engenheiro a sequência precisa de transições que leva ao estado proibido.

Exclusão mútua com dois processos

Considere modelar dois processos, cada um podendo estar em uma de três localizações: Outside (sem tentar entrar na seção crítica), Waiting (tentando entrar) ou Critical (dentro da seção crítica). Um único estado combinado registra as localizações dos dois processos ao mesmo tempo, e o model checker explora todo entrelaçamento possível dos passos individuais dos dois processos (toda ordem em que qualquer um dos processos possa avançar, já que um protocolo de exclusão mútua correto precisa valer sob qualquer entrelaçamento que um escalonador possa escolher, e não só sob uma ordem conveniente). O estado ruim procurado é qualquer estado combinado em que as localizações dos dois processos sejam Critical ao mesmo tempo. Se a busca exaustiva visitar todo estado combinado alcançável, em todo entrelaçamento que o modelo permite, e nunca encontrar um em que as duas localizações sejam Critical ao mesmo tempo, a exclusão mútua fica provada para esta abstração finita do protocolo; uma garantia que cobre todo entrelaçamento de escalonamento possível que o modelo admite, e não só os entrelaçamentos que alguém calhou de testar à mão.

Laço de vivacidade

Considere um rastro que começa com o prefixo Idle, Requested, depois do qual o sistema entra em um ciclo repetitivo Requested, Waiting, Requested, Waiting, ... que continua para sempre, sem o rótulo Acknowledged aparecer em nenhum ponto desse ciclo. É precisamente um laço no sentido já desenvolvido para a LTL: um prefixo finito (Idle, Requested) que leva a um ciclo (Requested, Waiting) que evita o evento prometido (Acknowledged) para sempre depois de entrar nele. Esse laço refuta completamente a propriedade de vivacidade "toda requisição acaba sendo confirmada", porque o caminho infinito que ele representa (o prefixo seguido do ciclo repetido sem fim) genuinamente nunca chega a um estado rotulado Acknowledged em nenhum ponto, satisfazendo exatamente a condição semântica de uma violação de vivacidade; e é exatamente o tipo de objeto que a busca em profundidade aninhada é construída para descobrir diretamente, encontrando um ciclo alcançável a partir do prefixo que revisita um estado já visto sem que o evento exigido ocorra pelo caminho.

• Chamar uma execução de simulação aleatória de "model checking". Uma execução de simulação (mesmo muito longa, ou muitas delas repetidas) explora exatamente um caminho (ou uma amostra escolhida à mão de caminhos) pelo espaço de estados, o que é fundamentalmente uma atividade de amostragem, no mesmo sentido dos testes; ela não consegue, por construção, excluir uma falha escondida ao longo de um caminho que a simulação nunca calhou de tomar, enquanto a exaustividade do model checking genuíno é precisamente o que testes e simulação não têm.
• Esquecer de incluir as transições do ambiente no espaço de estados modelado. Um modelo que só representa o sistema sob teste, omitindo em silêncio a gama de movimentos que um ambiente ou escalonador imprevisível poderia de fato fazer, está checando uma afirmação mais estreita e mais fácil do que a garantia real do sistema exige; qualquer propriedade provada contra esse modelo incompleto não traz nenhuma garantia sobre comportamentos que as transições omitidas do ambiente poderiam ter disparado.
• Checar só uma propriedade de segurança quando o requisito real é uma propriedade de vivacidade, ou o contrário. Como o contraste algorítmico acima deixa claro, elas exigem técnicas de busca genuinamente diferentes; uma checagem de segurança que nunca procura ciclos nunca vai pegar uma violação de vivacidade, por mais minuciosamente que explore os estados alcançáveis, porque a falha que uma violação de vivacidade representa é uma propriedade de uma cauda infinita, e não de um único estado alcançável.
• Presumir que não encontrar contraexemplo em uma busca limitada prova a propriedade ilimitada. Uma busca on-the-fly ou de outro modo incompleta que só explorou parte do espaço de estados alcançável (por um limite de profundidade explícito, um timeout ou uma estratégia de exploração incompleta) e não encontrou violação não provou com isso que a propriedade vale em todo lugar; a exaustividade genuína do model checking exige que a busca tenha de fato coberto todo estado alcançável, uma distinção a que the-limits-of-verification volta explicitamente ao distinguir resultados corretos e completos de resultados apenas corretos, mas limitados.

O model checking com estados explícitos transforma uma propriedade temporal e uma estrutura de Kripke finita em um problema de busca em grafo: a checagem de segurança se reduz à simples alcançabilidade, com a cadeia de predecessores de um estado violador reconstruindo um rastro de contraexemplo finito e concreto, enquanto a checagem de vivacidade exige a técnica genuinamente diferente de procurar um laço (um ciclo, alcançável a partir dos estados iniciais, que evita o evento prometido para sempre), usando algoritmos como a busca em profundidade aninhada, construídos exatamente para essa estrutura. A exploração on-the-fly, exemplificada pelo SPIN, gera sucessores só conforme necessário, em vez de construir o grafo de estados inteiro de antemão, permitindo que uma busca encontre rapidamente um contraexemplo comparativamente curto mesmo dentro de um modelo cujo espaço de estados alcançável total é enorme. Essa enormidade do espaço de estados alcançável, só indicada aqui, vira o obstáculo central de engenharia da disciplina já no próximo conceito, state-space-explosion-and-symbolic-model-checking.