Python : Looking for Model Checker tool and results to CNF convertion

Question

I would like to test my code with a modell checker and make a FSM out of it in an automated way. For this I need a modell checker and convert the FSM results to CNF.

Any advice how I can do this in Python ? I only know CBMC but thi is limited to C.

Thanks Adrian

Answer 1

Python is not a language suited to model checking, for example duck typing lets a lot of freedom to raise exceptions. If your Python code is essentially procedural, then you may try to first convert it to C using py2c or some equivalent.

Then use modex to extract a Promela model from the C code. This last step is called abstraction. Then you can use the SPIN model checker to verify the properties of interest.

If CNF stands for "Conjunctive Normal Form", then I do not understand how CNF relates to the results of model checking. Model checking yields either a:

• "yes, your model models the logic formula you provided" or

• "no it doesn't, and here's a counterexample why not".

The CNF is a particular syntactic form for Boolean formulas.

If you mentioned CNF as relevant to bounded model checking with CBMC and the SAT solving involved in that, then please note that SPIN accepts as input Kripke models expressed using the Promela language. So you don't need to convert anything to a Boolean formula and in addition you can run full liveness verification checks.

This list of tools includes model checkers. In particular, if you want to write a converter from Python to Promela, then you may find useful the following:

• ast module of the CPython standard library: abstract syntax tree for the Python language (the tree is constructed using CPython's parser)
• promela Python package: a parser and abstract syntax tree for Promela, implemented in Python
• promela-metamodel
• ocaml library for promela
• pi2promela
• Program to Promela converter.

Also, note that a "FSM" (Finite State Machine) is a transducer, not a Kripke structure. A transducer has both inputs and outputs. It reacts to inputs by producing outputs. It is the result of synthesis in an adversarial setting, where one has an environment (controlling the inputs) and a system (controlling the outputs), and wants to synthesize a strategy that satisfies some specification expressed in the form of a logic formula. There exist several tools for solving this problem. The result is a Mealy machine, or a Moore machine (they are different and not equivalent), both are types of transducers.

A transducer is not a Kripke structure (or transition system, though the latter term is used typically wrongly, so better to refer to a Kripke structure or model, that can be represented by a graph with nodes labeled by propositions that you refer to in the logic formula that is the desired specification).

Observe how synthesis differs from verification (model checking is a form of verification):

• closed-system synthesis (no environment) takes a formula and synthesizes a model satisfying it, in the form of a Kripke structure.

• closed-system verification takes a model and a desired formula, and then checks whether the model satisfies the specification.

Closed-system synthesis can be done also by using a "partial" model, in the sense that the model is an additional constraint to the formula. In that case, the result of synthesis must both satisfy the formula and be a "submodel" of the partial model.

Open-system synthesis can be performed with a logic formula as input, then by solving a game between the system and the environment, we obtain a transducer that implements a strategy for the system to satisfy the logic formula, irrespective of how the environment chooses to play (provided the environment complies with the logic formula).

Notice the difference between:

• a transducer (FSM), relevant in open-system synthesis, and

• a finite transition system (FTS) or Kripke structure that is given as input to closed-system synthesis.

Aside: model checkers typically take as input closed systems, so modeling an environment in a closed-system setting has to be done by introducing uncontrolled nondeterminism in the transition system.

---

The above description about open and closed systems, formulas, finite-state machines, finite-transition systems, synthesis, and verification, can be understood simply and in a unified way using TLA+:

• formulas are Boolean-valued expressions, for example the formulas:

  • a /\ ~ b and
  • (x = 1) /\ (y \in Nat).

• finite-state machines and finite-transition systems are not really different, they are just syntactic sugar for (temporal) formulas

• what is usually different is how we use graph-like constructs in verification, and how we use them in synthesis:

  • In verification, a graph-like construct that describes what steps (transitions) the system can take is sometimes called a "finite transition system". It is the input to verification.

  • In synthesis, a (synthesized) graph-like construct that describes how the system ("controlled" part of the world) changes when certain changes occur in the system's environment (the rest of the world), is sometimes called a "finite state machine".

  A finite state machine as a term can refer to a finite transition system. The essence is that we describe the world by specifying how "state" changes. This concept is not limited to finite constructs. So writing "state machine" suffices.

• informally, a closed system is a collection of behaviors of part of the world that can be described by a set of values.

• informally, an open system is a collection of behaviors of part of the world that includes unconstrained behavior: namely whatever behavior is described by a violation of assumptions on the environment.

• verification is quantifier elimination in a formula with a single quantifier. In other words, if:

  • the operator System(variable) describes the system's behavior in terms of variable variable, and
  • the operator Specification(variable) describes the desired system behavior,

  then verification is the activity of proving that the formula \AA variable: System(variable) => Specification(variable) is a theorem:

  THEOREM \AA variable:  System(variable) => Specification(variable)
  

  In words, this theorem asserts that for all temporal evolutions of the variable variable, if the formula System(variable) is TRUE of an evolution of variable, then the formula Specification(variable) too is TRUE of that evolution of variable.

  To connect with the above description in terms of finite transition systems and model checking:

  • The formula System(variable) describes in predicate logic, temporal logic, and set theory, what the transition system "graph" describes: how the system can behave (System(variable) can include liveness formulas, whereas when using transition systems, liveness is usually expressed in some other way, e.g., by using "automata", which are just graph-like ways of writing liveness formulas).

  • The formula Specification(variable) describes the requirements on the system, which in model checking are usually expressed using temporal logic, or automata, or a combination of both. (An automaton is a graph-like description of a state machine, together with an annotation of nodes that is interpreted as describing requirements on how often those nodes should be visited over the entire infinite behavior).

  • What a model checker does is attempt to prove the above theorem. This activity is equivalent to reasoning about whether the quantified temporal formula is TRUE, including reasoning about the logical implication =>.

• realizability (the decision problem that corresponds to synthesis) is quantifier elimination in a formula with alternation of quantifiers.

  In simplified form, realizability is the activity of proving that the formula \E system: \AA env_variable: \AA sys_variable: BehaviorOf(system, env_variable, sys_variable) => Specification(env_variable, sys_variable) is a theorem:

  THEOREM
      \E system:
          \AA env_variable:
          \AA sys_variable:
              BehaviorOf(system, env_variable, sys_variable)
              => Specification(env_variable, sys_variable)
  

  To compare with verification as formalized above, we here have to reason about two different quantifiers: (constant) existential quantification (\E) and (temporal) universal quantification (\AA). When "verifying" in the sense of model checking, we had to reason about only one kind of quantifier.

  Also, "verification" in this discussion refers specifically to model checking. If one says "verification" to mean "proof", then clearly both model checking and controller synthesis are proof activities, where the objective in each case is to prove a theorem. What differs in each case is the form of the theorem, which changes how computationally expensive this activity is.

  To connect with the above description in terms of finite state machines ("transducers"):

  • system is a value (set in set theory) within TLA+ that is constant throughout the temporal behavior, and describes what the designed system looks like. It is this value that is generated by a synthesis tool, i.e., the tool designs a system that solves the problem.

    So the "transducer" or "finite state machine" mentioned earlier corresponds to this system value, via the operator BehaviorOf, as described in the next item.

  • BehaviorOf(system, env_variable, sys_variable) is a formula that describes how the world behaves when we deploy a system defined by the value system.

    Specifically, the part of the world that we say something about is represented by the variables sys_variable, env_variable.

    The variable sys_variable is understood as describing the state of the "system" being designed, and the variable env_variable is thought of as the "rest of the world".

    More precisely, the formula BehaviorOf(system, env_variable, sys_variable) is a description in logic and set theory of the graph-like "state machine" or "transducer" that gets synthesized by a tool that solves the synthesis problem.

  • similarly to the case of verification, the formula Specification(env_variable, sys_variable) describes the required system behavior.

    In synthesis, the specification is usually described using temporal logic formulas, possibly in combination with other constructs, e.g., graph-like constructs (that are syntactic sugar for temporal logic formulas).

A description of the view of realizability as quantifier elimination in the presence of quantifier alternation can be read in Section IV of this paper (PDF).

A TLA+ specification of realizability is the TLA+ module Realizability.tla. In particular, the alternation of quantifiers is present there in that:

IsRealizable(..., ...) <=> \E f, g, mem0:  \AA x, y:  ...

• The symbol \E denotes existential quantification of constants (identifiers whose values remain unchanged throughout behavior steps).

• The symbol \AA denotes universal quantification of variables (identifiers whose values can change over behavior steps).

• In TLA+, a "behavior" is an infinite sequence of states. (More precisely, a behavior is a function that maps each natural number to a state; this function is itself in the metatheory of TLA+.)

• In TLA+, a "state" is an assignment of values to names (of variables). (More precisely, a state is a function that maps each variable name to a value; this function is itself in the metatheory of TLA+.)

• a "value" of a variable is a "set" in the metatheory of TLA+, when talking about states within the metatheory. Such a metatheoretic value is the semantics of the "value" that that variable represents within the object theory, TLA+.

  So there are two set theories present in this discussion:

  • the set theory within TLA+ (the object theory is TLA+)
  • the set theory within the metatheory of TLA+.

  The metatheory of TLA+ is where the semantics of TLA+ is defined. Inside the metatheory of TLA+, expressions of the object language TLA+ take the form of strings of the metatheory (those strings are "values" in the set theory of the metatheory, thus sets in the metatheory).

More about this formalization of realizability in TLA+ can be found in this document.

A formal definition of open systems and closed systems can be found in this paper (PDF), which describes also the definition of realizability.