Model Checking

Slides

1. Model Checking

1.1. TLC (LAMPORT, 2002)

Explicit-State model checker

  • Enumera todos os estados
  • Usa um grafo direcionado com estados e transições (reachability graph) e uma fila de estados para checar
  • Provavelmente, o tipo de model checker que um de nós escreveria se fôssemos tentar (sem pesquisar um monte antes)

1.2. Apalache (KONNOV; KUKOVEC; TRAN, 2019)

Model checker simbólico

  • Traduz a especificação para um conjunto de restrições (sem quantificação)
  • Usa um SMT solver para verificar a satisfabilidade das restrições

Bounded model checking

  • Necessário definir um número máximo de passos (bound) para o qual gerar restrições. A verificação se dá dentro desse limite, podendo haver estados atingíveis fora desse limite que não satisfazem a propriedade.

1.3. SMT

  • Generalização de problemas SAT

    • SAT: Problema da satisfabilidade Booleana
    • SMT: Satisfabilidade “modulo” teorias

      • modulo” no sentido de “dentro de”
      • Permite mais elementos: inteiros, reais, arrays, etc

Z3 (DE MOURA; BJØRNER, 2008):

1.4. Resolvendo SMT com Z3

(declare-fun p () Bool)
(declare-fun q () Bool)
(assert (implies p q))
(assert p)
(assert (not q))
(check-sat)

Resultado: unsat

(declare-fun p () Bool)
(declare-fun q () Bool)
(assert (implies p q))
(assert p)
(assert q)
(check-sat)

Resultado: sat

1.5. Resolvendo SMT com inteiros

(declare-const a Int)
(declare-const b Int)
(assert (= (+ a b) 20))
(assert (= (+ a (* 2 b)) 10))
(check-sat)
(get-model)

Resultado: sat

1.6. Simulação simbólica

Podemos classificar não-determinismo em dois tipos:

  • Não-determinismo de dados (data non-determinism)
    • 1.to(10).oneOf()
  • Não-determinismo de controle (control-flow non-determinism)
    • any { A, B }

Simulação simbólica:

  • Model Checkers: exaustivamente checam todos os dados e fluxos possíveis
  • Simuladores aleatórios: aleatoriamente checam alguns dados e fluxos
  • Simulador simbólico: aleatóriamente checa alguns fluxos, mas considerando todos os dados possíveis

1.7. Referências

DE MOURA, L.; BJØRNER, N. Z3: an efficient smt solverProceedings of the theory and practice of software, 14th international conference on tools and algorithms for the construction and analysis of systems. Anais.: Tacas’08/etaps’08.Budapest, Hungary: Springer-Verlag, 2008
KONNOV, I.; KUKOVEC, J.; TRAN, T.-H. Tla+ model checking made symbolic. Proc. acm program. lang., v. 3, n. OOPSLA, Oct. 2019.
LAMPORT, L. Specifying systems: The tla+ language and tools for hardware and software engineers. Boston: Addison-Wesley, 2002.